Сделал тут небольшую песочницу, чтобы поиграться с рандомизацией в вериляторе.
Напоминаю, что в предущих сериях верилятор перешёл на такой формат рандомизации: 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
