Merge remote-tracking branch 'origin/master' into eddie/abc9_refactor

6 files changed, 241 insertions, 28 deletions

diff --git a/passes/fsm/fsm_detect.cc b/passes/fsm/fsm_detect.cc
index fb3896669..a1c8067b4 100644
--- a/passes/fsm/fsm_detect.cc
+++ b/passes/fsm/fsm_detect.cc
@@ -34,13 +34,20 @@ static SigSet<sig2driver_entry_t> sig2driver, sig2user;
 static std::set<RTLIL::Cell*> muxtree_cells;
 static SigPool sig_at_port;
 
-static bool check_state_mux_tree(RTLIL::SigSpec old_sig, RTLIL::SigSpec sig, pool<Cell*> &recursion_monitor)
+static bool check_state_mux_tree(RTLIL::SigSpec old_sig, RTLIL::SigSpec sig, pool<Cell*> &recursion_monitor, dict<RTLIL::SigSpec, bool> &mux_tree_cache)
 {
+	if (mux_tree_cache.find(sig) != mux_tree_cache.end())
+		return mux_tree_cache.at(sig);
+
 	if (sig.is_fully_const() || old_sig == sig) {
+ret_true:
+		mux_tree_cache[sig] = true;
 		return true;
 	}
 
 	if (sig_at_port.check_any(assign_map(sig))) {
+ret_false:
+		mux_tree_cache[sig] = false;
 		return false;
 	}
 
@@ -49,13 +56,13 @@ static bool check_state_mux_tree(RTLIL::SigSpec old_sig, RTLIL::SigSpec sig, poo
 	for (auto &cellport : cellport_list)
 	{
 		if ((cellport.first->type != "$mux" && cellport.first->type != "$pmux") || cellport.second != "\\Y") {
-			return false;
+			goto ret_false;
 		}
 
 		if (recursion_monitor.count(cellport.first)) {
 			log_warning("logic loop in mux tree at signal %s in module %s.\n",
 					log_signal(sig), RTLIL::id2cstr(module->name));
-			return false;
+			goto ret_false;
 		}
 
 		recursion_monitor.insert(cellport.first);
@@ -63,22 +70,22 @@ static bool check_state_mux_tree(RTLIL::SigSpec old_sig, RTLIL::SigSpec sig, poo
 		RTLIL::SigSpec sig_a = assign_map(cellport.first->getPort("\\A"));
 		RTLIL::SigSpec sig_b = assign_map(cellport.first->getPort("\\B"));
 
-		if (!check_state_mux_tree(old_sig, sig_a, recursion_monitor)) {
+		if (!check_state_mux_tree(old_sig, sig_a, recursion_monitor, mux_tree_cache)) {
 			recursion_monitor.erase(cellport.first);
-			return false;
+			goto ret_false;
 		}
 
 		for (int i = 0; i < sig_b.size(); i += sig_a.size())
-			if (!check_state_mux_tree(old_sig, sig_b.extract(i, sig_a.size()), recursion_monitor)) {
+			if (!check_state_mux_tree(old_sig, sig_b.extract(i, sig_a.size()), recursion_monitor, mux_tree_cache)) {
 				recursion_monitor.erase(cellport.first);
-				return false;
+				goto ret_false;
 			}
 
 		recursion_monitor.erase(cellport.first);
 		muxtree_cells.insert(cellport.first);
 	}
 
-	return true;
+	goto ret_true;
 }
 
 static bool check_state_users(RTLIL::SigSpec sig)
@@ -143,11 +150,12 @@ static void detect_fsm(RTLIL::Wire *wire)
 		pool<Cell*> recursion_monitor;
 		RTLIL::SigSpec sig_q = assign_map(cellport.first->getPort("\\Q"));
 		RTLIL::SigSpec sig_d = assign_map(cellport.first->getPort("\\D"));
+		dict<RTLIL::SigSpec, bool> mux_tree_cache;
 
 		if (sig_q != assign_map(wire))
 			continue;
 
-		looks_like_state_reg = check_state_mux_tree(sig_q, sig_d, recursion_monitor);
+		looks_like_state_reg = check_state_mux_tree(sig_q, sig_d, recursion_monitor, mux_tree_cache);
 		looks_like_good_state_reg = check_state_users(sig_q);
 
 		if (!looks_like_state_reg)
diff --git a/passes/pmgen/ice40_dsp.cc b/passes/pmgen/ice40_dsp.cc
index f60e67158..c364cd91a 100644
--- a/passes/pmgen/ice40_dsp.cc
+++ b/passes/pmgen/ice40_dsp.cc
@@ -73,11 +73,11 @@ void create_ice40_dsp(ice40_dsp_pm &pm)
 
 	// SB_MAC16 Input Interface
 	SigSpec A = st.sigA;
-	A.extend_u0(16, st.mul->getParam(ID(A_SIGNED)).as_bool());
+	A.extend_u0(16, st.mul->parameters.at(ID(A_SIGNED), State::S0).as_bool());
 	log_assert(GetSize(A) == 16);
 
 	SigSpec B = st.sigB;
-	B.extend_u0(16, st.mul->getParam(ID(B_SIGNED)).as_bool());
+	B.extend_u0(16, st.mul->parameters.at(ID(B_SIGNED), State::S0).as_bool());
 	log_assert(GetSize(B) == 16);
 
 	SigSpec CD = st.sigCD;
@@ -248,8 +248,8 @@ void create_ice40_dsp(ice40_dsp_pm &pm)
 	cell->setParam(ID(BOTADDSUB_CARRYSELECT), Const(0, 2));
 
 	cell->setParam(ID(MODE_8x8), State::S0);
-	cell->setParam(ID(A_SIGNED), st.mul->getParam(ID(A_SIGNED)).as_bool());
-	cell->setParam(ID(B_SIGNED), st.mul->getParam(ID(B_SIGNED)).as_bool());
+	cell->setParam(ID(A_SIGNED), st.mul->parameters.at(ID(A_SIGNED), State::S0).as_bool());
+	cell->setParam(ID(B_SIGNED), st.mul->parameters.at(ID(B_SIGNED), State::S0).as_bool());
 
 	if (st.ffO) {
 		if (st.o_lo)
diff --git a/passes/pmgen/ice40_dsp.pmg b/passes/pmgen/ice40_dsp.pmg
index 6b6d2b56f..9d649cb98 100644
--- a/passes/pmgen/ice40_dsp.pmg
+++ b/passes/pmgen/ice40_dsp.pmg
@@ -56,11 +56,16 @@ code sigA sigB sigH
 			break;
 		sigH.append(O[i]);
 	}
+	// This sigM could have no users if downstream sinks (e.g. $add) is
+	//   narrower than $mul result, for example
+	if (i == 0)
+		reject;
+
 	log_assert(nusers(O.extract_end(i)) <= 1);
 endcode
 
 code argQ ffA ffAholdmux ffArstmux ffAholdpol ffArstpol sigA clock clock_pol
-	if (mul->type != \SB_MAC16 || !param(mul, \A_REG).as_bool()) {
+	if (mul->type != \SB_MAC16 || !param(mul, \A_REG, State::S0).as_bool()) {
 		argQ = sigA;
 		subpattern(in_dffe);
 		if (dff) {
@@ -81,7 +86,7 @@ code argQ ffA ffAholdmux ffArstmux ffAholdpol ffArstpol sigA clock clock_pol
 endcode
 
 code argQ ffB ffBholdmux ffBrstmux ffBholdpol ffBrstpol sigB clock clock_pol
-	if (mul->type != \SB_MAC16 || !param(mul, \B_REG).as_bool()) {
+	if (mul->type != \SB_MAC16 || !param(mul, \B_REG, State::S0).as_bool()) {
 		argQ = sigB;
 		subpattern(in_dffe);
 		if (dff) {
@@ -104,7 +109,7 @@ endcode
 code argD ffFJKG sigH clock clock_pol
 	if (nusers(sigH) == 2 &&
 			(mul->type != \SB_MAC16 ||
-			 (!param(mul, \TOP_8x8_MULT_REG).as_bool() && !param(mul, \BOT_8x8_MULT_REG).as_bool() && !param(mul, \PIPELINE_16x16_MULT_REG1).as_bool() && !param(mul, \PIPELINE_16x16_MULT_REG1).as_bool()))) {
+			 (!param(mul, \TOP_8x8_MULT_REG, State::S0).as_bool() && !param(mul, \BOT_8x8_MULT_REG, State::S0).as_bool() && !param(mul, \PIPELINE_16x16_MULT_REG1, State::S0).as_bool() && !param(mul, \PIPELINE_16x16_MULT_REG1, State::S0).as_bool()))) {
 		argD = sigH;
 		subpattern(out_dffe);
 		if (dff) {
@@ -143,7 +148,7 @@ endcode
 
 code argD ffH sigH sigO clock clock_pol
 	if (ffFJKG && nusers(sigH) == 2 &&
-			(mul->type != \SB_MAC16 || !param(mul, \PIPELINE_16x16_MULT_REG2).as_bool())) {
+			(mul->type != \SB_MAC16 || !param(mul, \PIPELINE_16x16_MULT_REG2, State::S0).as_bool())) {
 		argD = sigH;
 		subpattern(out_dffe);
 		if (dff) {
@@ -174,7 +179,7 @@ reject_ffH:		;
 endcode
 
 match add
-	if mul->type != \SB_MAC16 || (param(mul, \TOPOUTPUT_SELECT).as_int() == 3 && param(mul, \BOTOUTPUT_SELECT).as_int() == 3)
+	if mul->type != \SB_MAC16 || (param(mul, \TOPOUTPUT_SELECT, State::S0).as_int() == 3 && param(mul, \BOTOUTPUT_SELECT, State::S0).as_int() == 3)
 
 	select add->type.in($add)
 	choice <IdString> AB {\A, \B}
@@ -200,7 +205,7 @@ code sigCD sigO cd_signed
 		if ((actual_acc_width > actual_mul_width) && (natural_mul_width > actual_mul_width))
 			reject;
 		// If accumulator, check adder width and signedness
-		if (sigCD == sigH && (actual_acc_width != actual_mul_width) && (param(mul, \A_SIGNED).as_bool() != param(add, \A_SIGNED).as_bool()))
+		if (sigCD == sigH && (actual_acc_width != actual_mul_width) && (param(mul, \A_SIGNED, State::S0).as_bool() != param(add, \A_SIGNED).as_bool()))
 			reject;
 
 		sigO = port(add, \Y);
@@ -275,7 +280,7 @@ endcode
 
 code argQ ffCD ffCDholdmux ffCDholdpol ffCDrstpol sigCD clock clock_pol
 	if (!sigCD.empty() && sigCD != sigO &&
-			(mul->type != \SB_MAC16 || (!param(mul, \C_REG).as_bool() && !param(mul, \D_REG).as_bool()))) {
+			(mul->type != \SB_MAC16 || (!param(mul, \C_REG, State::S0).as_bool() && !param(mul, \D_REG, State::S0).as_bool()))) {
 		argQ = sigCD;
 		subpattern(in_dffe);
 		if (dff) {
@@ -328,6 +333,8 @@ arg argD argQ clock clock_pol
 
 code
 	dff = nullptr;
+	if (argQ.empty())
+		reject;
 	for (auto c : argQ.chunks()) {
 		if (!c.wire)
 			reject;
diff --git a/passes/pmgen/xilinx_dsp.pmg b/passes/pmgen/xilinx_dsp.pmg
index 5d3b9c2eb..af47ab111 100644
--- a/passes/pmgen/xilinx_dsp.pmg
+++ b/passes/pmgen/xilinx_dsp.pmg
@@ -120,7 +120,7 @@ endcode
 //      reset functionality, using a subpattern discussed above)
 //     If matched, treat 'A' input as input of ADREG
 code argQ ffAD ffADcemux ffADrstmux ffADcepol ffADrstpol sigA clock
-	if (param(dsp, \ADREG).as_int() == 0) {
+	if (param(dsp, \ADREG, 1).as_int() == 0) {
 		argQ = sigA;
 		subpattern(in_dffe);
 		if (dff) {
@@ -176,7 +176,7 @@ code argQ ffAD ffADcemux ffADrstmux ffADcepol ffADrstpol sigA clock ffA2 ffA2cem
 	// Only search for ffA2 if there was a pre-adder
 	//   (otherwise ffA2 would have been matched as ffAD)
 	if (preAdd) {
-		if (param(dsp, \AREG).as_int() == 0) {
+		if (param(dsp, \AREG, 1).as_int() == 0) {
 			argQ = sigA;
 			subpattern(in_dffe);
 			if (dff) {
@@ -237,7 +237,7 @@ endcode
 // (5) Match 'B' input for B2REG
 //     If B2REG, then match 'B' input for B1REG
 code argQ ffB2 ffB2cemux ffB2rstmux ffB2cepol ffBrstpol sigB clock ffB1 ffB1cemux ffB1rstmux ffB1cepol
-	if (param(dsp, \BREG).as_int() == 0) {
+	if (param(dsp, \BREG, 1).as_int() == 0) {
 		argQ = sigB;
 		subpattern(in_dffe);
 		if (dff) {
@@ -287,7 +287,7 @@ endcode
 
 // (6) Match 'D' input for DREG
 code argQ ffD ffDcemux ffDrstmux ffDcepol ffDrstpol sigD clock
-	if (param(dsp, \DREG).as_int() == 0) {
+	if (param(dsp, \DREG, 1).as_int() == 0) {
 		argQ = sigD;
 		subpattern(in_dffe);
 		if (dff) {
@@ -308,7 +308,7 @@ endcode
 
 // (7) Match 'P' output that exclusively drives an MREG
 code argD ffM ffMcemux ffMrstmux ffMcepol ffMrstpol sigM sigP clock
-	if (param(dsp, \MREG).as_int() == 0 && nusers(sigM) == 2) {
+	if (param(dsp, \MREG, 1).as_int() == 0 && nusers(sigM) == 2) {
 		argD = sigM;
 		subpattern(out_dffe);
 		if (dff) {
@@ -335,7 +335,7 @@ endcode
 //      recognised in xilinx_dsp.cc).
 match postAdd
 	// Ensure that Z mux is not already used
-	if port(dsp, \OPMODE, SigSpec()).extract(4,3).is_fully_zero()
+	if port(dsp, \OPMODE, SigSpec(0, 7)).extract(4,3).is_fully_zero()
 
 	select postAdd->type.in($add)
 	select GetSize(port(postAdd, \Y)) <= 48
@@ -363,7 +363,7 @@ endcode
 
 // (9) Match 'P' output that exclusively drives a PREG
 code argD ffP ffPcemux ffPrstmux ffPcepol ffPrstpol sigP clock
-	if (param(dsp, \PREG).as_int() == 0) {
+	if (param(dsp, \PREG, 1).as_int() == 0) {
 		int users = 2;
 		// If ffMcemux and no postAdd new-value net must have three users: ffMcemux, ffM and ffPcemux
 		if (ffMcemux && !postAdd) users++;
@@ -460,7 +460,7 @@ arg argD argQ clock
 
 code
 	dff = nullptr;
-	if (GetSize(argQ) == 0)
+	if (argQ.empty())
 		reject;
 	for (const auto &c : argQ.chunks()) {
 		// Abandon matches when 'Q' is a constant
diff --git a/passes/sat/Makefile.inc b/passes/sat/Makefile.inc
index fc3ac879e..4bb4b0edc 100644
--- a/passes/sat/Makefile.inc
+++ b/passes/sat/Makefile.inc
@@ -12,4 +12,5 @@ OBJS += passes/sat/supercover.o
 OBJS += passes/sat/fmcombine.o
 OBJS += passes/sat/mutate.o
 OBJS += passes/sat/cutpoint.o
+OBJS += passes/sat/fminit.o
 
diff --git a/passes/sat/fminit.cc b/passes/sat/fminit.cc
new file mode 100644
index 000000000..f3f00b382
--- /dev/null
+++ b/passes/sat/fminit.cc
@@ -0,0 +1,197 @@
+/*
+ *  yosys -- Yosys Open SYnthesis Suite
+ *
+ *  Copyright (C) 2012  Clifford Wolf <clifford@clifford.at>
+ *
+ *  Permission to use, copy, modify, and/or distribute this software for any
+ *  purpose with or without fee is hereby granted, provided that the above
+ *  copyright notice and this permission notice appear in all copies.
+ *
+ *  THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
+ *  WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
+ *  MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
+ *  ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
+ *  WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
+ *  ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
+ *  OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
+ *
+ */
+
+#include "kernel/yosys.h"
+#include "kernel/sigtools.h"
+
+USING_YOSYS_NAMESPACE
+PRIVATE_NAMESPACE_BEGIN
+
+struct FminitPass : public Pass {
+	FminitPass() : Pass("fminit", "set init values/sequences for formal") { }
+	void help() YS_OVERRIDE
+	{
+		//   |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
+		log("\n");
+		log("    fminit [options] <selection>\n");
+		log("\n");
+		log("This pass creates init constraints (for example for reset sequences) in a formal\n");
+		log("model.\n");
+		log("\n");
+		log("    -seq <signal> <sequence>\n");
+		log("        Set sequence using comma-separated list of values, use 'z for\n");
+		log("        unconstrained bits. The last value is used for the remainder of the\n");
+		log("        trace.\n");
+		log("\n");
+		log("    -set <signal> <value>\n");
+		log("        Add constant value constraint\n");
+		log("\n");
+		log("    -posedge <signal>\n");
+		log("    -negedge <signal>\n");
+		log("        Set clock for init sequences\n");
+		log("\n");
+	}
+	void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
+	{
+		vector<pair<string, vector<string>>> initdata;
+		vector<pair<string, string>> setdata;
+		string clocksignal;
+		bool clockedge;
+
+		log_header(design, "Executing FMINIT pass.\n");
+
+		size_t argidx;
+		for (argidx = 1; argidx < args.size(); argidx++)
+		{
+			// if (args[argidx] == "-o" && argidx+1 < args.size()) {
+			// 	filename = args[++argidx];
+			// 	continue;
+			// }
+			if (args[argidx] == "-seq" && argidx+2 < args.size()) {
+				string lhs = args[++argidx];
+				string rhs = args[++argidx];
+				initdata.push_back(make_pair(lhs, split_tokens(rhs, ",")));
+				continue;
+			}
+			if (args[argidx] == "-set" && argidx+2 < args.size()) {
+				string lhs = args[++argidx];
+				string rhs = args[++argidx];
+				setdata.push_back(make_pair(lhs, rhs));
+				continue;
+			}
+			if (args[argidx] == "-posedge" && argidx+1 < args.size()) {
+				clocksignal = args[++argidx];
+				clockedge = true;
+				continue;
+			}
+			if (args[argidx] == "-negedge" && argidx+1 < args.size()) {
+				clocksignal = args[++argidx];
+				clockedge = true;
+				continue;
+			}
+			break;
+		}
+		extra_args(args, argidx, design);
+
+		Module *module = nullptr;
+
+		for (auto mod : design->selected_modules()) {
+			if (module != nullptr)
+				log_error("'fminit' requires exactly one module to be selected.\n");
+			module = mod;
+		}
+
+		if (module == nullptr)
+			log_error("'fminit' requires exactly one module to be selected.\n");
+
+		SigSpec clksig;
+		if (!clocksignal.empty()) {
+			if (!SigSpec::parse(clksig, module, clocksignal))
+				log_error("Error parsing expression '%s'.\n", clocksignal.c_str());
+		}
+
+		for (auto &it : setdata)
+		{
+			SigSpec lhs, rhs;
+
+			if (!SigSpec::parse(lhs, module, it.first))
+				log_error("Error parsing expression '%s'.\n", it.first.c_str());
+
+			if (!SigSpec::parse_rhs(lhs, rhs, module, it.second))
+				log_error("Error parsing expression '%s'.\n", it.second.c_str());
+
+			SigSpec final_lhs, final_rhs;
+
+			for (int i = 0; i < GetSize(rhs); i++)
+				if (rhs[i] != State::Sz) {
+					final_lhs.append(lhs[i]);
+					final_rhs.append(rhs[i]);
+				}
+
+			if (!final_lhs.empty()) {
+				SigSpec eq = module->Eq(NEW_ID, final_lhs, final_rhs);
+				module->addAssume(NEW_ID, eq, State::S1);
+			}
+		}
+
+		vector<SigSpec> ctrlsig;
+		vector<SigSpec> ctrlsig_latched;
+
+		for (auto &it : initdata)
+		{
+			SigSpec lhs, rhs;
+
+			if (!SigSpec::parse(lhs, module, it.first))
+				log_error("Error parsing expression '%s'.\n", it.first.c_str());
+
+			for (int i = 0; i < GetSize(it.second); i++)
+			{
+				if (i >= GetSize(ctrlsig))
+				{
+					SigSpec insig = i > 0 ? ctrlsig.at(i-1) : State::S0;
+
+					Wire *outwire = module->addWire(NEW_ID);
+					outwire->attributes[ID(init)] = i > 0 ? State::S0 : State::S1;
+
+					if (clksig.empty())
+						module->addFf(NEW_ID, insig, outwire);
+					else
+						module->addDff(NEW_ID, clksig, insig, outwire, clockedge);
+
+					ctrlsig.push_back(outwire);
+					ctrlsig_latched.push_back(SigSpec());
+				}
+
+				if (i+1 == GetSize(it.second) && ctrlsig_latched[i].empty())
+				{
+					Wire *ffwire = module->addWire(NEW_ID);
+					ffwire->attributes[ID(init)] = State::S0;
+					SigSpec outsig = module->Or(NEW_ID, ffwire, ctrlsig[i]);
+
+					if (clksig.empty())
+						module->addFf(NEW_ID, outsig, ffwire);
+					else
+						module->addDff(NEW_ID, clksig, outsig, ffwire, clockedge);
+
+					ctrlsig_latched[i] = outsig;
+				}
+
+				SigSpec ctrl = i+1 == GetSize(it.second) ? ctrlsig_latched[i] : ctrlsig[i];
+
+				SigSpec final_lhs, final_rhs;
+
+				if (!SigSpec::parse_rhs(lhs, rhs, module, it.second[i]))
+					log_error("Error parsing expression '%s'.\n", it.second[i].c_str());
+
+				for (int i = 0; i < GetSize(rhs); i++)
+					if (rhs[i] != State::Sz) {
+						final_lhs.append(lhs[i]);
+						final_rhs.append(rhs[i]);
+					}
+
+				if (!final_lhs.empty()) {
+					SigSpec eq = module->Eq(NEW_ID, final_lhs, final_rhs);
+					module->addAssume(NEW_ID, eq, ctrl);
+				}
+			}
+		}
+	}
+} FminitPass;
+
+PRIVATE_NAMESPACE_END