From 778079b058a54c3d935bb4e39a8aa26957fb14dd Mon Sep 17 00:00:00 2001 From: "Emil J. Tywoniak" Date: Tue, 24 Jun 2025 12:01:12 +0200 Subject: [PATCH 1/3] dfflibmap: propagate negated next_state to output correctly --- passes/techmap/dfflibmap.cc | 18 +++- tests/techmap/dfflibmap_dffsr_not_next.lib | 28 +++++ tests/techmap/dfflibmap_formal.ys | 116 +++++++++++++++++++++ 3 files changed, 160 insertions(+), 2 deletions(-) create mode 100644 tests/techmap/dfflibmap_dffsr_not_next.lib create mode 100644 tests/techmap/dfflibmap_formal.ys diff --git a/passes/techmap/dfflibmap.cc b/passes/techmap/dfflibmap.cc index d00fee83b..f0b0ef20b 100644 --- a/passes/techmap/dfflibmap.cc +++ b/passes/techmap/dfflibmap.cc @@ -392,9 +392,21 @@ static void find_cell_sr(std::vector cells, IdString cell_ty continue; if (!parse_next_state(cell, ff->find("next_state"), cell_next_pin, cell_next_pol, cell_enable_pin, cell_enable_pol)) continue; - if (!parse_pin(cell, ff->find("preset"), cell_set_pin, cell_set_pol) || cell_set_pol != setpol) + + if (!parse_pin(cell, ff->find("preset"), cell_set_pin, cell_set_pol)) continue; - if (!parse_pin(cell, ff->find("clear"), cell_clr_pin, cell_clr_pol) || cell_clr_pol != clrpol) + if (!parse_pin(cell, ff->find("clear"), cell_clr_pin, cell_clr_pol)) + continue; + if (!cell_next_pol) { + // next_state is negated + // we later propagate this inversion to the output, + // which requires the swap of set and reset + std::swap(cell_set_pin, cell_clr_pin); + std::swap(cell_set_pol, cell_clr_pol); + } + if (cell_set_pol != setpol) + continue; + if (cell_clr_pol != clrpol) continue; std::map this_cell_ports; @@ -432,12 +444,14 @@ static void find_cell_sr(std::vector cells, IdString cell_ty for (size_t pos = value.find_first_of("\" \t"); pos != std::string::npos; pos = value.find_first_of("\" \t")) value.erase(pos, 1); if (value == ff->args[0]) { + // next_state negation propagated to output this_cell_ports[pin->args[0]] = cell_next_pol ? 'Q' : 'q'; if (cell_next_pol) found_noninv_output = true; found_output = true; } else if (value == ff->args[1]) { + // next_state negation propagated to output this_cell_ports[pin->args[0]] = cell_next_pol ? 'q' : 'Q'; if (!cell_next_pol) found_noninv_output = true; diff --git a/tests/techmap/dfflibmap_dffsr_not_next.lib b/tests/techmap/dfflibmap_dffsr_not_next.lib new file mode 100644 index 000000000..579dedb10 --- /dev/null +++ b/tests/techmap/dfflibmap_dffsr_not_next.lib @@ -0,0 +1,28 @@ +library (test_not_next) { + cell (dffsr_not_next) { + area : 1.0; + pin (Q) { + direction : output; + function : "STATE"; + } + pin (CLK) { + clock : true; + direction : input; + } + pin (D) { + direction : input; + } + pin (RN) { + direction : input; + } + pin (SN) { + direction : input; + } + ff (STATE,STATEN) { + clear : "!SN"; + clocked_on : "CLK"; + next_state : "!D"; + preset : "!RN"; + } + } +} \ No newline at end of file diff --git a/tests/techmap/dfflibmap_formal.ys b/tests/techmap/dfflibmap_formal.ys new file mode 100644 index 000000000..11c90ea6c --- /dev/null +++ b/tests/techmap/dfflibmap_formal.ys @@ -0,0 +1,116 @@ +################################################################## + +read_verilog -sv -icells < Date: Tue, 24 Jun 2025 12:31:30 +0200 Subject: [PATCH 2/3] fixup! dfflibmap: propagate negated next_state to output correctly --- tests/techmap/dfflibmap_dffr_not_next.lib | 33 +++++++++++++++++++++++ 1 file changed, 33 insertions(+) create mode 100644 tests/techmap/dfflibmap_dffr_not_next.lib diff --git a/tests/techmap/dfflibmap_dffr_not_next.lib b/tests/techmap/dfflibmap_dffr_not_next.lib new file mode 100644 index 000000000..74004bea1 --- /dev/null +++ b/tests/techmap/dfflibmap_dffr_not_next.lib @@ -0,0 +1,33 @@ +library(test) { + cell (dffr_not_next) { + 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; + } + pin(CLEAR) { + direction : input; + } + pin(PRESET) { + direction : input; + } + pin(Q) { + direction: output; + function : "IQ"; + } + pin(QN) { + direction: output; + function : "IQN"; + } + } +} From 7fe817c52f51591eaeb780e3022fe8f2a4114abc Mon Sep 17 00:00:00 2001 From: "Emil J. Tywoniak" Date: Thu, 10 Jul 2025 18:54:43 +0200 Subject: [PATCH 3/3] dfflibmap: test negated state next_state with mixed polarities --- tests/techmap/dfflibmap.ys | 16 ++++++++++ tests/techmap/dfflibmap_dffsr_mixedpol.lib | 35 ++++++++++++++++++++++ 2 files changed, 51 insertions(+) create mode 100644 tests/techmap/dfflibmap_dffsr_mixedpol.lib diff --git a/tests/techmap/dfflibmap.ys b/tests/techmap/dfflibmap.ys index 77488d60f..822d87a36 100644 --- a/tests/techmap/dfflibmap.ys +++ b/tests/techmap/dfflibmap.ys @@ -81,3 +81,19 @@ clean select -assert-count 0 t:dffn select -assert-count 5 t:dffsr select -assert-count 1 t:dffe + +design -load orig +dfflibmap -liberty dfflibmap.lib -liberty dfflibmap_dffsr_mixedpol.lib -dont_use dffsr +clean +# We have one more _NOT_ than with the regular dffsr +select -assert-count 6 t:$_NOT_ +select -assert-count 1 t:dffn +select -assert-count 4 t:dffsr_mixedpol +select -assert-count 1 t:dffe +# The additional NOT is on ff2. +# Originally, ff2.R is an active high "set". +# dffsr_mixedpol has functionally swapped labels due to the next_state inversion, +# so we use its CLEAR port for the "set", +# but we have to invert it because the CLEAR pin is active low. +# ff2.CLEAR = !R +select -assert-count 1 c:ff2 %x:+[CLEAR] %ci t:$_NOT_ %i diff --git a/tests/techmap/dfflibmap_dffsr_mixedpol.lib b/tests/techmap/dfflibmap_dffsr_mixedpol.lib new file mode 100644 index 000000000..8c6a2f509 --- /dev/null +++ b/tests/techmap/dfflibmap_dffsr_mixedpol.lib @@ -0,0 +1,35 @@ +library(test) { + cell (dffsr_mixedpol) { + area : 6; + ff("IQ", "IQN") { + // look here + next_state : "!D"; + clocked_on : "CLK"; + // look here + clear : "!CLEAR"; + preset : "PRESET"; + clear_preset_var1 : L; + clear_preset_var2 : L; + } + pin(D) { + direction : input; + } + pin(CLK) { + direction : input; + } + pin(CLEAR) { + direction : input; + } + pin(PRESET) { + direction : input; + } + pin(Q) { + direction: output; + function : "IQ"; + } + pin(QN) { + direction: output; + function : "IQN"; + } + } +}