1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
|
# Our implementation
read_verilog ../arith_map.v
read_verilog ../cells_sim.v
read_verilog -DSIMLIB_NOCHECKS ../../common/simlib.v
rename \$__SF2_ALU gate
hierarchy -top gate -chparam A_WIDTH 4 -chparam B_WIDTH 5 -chparam Y_WIDTH 5
flatten
opt
write_verilog gate.v
# The reference
read_verilog -DSIMLIB_NOCHECKS ../../common/simlib.v
rename \$alu gold
hierarchy -top gold -chparam A_WIDTH 4 -chparam B_WIDTH 5 -chparam Y_WIDTH 5
flatten
proc
clean
write_verilog gold.v
read_verilog gate.v
miter -equiv -flatten -make_outputs gold gate miter
sat -verify -prove trigger 0 -show-ports miter
|
