summaryrefslogtreecommitdiff
path: root/passes/sat
diff options
context:
space:
mode:
Diffstat (limited to 'passes/sat')
-rw-r--r--passes/sat/assertpmux.cc6
-rw-r--r--passes/sat/cutpoint.cc2
-rw-r--r--passes/sat/expose.cc2
-rw-r--r--passes/sat/fmcombine.cc45
-rw-r--r--passes/sat/miter.cc8
-rw-r--r--passes/sat/mutate.cc32
-rw-r--r--passes/sat/sat.cc5
-rw-r--r--passes/sat/sim.cc5
8 files changed, 91 insertions, 14 deletions
diff --git a/passes/sat/assertpmux.cc b/passes/sat/assertpmux.cc
index 509cb0ba..3b432c46 100644
--- a/passes/sat/assertpmux.cc
+++ b/passes/sat/assertpmux.cc
@@ -180,7 +180,7 @@ struct AssertpmuxWorker
};
struct AssertpmuxPass : public Pass {
- AssertpmuxPass() : Pass("assertpmux", "convert internal signals to module ports") { }
+ AssertpmuxPass() : Pass("assertpmux", "adds asserts for parallel muxes") { }
void help() YS_OVERRIDE
{
// |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
@@ -195,8 +195,8 @@ struct AssertpmuxPass : public Pass {
log("\n");
log(" -always\n");
log(" usually the $pmux condition is only checked when the $pmux output\n");
- log(" is used be the mux tree it drives. this option will deactivate this\n");
- log(" additional constrained and check the $pmux condition always.\n");
+ log(" is used by the mux tree it drives. this option will deactivate this\n");
+ log(" additional constraint and check the $pmux condition always.\n");
log("\n");
}
void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
diff --git a/passes/sat/cutpoint.cc b/passes/sat/cutpoint.cc
index 048aec7f..b4549bc3 100644
--- a/passes/sat/cutpoint.cc
+++ b/passes/sat/cutpoint.cc
@@ -24,7 +24,7 @@ USING_YOSYS_NAMESPACE
PRIVATE_NAMESPACE_BEGIN
struct CutpointPass : public Pass {
- CutpointPass() : Pass("cutpoint", "add hi/lo cover cells for each wire bit") { }
+ CutpointPass() : Pass("cutpoint", "adds formal cut points to the design") { }
void help() YS_OVERRIDE
{
// |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
diff --git a/passes/sat/expose.cc b/passes/sat/expose.cc
index 80934548..71ce1683 100644
--- a/passes/sat/expose.cc
+++ b/passes/sat/expose.cc
@@ -508,7 +508,7 @@ struct ExposePass : public Pass {
}
for (auto &conn : module->connections_)
- conn.first = out_to_in_map(sigmap(conn.first));
+ conn.first = out_to_in_map(conn.first);
}
if (flag_cut)
diff --git a/passes/sat/fmcombine.cc b/passes/sat/fmcombine.cc
index cd75ca86..00c09854 100644
--- a/passes/sat/fmcombine.cc
+++ b/passes/sat/fmcombine.cc
@@ -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;
@@ -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,24 @@ 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("$anyseq", "$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 (cell->type.in("$ff", "$dff", "$dffe",
+ "$dffsr", "$adff", "$dlatch", "$dlatchsr")) {
+ SigSpec gold_q = gold->getPort("\\Q");
+ SigSpec gate_q = gate->getPort("\\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);
}
@@ -229,6 +249,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");
@@ -261,6 +288,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 +332,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 +351,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();
diff --git a/passes/sat/miter.cc b/passes/sat/miter.cc
index d37f1b12..1a886af7 100644
--- a/passes/sat/miter.cc
+++ b/passes/sat/miter.cc
@@ -254,7 +254,7 @@ void create_miter_equiv(struct Pass *that, std::vector<std::string> args, RTLIL:
if (flag_flatten) {
log_push();
- Pass::call_on_module(design, miter_module, "flatten; opt_expr -keepdc -undriven;;");
+ Pass::call_on_module(design, miter_module, "flatten -wb; opt_expr -keepdc -undriven;;");
log_pop();
}
}
@@ -308,7 +308,7 @@ void create_miter_assert(struct Pass *that, std::vector<std::string> args, RTLIL
if (flag_flatten) {
log_push();
- Pass::call_on_module(design, module, "flatten;;");
+ Pass::call_on_module(design, module, "flatten -wb;;");
log_pop();
}
@@ -385,7 +385,7 @@ struct MiterPass : public Pass {
log(" also create an 'assert' cell that checks if trigger is always low.\n");
log("\n");
log(" -flatten\n");
- log(" call 'flatten; opt_expr -keepdc -undriven;;' on the miter circuit.\n");
+ log(" call 'flatten -wb; opt_expr -keepdc -undriven;;' on the miter circuit.\n");
log("\n");
log("\n");
log(" miter -assert [options] module [miter_name]\n");
@@ -399,7 +399,7 @@ struct MiterPass : public Pass {
log(" keep module output ports.\n");
log("\n");
log(" -flatten\n");
- log(" call 'flatten; opt_expr -keepdc -undriven;;' on the miter circuit.\n");
+ log(" call 'flatten -wb; opt_expr -keepdc -undriven;;' on the miter circuit.\n");
log("\n");
}
void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
diff --git a/passes/sat/mutate.cc b/passes/sat/mutate.cc
index c50678c5..b53bbfeb 100644
--- a/passes/sat/mutate.cc
+++ b/passes/sat/mutate.cc
@@ -934,6 +934,32 @@ struct MutatePass : public Pass {
return;
}
+ if (opts.module.empty())
+ log_cmd_error("Missing -module argument.\n");
+
+ Module *module = design->module(opts.module);
+ if (module == nullptr)
+ log_cmd_error("Module %s not found.\n", log_id(opts.module));
+
+ if (opts.cell.empty())
+ log_cmd_error("Missing -cell argument.\n");
+
+ Cell *cell = module->cell(opts.cell);
+ if (cell == nullptr)
+ log_cmd_error("Cell %s not found in module %s.\n", log_id(opts.cell), log_id(opts.module));
+
+ if (opts.port.empty())
+ log_cmd_error("Missing -port argument.\n");
+
+ if (!cell->hasPort(opts.port))
+ log_cmd_error("Port %s not found on cell %s.%s.\n", log_id(opts.port), log_id(opts.module), log_id(opts.cell));
+
+ if (opts.portbit < 0)
+ log_cmd_error("Missing -portbit argument.\n");
+
+ if (GetSize(cell->getPort(opts.port)) <= opts.portbit)
+ log_cmd_error("Out-of-range -portbit argument for port %s on cell %s.%s.\n", log_id(opts.port), log_id(opts.module), log_id(opts.cell));
+
if (opts.mode == "inv") {
mutate_inv(design, opts);
return;
@@ -944,6 +970,12 @@ struct MutatePass : public Pass {
return;
}
+ if (opts.ctrlbit < 0)
+ log_cmd_error("Missing -ctrlbit argument.\n");
+
+ if (GetSize(cell->getPort(opts.port)) <= opts.ctrlbit)
+ log_cmd_error("Out-of-range -ctrlbit argument for port %s on cell %s.%s.\n", log_id(opts.port), log_id(opts.module), log_id(opts.cell));
+
if (opts.mode == "cnot0" || opts.mode == "cnot1") {
mutate_cnot(design, opts, opts.mode == "cnot1");
return;
diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc
index 695a03e1..e4654d83 100644
--- a/passes/sat/sat.cc
+++ b/passes/sat/sat.cc
@@ -659,6 +659,7 @@ struct SatHelper
void dump_model_to_vcd(std::string vcd_file_name)
{
+ rewrite_filename(vcd_file_name);
FILE *f = fopen(vcd_file_name.c_str(), "w");
if (!f)
log_cmd_error("Can't open output file `%s' for writing: %s\n", vcd_file_name.c_str(), strerror(errno));
@@ -761,6 +762,7 @@ struct SatHelper
void dump_model_to_json(std::string json_file_name)
{
+ rewrite_filename(json_file_name);
FILE *f = fopen(json_file_name.c_str(), "w");
if (!f)
log_cmd_error("Can't open output file `%s' for writing: %s\n", json_file_name.c_str(), strerror(errno));
@@ -1169,6 +1171,7 @@ struct SatPass : public Pass {
if (args[argidx] == "-tempinduct-def") {
tempinduct = true;
tempinduct_def = true;
+ enable_undef = true;
continue;
}
if (args[argidx] == "-tempinduct-baseonly") {
@@ -1504,6 +1507,7 @@ struct SatPass : public Pass {
{
if (!cnf_file_name.empty())
{
+ rewrite_filename(cnf_file_name);
FILE *f = fopen(cnf_file_name.c_str(), "w");
if (!f)
log_cmd_error("Can't open output file `%s' for writing: %s\n", cnf_file_name.c_str(), strerror(errno));
@@ -1607,6 +1611,7 @@ struct SatPass : public Pass {
if (!cnf_file_name.empty())
{
+ rewrite_filename(cnf_file_name);
FILE *f = fopen(cnf_file_name.c_str(), "w");
if (!f)
log_cmd_error("Can't open output file `%s' for writing: %s\n", cnf_file_name.c_str(), strerror(errno));
diff --git a/passes/sat/sim.cc b/passes/sat/sim.cc
index 53e248ad..4c3022c7 100644
--- a/passes/sat/sim.cc
+++ b/passes/sat/sim.cc
@@ -88,6 +88,8 @@ struct SimInstance
SimInstance(SimShared *shared, Module *module, Cell *instance = nullptr, SimInstance *parent = nullptr) :
shared(shared), module(module), instance(instance), parent(parent), sigmap(module)
{
+ log_assert(module);
+
if (parent) {
log_assert(parent->children.count(instance) == 0);
parent->children[instance] = this;
@@ -848,6 +850,9 @@ struct SimPass : public Pass {
if (design->full_selection()) {
top_mod = design->top_module();
+
+ if (!top_mod)
+ log_cmd_error("Design has no top module, use the 'hierarchy' command to specify one.\n");
} else {
auto mods = design->selected_whole_modules();
if (GetSize(mods) != 1)
generated by cgit v1.2.3 (git 2.25.1) at 2024-05-01 07:28:39 +0000