Играемся с Verilator, SMT2, Z3 Сделал тут небольшую песочницу, чтобы поиграться с рандомизацией в вериляторе. Напоминаю, что в предущих сериях верилятор перешёл на такой формат рандомизации: SV констрейны парсятся, из них составляется запрос в SMT2 синтаксисе, запрос отправляется в решатель в системе (типа z3). Там есть разные хитрости в процессе, захотелось на них посмотреть и поиграть с z3. В итоге сделал репо, в котором разворачивается верилятор и slang-server, есть сниппеты кода с рандомизацией, а z3 обернут в скрипт, чтобы дампить ввод-вывод в файлы. https://github.com/esynr3z/verilator-rand Вот так, например, преобразование выглядит на практике: Класс с констрейном: class Test; rand byte a; constraint a_c { a >= 0; a <= 10; } endclass SMT2 код: (set-logic QF_ABV) (check-sat) (reset) (set-option :produce-models true) (set-logic QF_ABV) (define-fun __Vbv ((b Bool)) (_ BitVec 1) (ite b #b1 #b0)) (define-fun __Vbool ((v (_ BitVec 1))) Bool (= #b1 v)) (declare-fun a () (_ BitVec 8)) (assert (= #b1 (__Vbv (bvsge ((_ sign_extend 24) a) #x00000000)))) (assert (= #b1 (__Vbv (bvsle ((_ sign_extend 24) a) #x0000000a)))) (check-sat) (get-value ( a)) (assert (= #b0 (bvxor ((_ extract 1 1) a) ((_ extract 2 2) a) ((_ extract 3 3) a) ((_ extract 5 5) a)))) (check-sat) (get-value ( a)) (assert (= #b1 (bvxor ((_ extract 0 0) a) ((_ extract 2 2) a) ((_ extract 6 6) a) ((_ extract 7 7) a)))) (check-sat) (get-value ( a)) (assert (= #b1 (bvxor ((_ extract 0 0) a) ((_ extract 1 1) a) ((_ extract 3 3) a) ((_ extract 4 4) a)))) (check-sat) (get-value ( a)) (assert (= #b1 (bvxor ((_ extract 0 0) a) ((_ extract 1 1) a) ((_ extract 3 3) a) ((_ extract 7 7) a)))) (check-sat) (get-value ( a)) Понятно, что подобные развлечения они для гурманов, но из практической пользы - можно забрать девконтейнер себе. Можно использовать чтобы баги в вериляторе воспроизводить/репортить, slang-server тестить, ну или просто разработку/ci вести. Удобно когда в два клика в вскоде разворачивается рабочее окружение с нужными версиями тулов и плагинов. #verilator @positiveslack