Рандомизация в Verilator

Тут оказывается у верилятора сподвижки в рандомизации случились.

Если сжать всю историю до нескольких предложений, то

▫️ Первым заходом в рандомизацию было использование API-вызовов библиотеки CRAVE. Решение как оказалось было не совсем подходящим - слишком громоздкий и универсальный инструмент, который сильно усложняет сборку самого верилятора.
▫️Далее пошел заход через SMT-LIB2 - SV констрейны конвертируются в Lisp-подобное описание, которое идёт в рантайме на вход любому (почти) из популярных SMT-решателей, установленных в системе. Далее остается лишь забрать выхлоп и разложить по переменным.

Именно последний подход начали пиарить в недавних статье и докладе про текущие дела верилятора. Хотя PR на Github находился еще в работе, да и судя по комментариям мистер Снайдер похоже не сильно был воодушевлен таким подходом.

Однако, работу довели до мержа в мастер, и теперь по умолчанию верилятор пытается использовать z3, как бэкэнд для рандомизации.

Рандомизация работает, я проверил. Однако надо убедиться что решатель есть в системе, иначе в рантайме будет сюрприз

%Warning: Subprocess command `z3 --in' failed: exit status 127

Но сама рандомизация пока еще довольно слабая - можно глянуть в оригинальном PR, что ограничений пока довольно много.

#verilator
@positiveslack