riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity

Convert to miter/sat

This commit is contained in:
Alain Dargelas 2024-12-18 10:54:54 -08:00
parent ff5237f4b2
commit 7b70ba4fd6
1 changed files with 20 additions and 9 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

29
tests/peepopt/multdiv_c.ys
View File

@ -2,7 +2,7 @@ log -header "Test simple positive case"
log -push log -push
design -reset design -reset
read_verilog <<EOF read_verilog <<EOF
module muldiv_const_ok ( module top (
input wire [31:0] a, input wire [31:0] a,
output wire [63:0] y output wire [63:0] y
); );
@ -10,16 +10,22 @@ module muldiv_const_ok (
endmodule endmodule
EOF EOF
check -assert check -assert
equiv_opt -assert peepopt ;;; copy top orig
design -load postopt cd top
select -assert-any t:$mul # assert mult peepopt
select -assert-none t:$div
clean -purge
cd
miter -equiv -flatten -make_assert -make_outputs -ignore_gold_x top orig miter
sat -verify -prove-asserts -show-ports -enable_undef miter
log -pop log -pop
log -header "Test negative case where div is kept" log -header "Test negative case where div is kept"
log -push log -push
design -reset design -reset
read_verilog <<EOF read_verilog <<EOF
module muldiv_const_ko ( module top (
input wire signed [31:0] a, input wire signed [31:0] a,
output wire signed [63:0] y, output wire signed [63:0] y,
output wire probe output wire probe
@ -31,8 +37,13 @@ module muldiv_const_ko (
endmodule endmodule
EOF EOF
check -assert check -assert
equiv_opt -assert peepopt ;;; copy top orig
design -load postopt cd top
select -assert-any t:$div # assert div peepopt
select -assert-any t:$div
clean -purge
cd
miter -equiv -flatten -make_assert -make_outputs -ignore_gold_x top orig miter
sat -verify -prove-asserts -show-ports -enable_undef miter
log -pop