aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--passes/fsm/fsm_detect.cc16
-rw-r--r--passes/techmap/flowmap.cc5
-rw-r--r--techlibs/common/cmp2lut.v2
-rw-r--r--tests/arch/anlogic/fsm.ys11
-rw-r--r--tests/arch/ecp5/fsm.ys13
-rw-r--r--tests/arch/efinix/fsm.ys8
-rw-r--r--tests/arch/ice40/fsm.ys13
-rw-r--r--tests/arch/xilinx/fsm.ys6
8 files changed, 48 insertions, 26 deletions
diff --git a/passes/fsm/fsm_detect.cc b/passes/fsm/fsm_detect.cc
index 5ae991b28..fb3896669 100644
--- a/passes/fsm/fsm_detect.cc
+++ b/passes/fsm/fsm_detect.cc
@@ -158,22 +158,25 @@ static void detect_fsm(RTLIL::Wire *wire)
std::set<sig2driver_entry_t> cellport_list;
sig2user.find(sig_q, cellport_list);
+ auto sig_q_bits = sig_q.to_sigbit_pool();
+
for (auto &cellport : cellport_list)
{
RTLIL::Cell *cell = cellport.first;
bool set_output = false, clr_output = false;
- if (cell->type == "$ne")
+ if (cell->type.in("$ne", "$reduce_or", "$reduce_bool"))
set_output = true;
- if (cell->type == "$eq")
+ if (cell->type.in("$eq", "$logic_not", "$reduce_and"))
clr_output = true;
- if (!set_output && !clr_output) {
- clr_output = true;
+ if (set_output || clr_output) {
for (auto &port_it : cell->connections())
- if (port_it.first != "\\A" || port_it.first != "\\Y")
- clr_output = false;
+ if (cell->input(port_it.first))
+ for (auto bit : assign_map(port_it.second))
+ if (bit.wire != nullptr && !sig_q_bits.count(bit))
+ goto next_cellport;
}
if (set_output || clr_output) {
@@ -184,6 +187,7 @@ static void detect_fsm(RTLIL::Wire *wire)
ce.set(sig, val);
}
}
+ next_cellport:;
}
SigSpec sig_y = sig_d, sig_undef;
diff --git a/passes/techmap/flowmap.cc b/passes/techmap/flowmap.cc
index 5807178dd..a2ad87f7d 100644
--- a/passes/techmap/flowmap.cc
+++ b/passes/techmap/flowmap.cc
@@ -394,7 +394,7 @@ struct FlowGraph
pair<pool<RTLIL::SigBit>, pool<RTLIL::SigBit>> edge_cut()
{
- pool<RTLIL::SigBit> x, xi;
+ pool<RTLIL::SigBit> x = {source}, xi; // X and X̅ in the paper
NodePrime source_prime = {source, true};
pool<NodePrime> visited;
@@ -437,6 +437,7 @@ struct FlowGraph
for (auto collapsed_node : collapsed[sink])
xi.insert(collapsed_node);
+ log_assert(x[source] && !xi[source]);
log_assert(!x[sink] && xi[sink]);
return {x, xi};
}
@@ -1050,7 +1051,7 @@ struct FlowmapWorker
auto cut_inputs = cut_lut_at_gate(lut, lut_gate);
pool<RTLIL::SigBit> gate_inputs = cut_inputs.first, other_inputs = cut_inputs.second;
- if (gate_inputs.empty() && (int)other_inputs.size() == order)
+ if (gate_inputs.empty() && (int)other_inputs.size() >= order)
{
if (debug_relax)
log(" Breaking would result in a (k+1)-LUT.\n");
diff --git a/techlibs/common/cmp2lut.v b/techlibs/common/cmp2lut.v
index 0d0757767..1c8192b85 100644
--- a/techlibs/common/cmp2lut.v
+++ b/techlibs/common/cmp2lut.v
@@ -7,7 +7,7 @@
// with n <= k inputs should be techmapped in this way, because this shortens the critical path
// from n to 1 by avoiding carry chains.
-(* techmap_celltype = "$eq $ne $lt $le $gt $ge" *)
+(* techmap_celltype = "$lt $le $gt $ge" *)
module _90_lut_cmp_ (A, B, Y);
parameter A_SIGNED = 0;
diff --git a/tests/arch/anlogic/fsm.ys b/tests/arch/anlogic/fsm.ys
index f45951b13..0bcc4e011 100644
--- a/tests/arch/anlogic/fsm.ys
+++ b/tests/arch/anlogic/fsm.ys
@@ -1,12 +1,15 @@
read_verilog ../common/fsm.v
hierarchy -top fsm
proc
-#flatten
-#ERROR: Found 4 unproven $equiv cells in 'equiv_status -assert'.
-#equiv_opt -assert -map +/anlogic/cells_sim.v synth_anlogic # equivalency check
-equiv_opt -map +/anlogic/cells_sim.v synth_anlogic # equivalency check
+flatten
+
+equiv_opt -run :prove -map +/anlogic/cells_sim.v synth_anlogic
+miter -equiv -make_assert -flatten gold gate miter
+sat -verify -prove-asserts -show-public -set-at 1 in_reset 1 -seq 20 -prove-skip 1 miter
+
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd fsm # Constrain all select calls below inside the top module
+
select -assert-count 1 t:AL_MAP_LUT2
select -assert-count 5 t:AL_MAP_LUT5
select -assert-count 1 t:AL_MAP_LUT6
diff --git a/tests/arch/ecp5/fsm.ys b/tests/arch/ecp5/fsm.ys
index f834a4c6b..ba91e5fc0 100644
--- a/tests/arch/ecp5/fsm.ys
+++ b/tests/arch/ecp5/fsm.ys
@@ -2,11 +2,16 @@ read_verilog ../common/fsm.v
hierarchy -top fsm
proc
flatten
-equiv_opt -assert -map +/ecp5/cells_sim.v synth_ecp5 # equivalency check
+
+equiv_opt -run :prove -map +/ecp5/cells_sim.v synth_ecp5
+miter -equiv -make_assert -flatten gold gate miter
+sat -verify -prove-asserts -show-public -set-at 1 in_reset 1 -seq 20 -prove-skip 1 miter
+
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd fsm # Constrain all select calls below inside the top module
+
select -assert-count 1 t:L6MUX21
-select -assert-count 13 t:LUT4
-select -assert-count 5 t:PFUMX
-select -assert-count 5 t:TRELLIS_FF
+select -assert-count 15 t:LUT4
+select -assert-count 6 t:PFUMX
+select -assert-count 6 t:TRELLIS_FF
select -assert-none t:L6MUX21 t:LUT4 t:PFUMX t:TRELLIS_FF %% t:* %D
diff --git a/tests/arch/efinix/fsm.ys b/tests/arch/efinix/fsm.ys
index a8ba70fdb..a2db2ad98 100644
--- a/tests/arch/efinix/fsm.ys
+++ b/tests/arch/efinix/fsm.ys
@@ -2,9 +2,11 @@ read_verilog ../common/fsm.v
hierarchy -top fsm
proc
flatten
-#ERROR: Found 4 unproven $equiv cells in 'equiv_status -assert'.
-#equiv_opt -assert -map +/efinix/cells_sim.v synth_efinix # equivalency check
-equiv_opt -map +/efinix/cells_sim.v synth_efinix # equivalency check
+
+equiv_opt -run :prove -map +/efinix/cells_sim.v synth_efinix
+miter -equiv -make_assert -flatten gold gate miter
+sat -verify -prove-asserts -show-public -set-at 1 in_reset 1 -seq 20 -prove-skip 1 miter
+
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd fsm # Constrain all select calls below inside the top module
diff --git a/tests/arch/ice40/fsm.ys b/tests/arch/ice40/fsm.ys
index 5aacc6c73..223ba070e 100644
--- a/tests/arch/ice40/fsm.ys
+++ b/tests/arch/ice40/fsm.ys
@@ -2,12 +2,15 @@ read_verilog ../common/fsm.v
hierarchy -top fsm
proc
flatten
-equiv_opt -assert -map +/ice40/cells_sim.v synth_ice40 # equivalency check
+
+equiv_opt -run :prove -map +/ice40/cells_sim.v synth_ice40
+miter -equiv -make_assert -flatten gold gate miter
+sat -verify -prove-asserts -show-public -set-at 1 in_reset 1 -seq 20 -prove-skip 1 miter
+
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd fsm # Constrain all select calls below inside the top module
+select -assert-count 4 t:SB_DFF
select -assert-count 2 t:SB_DFFESR
-select -assert-count 2 t:SB_DFFSR
-select -assert-count 1 t:SB_DFFSS
-select -assert-count 13 t:SB_LUT4
-select -assert-none t:SB_DFFESR t:SB_DFFSR t:SB_DFFSS t:SB_LUT4 %% t:* %D
+select -assert-count 15 t:SB_LUT4
+select -assert-none t:SB_DFFESR t:SB_DFF t:SB_LUT4 %% t:* %D
diff --git a/tests/arch/xilinx/fsm.ys b/tests/arch/xilinx/fsm.ys
index d2b481421..2a72c34e8 100644
--- a/tests/arch/xilinx/fsm.ys
+++ b/tests/arch/xilinx/fsm.ys
@@ -2,7 +2,11 @@ read_verilog ../common/fsm.v
hierarchy -top fsm
proc
flatten
-equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
+
+equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx
+miter -equiv -make_assert -flatten gold gate miter
+sat -verify -prove-asserts -show-public -set-at 1 in_reset 1 -seq 20 -prove-skip 1 miter
+
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd fsm # Constrain all select calls below inside the top module
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-18 16:43:33 +0000