X-Git-Url: https://git.libre-soc.org/?a=blobdiff_plain;f=passes%2Fsat%2Ffmcombine.cc;h=e15bdf6a83d8f9e04988f08a192dabe6a08b23fb;hb=8be09b5b24ad5f6a09bbc0bc675ac0be241672ca;hp=cd75ca8605579ded2d39f774afb2e848454268a5;hpb=03d1606b42110f8eac7311ac57c7334d1f781273;p=yosys.git

diff --git a/passes/sat/fmcombine.cc b/passes/sat/fmcombine.cc
index cd75ca860..e15bdf6a8 100644
--- a/passes/sat/fmcombine.cc
+++ b/passes/sat/fmcombine.cc
@@ -1,7 +1,7 @@
 /*
  *  yosys -- Yosys Open SYnthesis Suite
  *
- *  Copyright (C) 2012  Clifford Wolf <clifford@clifford.at>
+ *  Copyright (C) 2012  Claire Xenia Wolf <claire@yosyshq.com>
  *
  *  Permission to use, copy, modify, and/or distribute this software for any
  *  purpose with or without fee is hereby granted, provided that the above
@@ -26,6 +26,8 @@ PRIVATE_NAMESPACE_BEGIN
 
 struct opts_t
 {
+	bool initeq = false;
+	bool anyeq = false;
 	bool fwd = false;
 	bool bwd = false;
 	bool nop = false;
@@ -41,7 +43,7 @@ struct FmcombineWorker
 
 	FmcombineWorker(Design *design, IdString orig_type, const opts_t &opts) :
 			opts(opts), design(design), original(design->module(orig_type)),
-			orig_type(orig_type), combined_type("$fmcombine" + orig_type.str())
+			orig_type(orig_type), combined_type(stringf("$fmcombine%s", orig_type.c_str()))
 	{
 	}
 
@@ -56,7 +58,7 @@ struct FmcombineWorker
 		return newsig;
 	}
 
-	void import_prim_cell(Cell *cell, const string &suffix)
+	Cell *import_prim_cell(Cell *cell, const string &suffix)
 	{
 		Cell *c = module->addCell(cell->name.str() + suffix, cell->type);
 		c->parameters = cell->parameters;
@@ -64,6 +66,8 @@ struct FmcombineWorker
 
 		for (auto &conn : cell->connections())
 			c->setPort(conn.first, import_sig(conn.second, suffix));
+
+		return c;
 	}
 
 	void import_hier_cell(Cell *cell)
@@ -102,8 +106,23 @@ struct FmcombineWorker
 
 		for (auto cell : original->cells()) {
 			if (design->module(cell->type) == nullptr) {
-				import_prim_cell(cell, "_gold");
-				import_prim_cell(cell, "_gate");
+				if (opts.anyeq && cell->type.in(ID($anyseq), ID($anyconst))) {
+					Cell *gold = import_prim_cell(cell, "_gold");
+					for (auto &conn : cell->connections())
+						module->connect(import_sig(conn.second, "_gate"), gold->getPort(conn.first));
+				} else {
+					Cell *gold = import_prim_cell(cell, "_gold");
+					Cell *gate = import_prim_cell(cell, "_gate");
+					if (opts.initeq) {
+						if (RTLIL::builtin_ff_cell_types().count(cell->type)) {
+							SigSpec gold_q = gold->getPort(ID::Q);
+							SigSpec gate_q = gate->getPort(ID::Q);
+							SigSpec en = module->Initstate(NEW_ID);
+							SigSpec eq = module->Eq(NEW_ID, gold_q, gate_q);
+							module->addAssume(NEW_ID, eq, en);
+						}
+					}
+				}
 			} else {
 				import_hier_cell(cell);
 			}
@@ -215,7 +234,7 @@ struct FmcombineWorker
 
 struct FmcombinePass : public Pass {
 	FmcombinePass() : Pass("fmcombine", "combine two instances of a cell into one") { }
-	void help() YS_OVERRIDE
+	void help() override
 	{
 		//   |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
 		log("\n");
@@ -229,6 +248,13 @@ struct FmcombinePass : public Pass {
 		log("This is useful for formal test benches that check what differences in behavior\n");
 		log("a slight difference in input causes in a module.\n");
 		log("\n");
+		log("    -initeq\n");
+		log("        Insert assumptions that initially all FFs in both circuits have the\n");
+		log("        same initial values.\n");
+		log("\n");
+		log("    -anyeq\n");
+		log("        Do not duplicate $anyseq/$anyconst cells.\n");
+		log("\n");
 		log("    -fwd\n");
 		log("        Insert forward hint assumptions into the combined module.\n");
 		log("\n");
@@ -245,7 +271,7 @@ struct FmcombinePass : public Pass {
 		log("If none of -fwd, -bwd, and -nop is given, then -fwd is used as default.\n");
 		log("\n");
 	}
-	void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
+	void execute(std::vector<std::string> args, RTLIL::Design *design) override
 	{
 		opts_t opts;
 		Module *module = nullptr;
@@ -261,6 +287,14 @@ struct FmcombinePass : public Pass {
 			// 	filename = args[++argidx];
 			// 	continue;
 			// }
+			if (args[argidx] == "-initeq") {
+				opts.initeq = true;
+				continue;
+			}
+			if (args[argidx] == "-anyeq") {
+				opts.anyeq = true;
+				continue;
+			}
 			if (args[argidx] == "-fwd") {
 				opts.fwd = true;
 				continue;
@@ -297,7 +331,7 @@ struct FmcombinePass : public Pass {
 
 			gate_cell = module->cell(gate_name);
 			if (gate_cell == nullptr)
-				log_cmd_error("Gold cell %s not found in module %s.\n", log_id(gate_name), log_id(module));
+				log_cmd_error("Gate cell %s not found in module %s.\n", log_id(gate_name), log_id(module));
 		}
 		else
 		{
@@ -316,7 +350,7 @@ struct FmcombinePass : public Pass {
 		if (!gold_cell->parameters.empty())
 			log_cmd_error("Gold cell has unresolved instance parameters.\n");
 		if (!gate_cell->parameters.empty())
-			log_cmd_error("Gold cell has unresolved instance parameters.\n");
+			log_cmd_error("Gate cell has unresolved instance parameters.\n");
 
 		FmcombineWorker worker(design, gold_cell->type, opts);
 		worker.generate();
@@ -324,7 +358,7 @@ struct FmcombinePass : public Pass {
 
 		Cell *cell = module->addCell(combined_cell_name, worker.combined_type);
 		cell->attributes = gold_cell->attributes;
-		cell->add_strpool_attribute("\\src", gate_cell->get_strpool_attribute("\\src"));
+		cell->add_strpool_attribute(ID::src, gate_cell->get_strpool_attribute(ID::src));
 
 		log("Combining cells %s and %s in module %s into new cell %s.\n", log_id(gold_cell), log_id(gate_cell), log_id(module), log_id(cell));