diff --git a/tests/techmap/dfflibmap.ys b/tests/techmap/dfflibmap.ys index 87ecc8bc7..499907d10 100644 --- a/tests/techmap/dfflibmap.ys +++ b/tests/techmap/dfflibmap.ys @@ -26,6 +26,8 @@ equiv_opt -map dfflibmap-sim.v -assert -multiclock dfflibmap -prepare -liberty d dfflibmap -prepare -liberty dfflibmap.lib equiv_opt -map dfflibmap-sim.v -assert -multiclock dfflibmap -map-only -liberty dfflibmap.lib +################################################################## + design -load orig dfflibmap -liberty dfflibmap.lib clean @@ -74,6 +76,8 @@ select -assert-count 1 t:dffe select -assert-count 4 t:dffsr select -assert-none t:dffn t:dffsr t:dffe t:$_NOT_ %% %n t:* %i +################################################################## + design -load orig dfflibmap -liberty dfflibmap.lib -dont_use *ffn clean @@ -82,6 +86,13 @@ select -assert-count 0 t:dffn select -assert-count 5 t:dffsr select -assert-count 1 t:dffe +################################################################## + +design -load orig +read_liberty -lib dfflibmap.lib dfflibmap_dffsr_mixedpol.lib +stat +equiv_opt -map dfflibmap-sim.v -map dfflibmap_dffsr_mixedpol-sim.v -assert -multiclock dfflibmap -liberty dfflibmap.lib -liberty dfflibmap_dffsr_mixedpol.lib -dont_use dffsr + design -load orig dfflibmap -liberty dfflibmap.lib -liberty dfflibmap_dffsr_mixedpol.lib -dont_use dffsr clean diff --git a/tests/techmap/dfflibmap_dffsr_h.lib b/tests/techmap/dfflibmap_dffsr_h.lib new file mode 100644 index 000000000..a49f23a35 --- /dev/null +++ b/tests/techmap/dfflibmap_dffsr_h.lib @@ -0,0 +1,34 @@ +library(test) { + cell (dffsr) { + area : 6; + ff("IQ", "IQN") { + next_state : "D"; + clocked_on : "CLK"; + clear : "CLEAR"; + preset : "PRESET"; + clear_preset_var1 : H; + clear_preset_var2 : H; + } + pin(D) { + direction : input; + } + pin(CLK) { + direction : input; + clock : true; + } + pin(CLEAR) { + direction : input; + } + pin(PRESET) { + direction : input; + } + pin(Q) { + direction: output; + function : "IQ"; + } + pin(QN) { + direction: output; + function : "IQN"; + } + } +} diff --git a/tests/techmap/dfflibmap_dffsr_l.lib b/tests/techmap/dfflibmap_dffsr_l.lib new file mode 100644 index 000000000..10c3480a0 --- /dev/null +++ b/tests/techmap/dfflibmap_dffsr_l.lib @@ -0,0 +1,34 @@ +library(test) { + cell (dffsr) { + area : 6; + ff("IQ", "IQN") { + next_state : "D"; + clocked_on : "CLK"; + clear : "CLEAR"; + preset : "PRESET"; + clear_preset_var1 : L; + clear_preset_var2 : L; + } + pin(D) { + direction : input; + } + pin(CLK) { + direction : input; + clock : true; + } + pin(CLEAR) { + direction : input; + } + pin(PRESET) { + direction : input; + } + pin(Q) { + direction: output; + function : "IQ"; + } + pin(QN) { + direction: output; + function : "IQN"; + } + } +} diff --git a/tests/techmap/dfflibmap_dffsr_mixedpol-sim.v b/tests/techmap/dfflibmap_dffsr_mixedpol-sim.v new file mode 100644 index 000000000..9babda0b5 --- /dev/null +++ b/tests/techmap/dfflibmap_dffsr_mixedpol-sim.v @@ -0,0 +1,10 @@ +module dffsr_mixedpol(input CLK, D, CLEAR, PRESET, output reg Q, output QN); + + always @(posedge CLK, negedge CLEAR, posedge PRESET) + if (PRESET) Q <= 1'b1; + else if (~CLEAR) Q <= 1'b0; + else Q <= ~D; + + assign QN = ~Q; + +endmodule diff --git a/tests/techmap/dfflibmap_dffsr_r.lib b/tests/techmap/dfflibmap_dffsr_r.lib index f36e200a0..433748375 100644 --- a/tests/techmap/dfflibmap_dffsr_r.lib +++ b/tests/techmap/dfflibmap_dffsr_r.lib @@ -14,6 +14,7 @@ library(test) { } pin(CLK) { direction : input; + clock : true; } pin(CLEAR) { direction : input; diff --git a/tests/techmap/dfflibmap_dffsr_s.lib b/tests/techmap/dfflibmap_dffsr_s.lib index cf930f3c7..da9919286 100644 --- a/tests/techmap/dfflibmap_dffsr_s.lib +++ b/tests/techmap/dfflibmap_dffsr_s.lib @@ -14,6 +14,7 @@ library(test) { } pin(CLK) { direction : input; + clock : true; } pin(CLEAR) { direction : input; diff --git a/tests/techmap/dfflibmap_dffsr_x.lib b/tests/techmap/dfflibmap_dffsr_x.lib index 91d702412..3c7f625c3 100644 --- a/tests/techmap/dfflibmap_dffsr_x.lib +++ b/tests/techmap/dfflibmap_dffsr_x.lib @@ -14,6 +14,7 @@ library(test) { } pin(CLK) { direction : input; + clock : true; } pin(CLEAR) { direction : input; diff --git a/tests/techmap/dfflibmap_formal.ys b/tests/techmap/dfflibmap_formal.ys index afa2c4d9d..7f44c0d23 100644 --- a/tests/techmap/dfflibmap_formal.ys +++ b/tests/techmap/dfflibmap_formal.ys @@ -88,6 +88,86 @@ $_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])); + +$_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_l.lib + +copy top top_unmapped +dfflibmap -liberty dfflibmap_dffsr_l.lib top + +clk2fflogic +flatten +opt_clean -purge +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 <