Сборка SMV

SMV - первый верификатор, в котором был реализован алгоритм символьной верификации на основе бинарных решающих диаграмм. Проект не радует своим дружелюбием, так как готовые сборки для linux не запускаются, из исходников проект собирается, но для этого пришлось поразбираться с исходными кодами. Чтобы сэкономить время другим желающим заняться верификацией, ниже описаны шаги по сборке SMV.

Шаг первый: скачиваем и распаковываем
Необходимо скачать исходные коды smv по ссылке smv.r2.5.4.3.tar.gz и распаковать:
tar -xzf smv.r2.5.4.3.tar.gz

Шаг второй: изменяем makefile
К строке в файле makefile
DFLAGS = -DBETTERHASH -DSMV_SIGNALS -DOTHER_SIMP
необходимо добавить
-DYYMALLOC=malloc

Шаг третий: собираем проект
Запустить сборку
make

Далее можно запустить один из примеров:
./smv examples/counter.smv
На экран должно быть выведено сообщение вида
-- specification AG AF bit2.carry_out is true
-- specification AG (!bit2.carry_out) is false
-- as demonstrated by the following execution sequence
state 1.1:
bit0.carry_out = 0
bit0.value = 0
bit1.carry_out = 0
bit1.value = 0
bit2.carry_out = 0
bit2.value = 0
...