Я ищу альтернативу языку SystemVerilog на основе C ++. Хотя я сомневаюсь, что что-то там может сравниться с простотой и гибкостью языка ограничений SystemVerilog, я решил использовать Z3 или Gecode для того, над чем я работаю, в первую очередь потому, что они оба находятся под лицензией MIT.
Я ищу:
- Поддержка битовых векторов переменного размера И арифметических логических операций с битовыми векторами. Например:
bit_vector a<30>; bit_vector b<30>; constraint { a == (b << 2); a == (b * 2); b < a; }
Проблема с Gecode, насколько я могу судить, в том, что он не предоставляет битовые векторы прямо из коробки. Однако его модель программирования кажется немного проще, и она действительно предоставляет средства для создания собственных типов переменных. Так что, возможно, я мог бы создать какую-то оболочку вокруг битового набора C ++, похожую на то, как IntVar обертывает 32-битные целые числа. Однако в этом случае не будет возможности выполнять ограничения на основе умножения, поскольку битовые наборы C ++ не поддерживают такие операции.
Z3 предоставляет битовые векторы прямо из коробки, но я не уверен, как он справится с попыткой установить ограничения, например, на 128-битные векторы. Я также не уверен, как я могу указать, что я хочу создать множество случайных переменных, которые удовлетворяют ограничению, когда это возможно. С Gecode это намного яснее, учитывая, насколько тщательна его документация.
Упрощенная модель программирования ограничений, близкая или аналогичная SystemVerilog. Например, язык, на котором мне нужно только ввести (x == y + z) вместо чего-то вроде EQ (x, y + z). Насколько я могу судить, оба API предоставляют такую простую модель программирования.
Средство выполнения ограниченной рандомизации ради создания случайного стимула. То есть, я могу предоставить случайное начальное число, которое, в зависимости от ограничений, приведет к ответу, который может отличаться от предыдущего ответа. Подобно тому, как SystemVerilog рандомизирует вызовы, может давать новые случайные результаты. Gecode, похоже, поддерживает использование случайных начальных чисел. Z3, все гораздо менее понятно.
Поддержка взвешенного распределения. Gecode, похоже, поддерживает это посредством взвешенных наборов. Я полагаю, что могу установить связь между определенными условиями и логическими переменными, а затем добавить веса к этим переменным. Z3 кажется более гибким в том смысле, что вы можете назначать веса выражениям с помощью класса optimize.
На данный момент я не определился, потому что в Z3 отсутствует документация, чего не хватает Gecode в стандартных типах переменных. Мне интересно, есть ли у кого-нибудь предыдущий опыт использования любого инструмента для достижения того, что может SystemVerilog. Я также хотел бы услышать предложения по любому другому API с гибкой лицензией.
