summaryrefslogtreecommitdiff
path: root/frontends/verific/test_navre.ys
blob: a56b725ac4e73f0c0876c57bdc9b25dd8bbdc894 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
verific -vlog2k ../yosys-bigsim/softusb_navre/rtl/softusb_navre.v
verific -import softusb_navre

memory softusb_navre
flatten softusb_navre
rename softusb_navre gate

read_verilog ../yosys-bigsim/softusb_navre/rtl/softusb_navre.v
cd softusb_navre; proc; opt; memory; opt; cd ..
rename softusb_navre gold

expose -dff -shared gold gate
miter -equiv -ignore_gold_x -make_assert -make_outputs -make_outcmp gold gate miter

cd miter
flatten; opt -undriven
sat -verify -maxsteps 5 -set-init-undef -set-def-inputs -prove-asserts -tempinduct-def \
    -seq 1 -set-at 1 in_rst 1 # -show-inputs -show-outputs