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

Merge pull request #4 from alainmarcel/new_peepopts 

Switch formal proof to use miter/sat
This commit is contained in:
Akash Levy 2024-12-18 10:53:11 -08:00 committed by GitHub
parent d81bda8ce7 ff5237f4b2
commit 029c25536c
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
1 changed files with 52 additions and 14 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

66
tests/peepopt/muxadd.ys
View File

@ -7,17 +7,21 @@ module top(a, b, s, y);
input wire [3:0] b; input wire [3:0] b;
input wire s; input wire s;
output wire [3:0] y; output wire [3:0] y;
assign y = s ? (a + b) : a; assign y = s ? (a + b) : a;
endmodule endmodule
EOF EOF
check -assert check -assert
equiv_opt -assert peepopt ;;; copy top orig
design -load postopt cd top
peepopt
select -assert-any t:$add %co1 %a w:y %i # assert adder rewired select -assert-any t:$add %co1 %a w:y %i # assert adder rewired
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 basic s?(a+b):a pattern with intermediate var gets transformed (a,b module inputs)" log -header "Test basic s?(a+b):a pattern with intermediate var gets transformed (a,b module inputs)"
log -push log -push
design -reset design -reset
@ -33,9 +37,15 @@ module top(a, b, s, y);
endmodule endmodule
EOF EOF
check -assert check -assert
equiv_opt -assert peepopt ;;; copy top orig
design -load postopt cd top
peepopt
select -assert-any t:$add %co1 %a w:y %i # assert adder rewired select -assert-any t:$add %co1 %a w:y %i # assert adder rewired
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 basic s?(a+b):a pattern gets transformed (a is driven by a cell)" log -header "Test basic s?(a+b):a pattern gets transformed (a is driven by a cell)"
@ -54,9 +64,15 @@ module top(a_, b, s, y);
endmodule endmodule
EOF EOF
check -assert check -assert
equiv_opt -assert peepopt copy top orig
design -load postopt cd top
peepopt
select -assert-any t:$add %co1 %a w:y %i # assert adder rewired select -assert-any t:$add %co1 %a w:y %i # assert adder rewired
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 basic s?(a+b):a pattern gets transformed (b is driven by a cell, output consumed by a cell)" log -header "Test basic s?(a+b):a pattern gets transformed (b is driven by a cell, output consumed by a cell)"
@ -78,9 +94,15 @@ module top(a, b_, f, s, y_);
endmodule endmodule
EOF EOF
check -assert check -assert
equiv_opt -assert peepopt copy top orig
design -load postopt cd top
peepopt
select -assert-any t:$add %co1 %a w:y %i # assert adder rewired select -assert-any t:$add %co1 %a w:y %i # assert adder rewired
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 no transform when a+b has more fanouts (module output)" log -header "Test no transform when a+b has more fanouts (module output)"
@ -98,9 +120,15 @@ module top(a, b, ab, s, y);
endmodule endmodule
EOF EOF
check -assert check -assert
equiv_opt -assert peepopt copy top orig
design -load postopt cd top
peepopt
select -assert-none t:$add %co1 %a w:y %i select -assert-none t:$add %co1 %a w:y %i
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 no transform when a+b has more fanouts (single bit, cell)" log -header "Test no transform when a+b has more fanouts (single bit, cell)"
@ -118,9 +146,19 @@ module top(a, b, s, y, z);
endmodule endmodule
EOF EOF
check -assert check -assert
equiv_opt -assert peepopt copy top orig
design -load postopt cd top
peepopt
select -assert-none t:$add %co1 %a w:y %i select -assert-none t:$add %co1 %a w:y %i
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 Please fix all the designs below to use the miter/sat proof
quit
log -pop log -pop
log -header "Test no transform when a+b width smaller than a's width" log -header "Test no transform when a+b width smaller than a's width"