Google Git
Sign in
foss-fpga-tools/third_party/yosys/89834b98f7715b131193f8283f09d665b9290eff^2..89834b98f7715b131193f8283f09d665b9290eff/.
commit
89834b98f7715b131193f8283f09d665b9290eff
[log]
author
Clifford Wolf <clifford@clifford.at>
Thu Nov 14 11:52:41 2019 +0100
committer
Clifford Wolf <clifford@clifford.at>
Thu Nov 14 11:52:41 2019 +0100
tree
3830defbea85a6d26e377f42693fec47e1d4326a
parent
ab0fb19cfff7760bfd69b49ed6d81a823be2a6ba [diff]
parent
d88cc139a029764cf62d95b2eaaff99e270a134a [diff]
Merge branch 'label-bads-btor' of https://github.com/makaimann/yosys into makaimann-label-bads-btor

diff --git a/passes/fsm/fsm_detect.cc b/passes/fsm/fsm_detect.cc
index 5ae991b..fb38966 100644
--- a/passes/fsm/fsm_detect.cc
+++ b/passes/fsm/fsm_detect.cc

@@ -158,22 +158,25 @@
 		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 @@
 						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 5807178..a2ad87f 100644
--- a/passes/techmap/flowmap.cc
+++ b/passes/techmap/flowmap.cc

@@ -394,7 +394,7 @@
 
 	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 @@
 		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 @@
 
 				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 0d07577..1c8192b 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 f45951b..0bcc4e0 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 f834a4c..ba91e5f 100644
--- a/tests/arch/ecp5/fsm.ys
+++ b/tests/arch/ecp5/fsm.ys

@@ -2,11 +2,16 @@
 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 a8ba70f..a2db2ad 100644
--- a/tests/arch/efinix/fsm.ys
+++ b/tests/arch/efinix/fsm.ys

@@ -2,9 +2,11 @@
 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 5aacc6c..223ba07 100644
--- a/tests/arch/ice40/fsm.ys
+++ b/tests/arch/ice40/fsm.ys

@@ -2,12 +2,15 @@
 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 d2b4814..2a72c34 100644
--- a/tests/arch/xilinx/fsm.ys
+++ b/tests/arch/xilinx/fsm.ys

@@ -2,7 +2,11 @@
 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