Я ищу основанную на C ++ альтернативу языку SystemVerilog. Хотя я сомневаюсь, что что-то может сравниться с простотой и гибкостью языка ограничений SystemVerilog, я остановился на использовании Z3 или Gecode для того, над чем я работаю, в первую очередь потому, что они оба под лицензией MIT.
То, что я ищу, это:
- Поддержка битовых векторов переменного размера и арифметических битовых векторов c logi c операций. Например:
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 гораздо понятнее, учитывая, насколько тщательна его документация.
Упрощенная c модель программирования ограничений, близкая или похожая на SystemVerilog. Например, язык, на котором мне нужно только напечатать (x == y + z) вместо чего-то вроде EQ (x, y + z). Насколько я могу судить, оба API предоставляют такую простую модель программирования.
Средство выполнения ограниченной рандомизации ради создания случайного стимула. Например, я могу предоставить случайное начальное число, которое, в зависимости от ограничений, приведет к ответу, который может отличаться от предыдущего ответа. Подобно тому, как рандомизированные вызовы SystemVerilog могут давать новые случайные результаты. Gecode, кажется, поддерживает использование случайных семян. Z3, это гораздо менее понятно.
Поддержка взвешенного распределения. Gecode, кажется, поддерживает это с помощью взвешенных множеств. Я предполагаю, что могу установить sh связь между определенными условиями и логическими переменными, а затем добавить веса к этим переменным. Z3 выглядит более гибким в том смысле, что вы можете присваивать веса выражениям через класс оптимизации.
В данный момент я не определился, потому что Z3 не хватает документации, чего не хватает в Gecode готовые типы переменных. Мне интересно, есть ли у кого-либо предыдущий опыт использования любого инструмента для достижения того, что мог бы SystemVerilog. Я также хотел бы услышать любые предложения по любому другому API под гибкой лицензией.