mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2026-03-04 12:40:25 +00:00
Code Activity

dfflibmap: fix formal $dffsr tests with sat, prove "no s&r" assumption only needed when appropriate

Browse source
This commit is contained in:
Emil J. Tywoniak 2026-03-03 01:19:22 +01:00
parent 22916aaab1
commit 5b4603c54f
4 changed files with 121 additions and 38 deletions
Download patch file Download diff file Expand all files Collapse all files

89
tests/techmap/dfflibmap_formal.ys
View file

@ -8,6 +8,7 @@ $_DFF_P_ ff0 (.C(C), .D(D), .Q(Q[0]));
$_DFF_PP0_ ff1 (.C(C), .D(D), .R(R), .Q(Q[1]));
$_DFF_PP1_ ff2 (.C(C), .D(D), .R(R), .Q(Q[2]));
assume property (~R || ~S);
$_DFFSR_PPP_ ff3 (.C(C), .D(D), .R(R), .S(S), .Q(Q[3]));
$_DFFSR_NNN_ ff4 (.C(C), .D(D), .R(~R), .S(~S), .Q(Q[4]));
@ -29,9 +30,12 @@ dfflibmap -liberty dfflibmap_dffsr_s.lib top
clk2fflogic
flatten
opt_clean -purge
equiv_make top top_unmapped equiv
equiv_induct -set-assumes equiv
equiv_status -assert equiv
miter -equiv -make_assert -flatten top_unmapped top miter
hierarchy -top miter
# Prove that this is equivalent with the assumption
sat -verify -prove-asserts -set-assumes -enable_undef -set-init-undef -show-public -seq 3 miter
# Prove that this is NOT equivalent WITHOUT the assumption
sat -falsify -prove-asserts -enable_undef -set-init-undef -seq 3 miter
##################################################################
@ -44,6 +48,7 @@ $_DFF_P_ ff0 (.C(C), .D(D), .Q(Q[0]));
$_DFF_PP0_ ff1 (.C(C), .D(D), .R(R), .Q(Q[1]));
$_DFF_PP1_ ff2 (.C(C), .D(D), .R(R), .Q(Q[2]));
assume property (~R || ~S);
$_DFFSR_PPP_ ff3 (.C(C), .D(D), .R(R), .S(S), .Q(Q[3]));
$_DFFSR_NNN_ ff4 (.C(C), .D(D), .R(~R), .S(~S), .Q(Q[4]));
@ -65,9 +70,52 @@ dfflibmap -liberty dfflibmap_dffsr_r.lib top
clk2fflogic
flatten
opt_clean -purge
equiv_make top top_unmapped equiv
equiv_induct -set-assumes equiv
equiv_status -assert equiv
miter -equiv -make_assert -flatten top_unmapped top miter
hierarchy -top miter
# Prove that this is equivalent with the assumption
sat -verify -prove-asserts -set-assumes -enable_undef -set-init-undef -show-public -seq 3 miter
# Prove that this is NOT equivalent WITHOUT the assumption
sat -falsify -prove-asserts -enable_undef -set-init-undef -seq 3 miter
##################################################################
design -reset
read_verilog -sv -icells <<EOT
module top(input C, D, E, S, R, output [11:0] Q);
$_DFF_P_ ff0 (.C(C), .D(D), .Q(Q[0]));
$_DFF_PP0_ ff1 (.C(C), .D(D), .R(R), .Q(Q[1]));
$_DFF_PP1_ ff2 (.C(C), .D(D), .R(R), .Q(Q[2]));
// no assume when mapping to X
$_DFFSR_PPP_ ff3 (.C(C), .D(D), .R(R), .S(S), .Q(Q[3]));
$_DFFSR_NNN_ ff4 (.C(C), .D(D), .R(~R), .S(~S), .Q(Q[4]));
$_DFFE_PP_ ff5 (.C(C), .D(D), .E(E), .Q(Q[5]));
assign Q[11:6] = ~Q[5:0];
endmodule
EOT
proc
opt
read_liberty dfflibmap_dffsr_x.lib
opt
copy top top_unmapped
dfflibmap -liberty dfflibmap_dffsr_x.lib top
clk2fflogic
flatten
opt_clean -purge
miter -equiv -make_assert -flatten top_unmapped top miter
hierarchy -top miter
# Prove that this is equivalent
sat -verify -prove-asserts -set-init-undef -show-public -seq 3 miter
##################################################################
@ -83,8 +131,7 @@ $_DFF_PP1_ ff2 (.C(C), .D(D), .R(R), .Q(Q[2]));
// Formal checking of directly instantiated DFFSR doesn't work at the moment
// likely due to an equiv_induct -set-assumes assume bug #5196
// Workaround for DFFSR bug #5194
assume property (~R || ~S);
// no assume when mapping to unset clear_preset_var
$_DFFSR_PPP_ ff3 (.C(C), .D(D), .R(R), .S(S), .Q(Q[3]));
$_DFFSR_NNN_ ff4 (.C(C), .D(D), .R(~R), .S(~S), .Q(Q[4]));
@ -107,9 +154,11 @@ dfflibmap -liberty dfflibmap_dffn_dffe.lib -liberty dfflibmap_dffsr_not_next.lib
clk2fflogic
flatten
opt_clean -purge
equiv_make top top_unmapped equiv
equiv_induct -set-assumes equiv
equiv_status -assert equiv
miter -equiv -make_assert -flatten top_unmapped top miter
hierarchy -top miter
# Prove that this is equivalent
sat -verify -prove-asserts -set-init-undef -show-public -seq 3 miter
##################################################################
@ -122,10 +171,6 @@ $_DFF_P_ ff0 (.C(C), .D(D), .Q(Q[0]));
$_DFF_PP0_ ff1 (.C(C), .D(D), .R(R), .Q(Q[1]));
$_DFF_PP1_ ff2 (.C(C), .D(D), .R(R), .Q(Q[2]));
// Formal checking of directly instantiated DFFSR doesn't work at the moment
// likely due to an equiv_induct -set-assumes assume bug #5196
// Workaround for DFFSR inconsistency #5194
assume property (~R || ~S);
$_DFFSR_PPP_ ff3 (.C(C), .D(D), .R(R), .S(S), .Q(Q[3]));
$_DFFSR_NNN_ ff4 (.C(C), .D(D), .R(~R), .S(~S), .Q(Q[4]));
@ -140,17 +185,21 @@ EOT
proc
opt
read_liberty dfflibmap_dffr_not_next.lib
read_liberty dfflibmap_dffsr_not_next_l.lib
copy top top_unmapped
dfflibmap -liberty dfflibmap_dffr_not_next.lib top
dfflibmap -liberty dfflibmap_dffsr_not_next_l.lib top
clk2fflogic
flatten
opt_clean -purge
equiv_make top top_unmapped equiv
equiv_induct -set-assumes equiv
equiv_status -assert equiv
miter -equiv -make_assert -flatten top_unmapped top miter
hierarchy -top miter
# Prove that this is equivalent with the assumption
sat -verify -prove-asserts -set-assumes -enable_undef -set-init-undef -show-public -seq 3 miter
# Prove that this is NOT equivalent WITHOUT the assumption
sat -falsify -prove-asserts -enable_undef -set-init-undef -seq 3 miter
##################################################################