Тут оказывается у верилятора сподвижки в рандомизации случились.
Если сжать всю историю до нескольких предложений, то
▫️ Первым заходом в рандомизацию было использование API-вызовов библиотеки CRAVE. Решение как оказалось было не совсем подходящим - слишком громоздкий и универсальный инструмент, который сильно усложняет сборку самого верилятора.
▫️Далее пошел заход через SMT-LIB2 - SV констрейны конвертируются в Lisp-подобное описание, которое идёт в рантайме на вход любому (почти) из популярных SMT-решателей, установленных в системе. Далее остается лишь забрать выхлоп и разложить по переменным.
Именно последний подход начали пиарить в недавних статье и докладе про текущие дела верилятора. Хотя PR на Github находился еще в работе, да и судя по комментариям мистер Снайдер похоже не сильно был воодушевлен таким подходом.
Однако, работу довели до мержа в мастер, и теперь по умолчанию верилятор пытается использовать z3, как бэкэнд для рандомизации.
Рандомизация работает, я проверил. Однако надо убедиться что решатель есть в системе, иначе в рантайме будет сюрприз
%Warning: Subprocess command `z3 --in' failed: exit status 127
Но сама рандомизация пока еще довольно слабая - можно глянуть в оригинальном PR, что ограничений пока довольно много.
#verilator
@positiveslack