aboutsummaryrefslogtreecommitdiffstats
path: root/passes
diff options
context:
space:
mode:
Diffstat (limited to 'passes')
-rw-r--r--passes/cmds/select.cc2
-rw-r--r--passes/cmds/stat.cc156
-rw-r--r--passes/equiv/equiv_make.cc93
-rw-r--r--passes/equiv/equiv_opt.cc14
-rw-r--r--passes/fsm/fsm.cc9
-rw-r--r--passes/fsm/fsm_detect.cc9
-rw-r--r--passes/hierarchy/hierarchy.cc2
-rw-r--r--passes/opt/opt_expr.cc2
-rw-r--r--passes/sat/clk2fflogic.cc190
-rw-r--r--passes/sat/miter.cc36
-rw-r--r--passes/sat/mutate.cc2
-rw-r--r--passes/sat/sat.cc29
-rw-r--r--passes/sat/sim.cc25
-rw-r--r--passes/techmap/flowmap.cc3
14 files changed, 296 insertions, 276 deletions
diff --git a/passes/cmds/select.cc b/passes/cmds/select.cc
index fdf56641c..03d00816e 100644
--- a/passes/cmds/select.cc
+++ b/passes/cmds/select.cc
@@ -1607,12 +1607,14 @@ struct CdPass : public Pass {
log("with the specified name in the current module, then this is equivalent\n");
log("to 'cd <celltype>'.\n");
log("\n");
+ log("\n");
log(" cd ..\n");
log("\n");
log("Remove trailing substrings that start with '.' in current module name until\n");
log("the name of a module in the current design is generated, then switch to that\n");
log("module. Otherwise clear the current selection.\n");
log("\n");
+ log("\n");
log(" cd\n");
log("\n");
log("This is just a shortcut for 'select -clear'.\n");
diff --git a/passes/cmds/stat.cc b/passes/cmds/stat.cc
index a4984597d..a998ab8e7 100644
--- a/passes/cmds/stat.cc
+++ b/passes/cmds/stat.cc
@@ -149,6 +149,78 @@ struct statdata_t
}
}
+ unsigned int estimate_xilinx_lc()
+ {
+ unsigned int lut6_cnt = num_cells_by_type[ID(LUT6)];
+ unsigned int lut5_cnt = num_cells_by_type[ID(LUT5)];
+ unsigned int lut4_cnt = num_cells_by_type[ID(LUT4)];
+ unsigned int lut3_cnt = num_cells_by_type[ID(LUT3)];
+ unsigned int lut2_cnt = num_cells_by_type[ID(LUT2)];
+ unsigned int lut1_cnt = num_cells_by_type[ID(LUT1)];
+ unsigned int lc_cnt = 0;
+
+ lc_cnt += lut6_cnt;
+
+ lc_cnt += lut5_cnt;
+ if (lut1_cnt) {
+ int cnt = std::min(lut5_cnt, lut1_cnt);
+ lut5_cnt -= cnt;
+ lut1_cnt -= cnt;
+ }
+
+ lc_cnt += lut4_cnt;
+ if (lut1_cnt) {
+ int cnt = std::min(lut4_cnt, lut1_cnt);
+ lut4_cnt -= cnt;
+ lut1_cnt -= cnt;
+ }
+ if (lut2_cnt) {
+ int cnt = std::min(lut4_cnt, lut2_cnt);
+ lut4_cnt -= cnt;
+ lut2_cnt -= cnt;
+ }
+
+ lc_cnt += lut3_cnt;
+ if (lut1_cnt) {
+ int cnt = std::min(lut3_cnt, lut1_cnt);
+ lut3_cnt -= cnt;
+ lut1_cnt -= cnt;
+ }
+ if (lut2_cnt) {
+ int cnt = std::min(lut3_cnt, lut2_cnt);
+ lut3_cnt -= cnt;
+ lut2_cnt -= cnt;
+ }
+ if (lut3_cnt) {
+ int cnt = (lut3_cnt + 1) / 2;
+ lut3_cnt -= cnt;
+ }
+
+ lc_cnt += (lut2_cnt + lut1_cnt + 1) / 2;
+
+ return lc_cnt;
+ }
+
+ unsigned int cmos_transistor_count(bool *tran_cnt_exact)
+ {
+ unsigned int tran_cnt = 0;
+ auto &gate_costs = CellCosts::cmos_gate_cost();
+
+ for (auto it : num_cells_by_type) {
+ auto ctype = it.first;
+ auto cnum = it.second;
+
+ if (gate_costs.count(ctype))
+ tran_cnt += cnum * gate_costs.at(ctype);
+ else if (ctype.in(ID($_DFF_P_), ID($_DFF_N_)))
+ tran_cnt += cnum * 16;
+ else
+ *tran_cnt_exact = false;
+ }
+
+ return tran_cnt;
+ }
+
void log_data(RTLIL::IdString mod_name, bool top_mod)
{
log(" Number of wires: %6u\n", num_wires);
@@ -176,74 +248,14 @@ struct statdata_t
if (tech == "xilinx")
{
- unsigned int lut6_cnt = num_cells_by_type[ID(LUT6)];
- unsigned int lut5_cnt = num_cells_by_type[ID(LUT5)];
- unsigned int lut4_cnt = num_cells_by_type[ID(LUT4)];
- unsigned int lut3_cnt = num_cells_by_type[ID(LUT3)];
- unsigned int lut2_cnt = num_cells_by_type[ID(LUT2)];
- unsigned int lut1_cnt = num_cells_by_type[ID(LUT1)];
- unsigned int lc_cnt = 0;
-
- lc_cnt += lut6_cnt;
-
- lc_cnt += lut5_cnt;
- if (lut1_cnt) {
- int cnt = std::min(lut5_cnt, lut1_cnt);
- lut5_cnt -= cnt;
- lut1_cnt -= cnt;
- }
-
- lc_cnt += lut4_cnt;
- if (lut1_cnt) {
- int cnt = std::min(lut4_cnt, lut1_cnt);
- lut4_cnt -= cnt;
- lut1_cnt -= cnt;
- }
- if (lut2_cnt) {
- int cnt = std::min(lut4_cnt, lut2_cnt);
- lut4_cnt -= cnt;
- lut2_cnt -= cnt;
- }
-
- lc_cnt += lut3_cnt;
- if (lut1_cnt) {
- int cnt = std::min(lut3_cnt, lut1_cnt);
- lut3_cnt -= cnt;
- lut1_cnt -= cnt;
- }
- if (lut2_cnt) {
- int cnt = std::min(lut3_cnt, lut2_cnt);
- lut3_cnt -= cnt;
- lut2_cnt -= cnt;
- }
- if (lut3_cnt) {
- int cnt = (lut3_cnt + 1) / 2;
- lut3_cnt -= cnt;
- }
-
- lc_cnt += (lut2_cnt + lut1_cnt + 1) / 2;
-
log("\n");
- log(" Estimated number of LCs: %10u\n", lc_cnt);
+ log(" Estimated number of LCs: %10u\n", estimate_xilinx_lc());
}
if (tech == "cmos")
{
- unsigned int tran_cnt = 0;
bool tran_cnt_exact = true;
- auto &gate_costs = CellCosts::cmos_gate_cost();
-
- for (auto it : num_cells_by_type) {
- auto ctype = it.first;
- auto cnum = it.second;
-
- if (gate_costs.count(ctype))
- tran_cnt += cnum * gate_costs.at(ctype);
- else if (ctype.in(ID($_DFF_P_), ID($_DFF_N_)))
- tran_cnt += cnum * 16;
- else
- tran_cnt_exact = false;
- }
+ unsigned int tran_cnt = cmos_transistor_count(&tran_cnt_exact);
log("\n");
log(" Estimated number of transistors: %10u%s\n", tran_cnt, tran_cnt_exact ? "" : "+");
@@ -273,7 +285,20 @@ struct statdata_t
first_line = false;
}
log("\n");
- log(" }\n");
+ log(" }");
+ if (tech == "xilinx")
+ {
+ log(",\n");
+ log(" \"estimated_num_lc\": %u", estimate_xilinx_lc());
+ }
+ if (tech == "cmos")
+ {
+ bool tran_cnt_exact = true;
+ unsigned int tran_cnt = cmos_transistor_count(&tran_cnt_exact);
+ log(",\n");
+ log(" \"estimated_num_transistors\": \"%u%s\"", tran_cnt, tran_cnt_exact ? "" : "+");
+ }
+ log("\n");
log(" }");
}
};
@@ -352,8 +377,6 @@ struct StatPass : public Pass {
}
void execute(std::vector<std::string> args, RTLIL::Design *design) override
{
- log_header(design, "Printing statistics.\n");
-
bool width_mode = false, json_mode = false;
RTLIL::Module *top_mod = nullptr;
std::map<RTLIL::IdString, statdata_t> mod_stat;
@@ -391,6 +414,9 @@ struct StatPass : public Pass {
}
extra_args(args, argidx, design);
+ if(!json_mode)
+ log_header(design, "Printing statistics.\n");
+
if (techname != "" && techname != "xilinx" && techname != "cmos" && !json_mode)
log_cmd_error("Unsupported technology: '%s'\n", techname.c_str());
diff --git a/passes/equiv/equiv_make.cc b/passes/equiv/equiv_make.cc
index 7ef2827bf..27cec7549 100644
--- a/passes/equiv/equiv_make.cc
+++ b/passes/equiv/equiv_make.cc
@@ -40,16 +40,6 @@ struct EquivMakeWorker
pool<SigBit> undriven_bits;
SigMap assign_map;
- dict<SigBit, pool<Cell*>> bit2driven; // map: bit <--> and its driven cells
-
- CellTypes comb_ct;
-
- EquivMakeWorker()
- {
- comb_ct.setup_internals();
- comb_ct.setup_stdcells();
- }
-
void read_blacklists()
{
for (auto fn : blacklists)
@@ -147,6 +137,7 @@ struct EquivMakeWorker
{
SigMap assign_map(equiv_mod);
SigMap rd_signal_map;
+ SigPool primary_inputs;
// list of cells without added $equiv cells
auto cells_list = equiv_mod->cells().to_vector();
@@ -262,6 +253,9 @@ struct EquivMakeWorker
gate_wire->port_input = false;
equiv_mod->connect(gold_wire, wire);
equiv_mod->connect(gate_wire, wire);
+ primary_inputs.add(assign_map(gold_wire));
+ primary_inputs.add(assign_map(gate_wire));
+ primary_inputs.add(wire);
}
else
{
@@ -288,31 +282,19 @@ struct EquivMakeWorker
}
}
- init_bit2driven();
-
- pool<Cell*> visited_cells;
for (auto c : cells_list)
for (auto &conn : c->connections())
if (!ct.cell_output(c->type, conn.first)) {
SigSpec old_sig = assign_map(conn.second);
SigSpec new_sig = rd_signal_map(old_sig);
-
- if(old_sig != new_sig) {
- SigSpec tmp_sig = old_sig;
- for (int i = 0; i < GetSize(old_sig); i++) {
- SigBit old_bit = old_sig[i], new_bit = new_sig[i];
-
- visited_cells.clear();
- if (check_signal_in_fanout(visited_cells, old_bit, new_bit))
- continue;
-
- log("Changing input %s of cell %s (%s): %s -> %s\n",
- log_id(conn.first), log_id(c), log_id(c->type),
- log_signal(old_bit), log_signal(new_bit));
-
- tmp_sig[i] = new_bit;
- }
- c->setPort(conn.first, tmp_sig);
+ for (int i = 0; i < GetSize(old_sig); i++)
+ if (primary_inputs.check(old_sig[i]))
+ new_sig[i] = old_sig[i];
+ if (old_sig != new_sig) {
+ log("Changing input %s of cell %s (%s): %s -> %s\n",
+ log_id(conn.first), log_id(c), log_id(c->type),
+ log_signal(old_sig), log_signal(new_sig));
+ c->setPort(conn.first, new_sig);
}
}
@@ -403,57 +385,6 @@ struct EquivMakeWorker
}
}
- void init_bit2driven()
- {
- for (auto cell : equiv_mod->cells()) {
- if (!ct.cell_known(cell->type) && !cell->type.in(ID($dff), ID($_DFF_P_), ID($_DFF_N_), ID($ff), ID($_FF_)))
- continue;
- for (auto &conn : cell->connections())
- {
- if (yosys_celltypes.cell_input(cell->type, conn.first))
- for (auto bit : assign_map(conn.second))
- {
- bit2driven[bit].insert(cell);
- }
- }
- }
- }
-
- bool check_signal_in_fanout(pool<Cell*> & visited_cells, SigBit source_bit, SigBit target_bit)
- {
- if (source_bit == target_bit)
- return true;
-
- if (bit2driven.count(source_bit) == 0)
- return false;
-
- auto driven_cells = bit2driven.at(source_bit);
- for (auto driven_cell: driven_cells)
- {
- bool is_comb = comb_ct.cell_known(driven_cell->type);
- if (!is_comb)
- continue;
-
- if (visited_cells.count(driven_cell) > 0)
- continue;
- visited_cells.insert(driven_cell);
-
- for (auto &conn: driven_cell->connections())
- {
- if (yosys_celltypes.cell_input(driven_cell->type, conn.first))
- continue;
-
- for (auto bit: conn.second) {
- bool is_in_fanout = check_signal_in_fanout(visited_cells, bit, target_bit);
- if (is_in_fanout == true)
- return true;
- }
- }
- }
-
- return false;
- }
-
void run()
{
copy_to_equiv();
diff --git a/passes/equiv/equiv_opt.cc b/passes/equiv/equiv_opt.cc
index 4d0400448..f5eb75730 100644
--- a/passes/equiv/equiv_opt.cc
+++ b/passes/equiv/equiv_opt.cc
@@ -60,13 +60,16 @@ struct EquivOptPass:public ScriptPass
log(" -undef\n");
log(" enable modelling of undef states during equiv_induct.\n");
log("\n");
+ log(" -nocheck\n");
+ log(" disable running check before and after the command under test.\n");
+ log("\n");
log("The following commands are executed by this verification command:\n");
help_script();
log("\n");
}
std::string command, techmap_opts, make_opts;
- bool assert, undef, multiclock, async2sync;
+ bool assert, undef, multiclock, async2sync, nocheck;
void clear_flags() override
{
@@ -77,6 +80,7 @@ struct EquivOptPass:public ScriptPass
undef = false;
multiclock = false;
async2sync = false;
+ nocheck = false;
}
void execute(std::vector < std::string > args, RTLIL::Design * design) override
@@ -110,6 +114,10 @@ struct EquivOptPass:public ScriptPass
undef = true;
continue;
}
+ if (args[argidx] == "-nocheck") {
+ nocheck = true;
+ continue;
+ }
if (args[argidx] == "-multiclock") {
multiclock = true;
continue;
@@ -153,10 +161,14 @@ struct EquivOptPass:public ScriptPass
if (check_label("run_pass")) {
run("hierarchy -auto-top");
run("design -save preopt");
+ if (!nocheck)
+ run("check -assert", "(unless -nocheck)");
if (help_mode)
run("[command]");
else
run(command);
+ if (!nocheck)
+ run("check -assert", "(unless -nocheck)");
run("design -stash postopt");
}
diff --git a/passes/fsm/fsm.cc b/passes/fsm/fsm.cc
index 0c5e624dc..8e7e09d4c 100644
--- a/passes/fsm/fsm.cc
+++ b/passes/fsm/fsm.cc
@@ -67,6 +67,15 @@ struct FsmPass : public Pass {
log(" -encfile file\n");
log(" passed through to fsm_recode pass\n");
log("\n");
+ log("This pass uses a subset of FF types to detect FSMs. Run 'opt -nosdff -nodffe'\n");
+ log("before this pass to prepare the design.\n");
+ log("\n");
+#ifdef YOSYS_ENABLE_VERIFIC
+ log("The Verific frontend may merge multiplexers in a way that interferes with FSM\n");
+ log("detection. Run 'verific -cfg db_infer_wide_muxes_post_elaboration 0' before\n");
+ log("reading the source, and 'bmuxmap' after 'proc' for best results.\n");
+ log("\n");
+#endif
}
void execute(std::vector<std::string> args, RTLIL::Design *design) override
{
diff --git a/passes/fsm/fsm_detect.cc b/passes/fsm/fsm_detect.cc
index f829714c4..5378ec89e 100644
--- a/passes/fsm/fsm_detect.cc
+++ b/passes/fsm/fsm_detect.cc
@@ -272,6 +272,15 @@ struct FsmDetectPass : public Pass {
log("Signals can be protected from being detected by this pass by setting the\n");
log("'fsm_encoding' attribute to \"none\".\n");
log("\n");
+ log("This pass uses a subset of FF types to detect FSMs. Run 'opt -nosdff -nodffe'\n");
+ log("before this pass to prepare the design for fsm_detect.\n");
+ log("\n");
+#ifdef YOSYS_ENABLE_VERIFIC
+ log("The Verific frontend may merge multiplexers in a way that interferes with FSM\n");
+ log("detection. Run 'verific -cfg db_infer_wide_muxes_post_elaboration 0' before\n");
+ log("reading the source, and 'bmuxmap' after 'proc' for best results.\n");
+ log("\n");
+#endif
}
void execute(std::vector<std::string> args, RTLIL::Design *design) override
{
diff --git a/passes/hierarchy/hierarchy.cc b/passes/hierarchy/hierarchy.cc
index eea6abb04..bf0137503 100644
--- a/passes/hierarchy/hierarchy.cc
+++ b/passes/hierarchy/hierarchy.cc
@@ -960,7 +960,7 @@ struct HierarchyPass : public Pass {
if (top_mod == nullptr && !load_top_mod.empty()) {
#ifdef YOSYS_ENABLE_VERIFIC
if (verific_import_pending) {
- verific_import(design, parameters, load_top_mod);
+ load_top_mod = verific_import(design, parameters, load_top_mod);
top_mod = design->module(RTLIL::escape_id(load_top_mod));
}
#endif
diff --git a/passes/opt/opt_expr.cc b/passes/opt/opt_expr.cc
index be0cd470b..9cc0170dc 100644
--- a/passes/opt/opt_expr.cc
+++ b/passes/opt/opt_expr.cc
@@ -1494,7 +1494,7 @@ skip_identity:
RTLIL::SigSpec input = assign_map(cell->getPort(ID::S));
RTLIL::SigSpec inA = assign_map(cell->getPort(ID::A));
RTLIL::SigSpec inB = assign_map(cell->getPort(ID::B));
- if (input.is_fully_const())
+ if (input.is_fully_const() && (!keepdc || input.is_fully_def()))
ACTION_DO(ID::Y, input.as_bool() ? cell->getPort(ID::B) : cell->getPort(ID::A));
else if (inA == inB)
ACTION_DO(ID::Y, cell->getPort(ID::A));
diff --git a/passes/sat/clk2fflogic.cc b/passes/sat/clk2fflogic.cc
index 2384ffced..bba2cbbec 100644
--- a/passes/sat/clk2fflogic.cc
+++ b/passes/sat/clk2fflogic.cc
@@ -26,6 +26,11 @@
USING_YOSYS_NAMESPACE
PRIVATE_NAMESPACE_BEGIN
+struct SampledSig {
+ SigSpec sampled, current;
+ SigSpec &operator[](bool get_current) { return get_current ? current : sampled; }
+};
+
struct Clk2fflogicPass : public Pass {
Clk2fflogicPass() : Pass("clk2fflogic", "convert clocked FFs to generic $ff cells") { }
void help() override
@@ -38,37 +43,65 @@ struct Clk2fflogicPass : public Pass {
log("implicit global clock. This is useful for formal verification of designs with\n");
log("multiple clocks.\n");
log("\n");
+ log("This pass assumes negative hold time for the async FF inputs. For example when\n");
+ log("a reset deasserts with the clock edge, then the FF output will still drive the\n");
+ log("reset value in the next cycle regardless of the data-in value at the time of\n");
+ log("the clock edge.\n");
+ log("\n");
}
- SigSpec wrap_async_control(Module *module, SigSpec sig, bool polarity, bool is_fine, IdString past_sig_id) {
- if (!is_fine)
- return wrap_async_control(module, sig, polarity, past_sig_id);
- return wrap_async_control_gate(module, sig, polarity, past_sig_id);
+ // Active-high sampled and current value of a level-triggered control signal. Initial sampled values is low/non-asserted.
+ SampledSig sample_control(Module *module, SigSpec sig, bool polarity, bool is_fine) {
+ if (!polarity) {
+ if (is_fine)
+ sig = module->NotGate(NEW_ID, sig);
+ else
+ sig = module->Not(NEW_ID, sig);
+ }
+ std::string sig_str = log_signal(sig);
+ sig_str.erase(std::remove(sig_str.begin(), sig_str.end(), ' '), sig_str.end());
+ Wire *sampled_sig = module->addWire(NEW_ID_SUFFIX(stringf("%s#sampled", sig_str.c_str())), GetSize(sig));
+ sampled_sig->attributes[ID::init] = RTLIL::Const(State::S0, GetSize(sig));
+ if (is_fine)
+ module->addFfGate(NEW_ID, sig, sampled_sig);
+ else
+ module->addFf(NEW_ID, sig, sampled_sig);
+ return {sampled_sig, sig};
}
- SigSpec wrap_async_control(Module *module, SigSpec sig, bool polarity, IdString past_sig_id) {
- Wire *past_sig = module->addWire(past_sig_id, GetSize(sig));
- past_sig->attributes[ID::init] = RTLIL::Const(polarity ? State::S0 : State::S1, GetSize(sig));
- module->addFf(NEW_ID, sig, past_sig);
- if (polarity)
- sig = module->Or(NEW_ID, sig, past_sig);
+ // Active-high trigger signal for an edge-triggered control signal. Initial values is low/non-edge.
+ SigSpec sample_control_edge(Module *module, SigSpec sig, bool polarity, bool is_fine) {
+ std::string sig_str = log_signal(sig);
+ sig_str.erase(std::remove(sig_str.begin(), sig_str.end(), ' '), sig_str.end());
+ Wire *sampled_sig = module->addWire(NEW_ID_SUFFIX(stringf("%s#sampled", sig_str.c_str())), GetSize(sig));
+ sampled_sig->attributes[ID::init] = RTLIL::Const(polarity ? State::S1 : State::S0, GetSize(sig));
+ if (is_fine)
+ module->addFfGate(NEW_ID, sig, sampled_sig);
else
- sig = module->And(NEW_ID, sig, past_sig);
- if (polarity)
- return sig;
+ module->addFf(NEW_ID, sig, sampled_sig);
+ return module->Eqx(NEW_ID, {sampled_sig, sig}, polarity ? SigSpec {State::S0, State::S1} : SigSpec {State::S1, State::S0});
+ }
+ // Sampled and current value of a data signal.
+ SampledSig sample_data(Module *module, SigSpec sig, RTLIL::Const init, bool is_fine) {
+ std::string sig_str = log_signal(sig);
+ sig_str.erase(std::remove(sig_str.begin(), sig_str.end(), ' '), sig_str.end());
+ Wire *sampled_sig = module->addWire(NEW_ID_SUFFIX(stringf("%s#sampled", sig_str.c_str())), GetSize(sig));
+ sampled_sig->attributes[ID::init] = init;
+ if (is_fine)
+ module->addFfGate(NEW_ID, sig, sampled_sig);
else
- return module->Not(NEW_ID, sig);
+ module->addFf(NEW_ID, sig, sampled_sig);
+ return {sampled_sig, sig};
}
- SigSpec wrap_async_control_gate(Module *module, SigSpec sig, bool polarity, IdString past_sig_id) {
- Wire *past_sig = module->addWire(past_sig_id);
- past_sig->attributes[ID::init] = polarity ? State::S0 : State::S1;
- module->addFfGate(NEW_ID, sig, past_sig);
- if (polarity)
- sig = module->OrGate(NEW_ID, sig, past_sig);
+ SigSpec mux(Module *module, SigSpec a, SigSpec b, SigSpec s, bool is_fine) {
+ if (is_fine)
+ return module->MuxGate(NEW_ID, a, b, s);
else
- sig = module->AndGate(NEW_ID, sig, past_sig);
- if (polarity)
- return sig;
+ return module->Mux(NEW_ID, a, b, s);
+ }
+ SigSpec bitwise_sr(Module *module, SigSpec a, SigSpec s, SigSpec r, bool is_fine) {
+ if (is_fine)
+ return module->AndGate(NEW_ID, module->OrGate(NEW_ID, a, s), module->NotGate(NEW_ID, r));
else
- return module->NotGate(NEW_ID, sig);
+ return module->And(NEW_ID, module->Or(NEW_ID, a, s), module->Not(NEW_ID, r));
}
void execute(std::vector<std::string> args, RTLIL::Design *design) override
{
@@ -177,96 +210,47 @@ struct Clk2fflogicPass : public Pass {
ff.remove();
- // Strip spaces from signal name, since Yosys IDs can't contain spaces
- // Spaces only occur when we have a signal that's a slice of a larger bus,
- // e.g. "\myreg [5:0]", so removing spaces shouldn't result in loss of uniqueness
- std::string sig_q_str = log_signal(ff.sig_q);
- sig_q_str.erase(std::remove(sig_q_str.begin(), sig_q_str.end(), ' '), sig_q_str.end());
-
- Wire *past_q = module->addWire(NEW_ID_SUFFIX(stringf("%s#past_q_wire", sig_q_str.c_str())), ff.width);
-
- if (!ff.is_fine) {
- module->addFf(NEW_ID, ff.sig_q, past_q);
- } else {
- module->addFfGate(NEW_ID, ff.sig_q, past_q);
- }
- if (!ff.val_init.is_fully_undef())
- initvals.set_init(past_q, ff.val_init);
-
- if (ff.has_clk) {
+ if (ff.has_clk)
ff.unmap_ce_srst();
- Wire *past_clk = module->addWire(NEW_ID_SUFFIX(stringf("%s#past_clk#%s", sig_q_str.c_str(), log_signal(ff.sig_clk))));
- initvals.set_init(past_clk, ff.pol_clk ? State::S1 : State::S0);
-
- if (!ff.is_fine)
- module->addFf(NEW_ID, ff.sig_clk, past_clk);
- else
- module->addFfGate(NEW_ID, ff.sig_clk, past_clk);
+ auto next_q = sample_data(module, ff.sig_q, ff.val_init, ff.is_fine).sampled;
- SigSpec clock_edge_pattern;
-
- if (ff.pol_clk) {
- clock_edge_pattern.append(State::S0);
- clock_edge_pattern.append(State::S1);
- } else {
- clock_edge_pattern.append(State::S1);
- clock_edge_pattern.append(State::S0);
- }
-
- SigSpec clock_edge = module->Eqx(NEW_ID, {ff.sig_clk, SigSpec(past_clk)}, clock_edge_pattern);
-
- Wire *past_d = module->addWire(NEW_ID_SUFFIX(stringf("%s#past_d_wire", sig_q_str.c_str())), ff.width);
- if (!ff.is_fine)
- module->addFf(NEW_ID, ff.sig_d, past_d);
- else
- module->addFfGate(NEW_ID, ff.sig_d, past_d);
-
- if (!ff.val_init.is_fully_undef())
- initvals.set_init(past_d, ff.val_init);
-
- if (!ff.is_fine)
- qval = module->Mux(NEW_ID, past_q, past_d, clock_edge);
- else
- qval = module->MuxGate(NEW_ID, past_q, past_d, clock_edge);
- } else {
- qval = past_q;
+ if (ff.has_clk) {
+ // The init value for the sampled d is never used, so we can set it to fixed zero, reducing uninit'd FFs
+ auto sampled_d = sample_data(module, ff.sig_d, RTLIL::Const(State::S0, ff.width), ff.is_fine);
+ auto clk_edge = sample_control_edge(module, ff.sig_clk, ff.pol_clk, ff.is_fine);
+ next_q = mux(module, next_q, sampled_d.sampled, clk_edge, ff.is_fine);
}
+ SampledSig sampled_aload, sampled_ad, sampled_set, sampled_clr, sampled_arst;
// The check for a constant sig_aload is also done by opt_dff, but when using verific and running
// clk2fflogic before opt_dff (which does more and possibly unwanted optimizations) this check avoids
// generating a lot of extra logic.
- if (ff.has_aload && ff.sig_aload != (ff.pol_aload ? State::S0 : State::S1)) {
- SigSpec sig_aload = wrap_async_control(module, ff.sig_aload, ff.pol_aload, ff.is_fine, NEW_ID);
-
- if (!ff.is_fine)
- qval = module->Mux(NEW_ID, qval, ff.sig_ad, sig_aload);
- else
- qval = module->MuxGate(NEW_ID, qval, ff.sig_ad, sig_aload);
+ bool has_nonconst_aload = ff.has_aload && ff.sig_aload != (ff.pol_aload ? State::S0 : State::S1);
+ if (has_nonconst_aload) {
+ sampled_aload = sample_control(module, ff.sig_aload, ff.pol_aload, ff.is_fine);
+ // The init value for the sampled ad is never used, so we can set it to fixed zero, reducing uninit'd FFs
+ sampled_ad = sample_data(module, ff.sig_ad, RTLIL::Const(State::S0, ff.width), ff.is_fine);
}
-
if (ff.has_sr) {
- SigSpec setval = wrap_async_control(module, ff.sig_set, ff.pol_set, ff.is_fine, NEW_ID);
- SigSpec clrval = wrap_async_control(module, ff.sig_clr, ff.pol_clr, ff.is_fine, NEW_ID);
- if (!ff.is_fine) {
- clrval = module->Not(NEW_ID, clrval);
- qval = module->Or(NEW_ID, qval, setval);
- module->addAnd(NEW_ID, qval, clrval, ff.sig_q);
- } else {
- clrval = module->NotGate(NEW_ID, clrval);
- qval = module->OrGate(NEW_ID, qval, setval);
- module->addAndGate(NEW_ID, qval, clrval, ff.sig_q);
- }
- } else if (ff.has_arst) {
- IdString id = NEW_ID_SUFFIX(stringf("%s#past_arst#%s", sig_q_str.c_str(), log_signal(ff.sig_arst)));
- SigSpec arst = wrap_async_control(module, ff.sig_arst, ff.pol_arst, ff.is_fine, id);
- if (!ff.is_fine)
- module->addMux(NEW_ID, qval, ff.val_arst, arst, ff.sig_q);
- else
- module->addMuxGate(NEW_ID, qval, ff.val_arst[0], arst, ff.sig_q);
- } else {
- module->connect(ff.sig_q, qval);
+ sampled_set = sample_control(module, ff.sig_set, ff.pol_set, ff.is_fine);
+ sampled_clr = sample_control(module, ff.sig_clr, ff.pol_clr, ff.is_fine);
+ }
+ if (ff.has_arst)
+ sampled_arst = sample_control(module, ff.sig_arst, ff.pol_arst, ff.is_fine);
+
+ // First perform updates using _only_ sampled values, then again using _only_ current values. Unlike the previous
+ // implementation, this approach correctly handles all the cases of multiple signals changing simultaneously.
+ for (int current = 0; current < 2; current++) {
+ if (has_nonconst_aload)
+ next_q = mux(module, next_q, sampled_ad[current], sampled_aload[current], ff.is_fine);
+ if (ff.has_sr)
+ next_q = bitwise_sr(module, next_q, sampled_set[current], sampled_clr[current], ff.is_fine);
+ if (ff.has_arst)
+ next_q = mux(module, next_q, ff.val_arst, sampled_arst[current], ff.is_fine);
}
+
+ module->connect(ff.sig_q, next_q);
}
}
}
diff --git a/passes/sat/miter.cc b/passes/sat/miter.cc
index 37efadfbd..bf33c9ce3 100644
--- a/passes/sat/miter.cc
+++ b/passes/sat/miter.cc
@@ -31,6 +31,7 @@ void create_miter_equiv(struct Pass *that, std::vector<std::string> args, RTLIL:
bool flag_make_outcmp = false;
bool flag_make_assert = false;
bool flag_flatten = false;
+ bool flag_cross = false;
log_header(design, "Executing MITER pass (creating miter circuit).\n");
@@ -57,6 +58,10 @@ void create_miter_equiv(struct Pass *that, std::vector<std::string> args, RTLIL:
flag_flatten = true;
continue;
}
+ if (args[argidx] == "-cross") {
+ flag_cross = true;
+ continue;
+ }
break;
}
if (argidx+3 != args.size() || args[argidx].compare(0, 1, "-") == 0)
@@ -75,6 +80,7 @@ void create_miter_equiv(struct Pass *that, std::vector<std::string> args, RTLIL:
RTLIL::Module *gold_module = design->module(gold_name);
RTLIL::Module *gate_module = design->module(gate_name);
+ pool<Wire*> gold_cross_ports;
for (auto gold_wire : gold_module->wires()) {
if (gold_wire->port_id == 0)
@@ -82,12 +88,17 @@ void create_miter_equiv(struct Pass *that, std::vector<std::string> args, RTLIL:
RTLIL::Wire *gate_wire = gate_module->wire(gold_wire->name);
if (gate_wire == nullptr)
goto match_gold_port_error;
+ if (gold_wire->width != gate_wire->width)
+ goto match_gold_port_error;
+ if (flag_cross && !gold_wire->port_input && gold_wire->port_output &&
+ gate_wire->port_input && !gate_wire->port_output) {
+ gold_cross_ports.insert(gold_wire);
+ continue;
+ }
if (gold_wire->port_input != gate_wire->port_input)
goto match_gold_port_error;
if (gold_wire->port_output != gate_wire->port_output)
goto match_gold_port_error;
- if (gold_wire->width != gate_wire->width)
- goto match_gold_port_error;
continue;
match_gold_port_error:
log_cmd_error("No matching port in gate module was found for %s!\n", gold_wire->name.c_str());
@@ -99,12 +110,15 @@ void create_miter_equiv(struct Pass *that, std::vector<std::string> args, RTLIL:
RTLIL::Wire *gold_wire = gold_module->wire(gate_wire->name);
if (gold_wire == nullptr)
goto match_gate_port_error;
+ if (gate_wire->width != gold_wire->width)
+ goto match_gate_port_error;
+ if (flag_cross && !gold_wire->port_input && gold_wire->port_output &&
+ gate_wire->port_input && !gate_wire->port_output)
+ continue;
if (gate_wire->port_input != gold_wire->port_input)
goto match_gate_port_error;
if (gate_wire->port_output != gold_wire->port_output)
goto match_gate_port_error;
- if (gate_wire->width != gold_wire->width)
- goto match_gate_port_error;
continue;
match_gate_port_error:
log_cmd_error("No matching port in gold module was found for %s!\n", gate_wire->name.c_str());
@@ -123,6 +137,14 @@ void create_miter_equiv(struct Pass *that, std::vector<std::string> args, RTLIL:
for (auto gold_wire : gold_module->wires())
{
+ if (gold_cross_ports.count(gold_wire))
+ {
+ RTLIL::Wire *w = miter_module->addWire("\\cross_" + RTLIL::unescape_id(gold_wire->name), gold_wire->width);
+ gold_cell->setPort(gold_wire->name, w);
+ gate_cell->setPort(gold_wire->name, w);
+ continue;
+ }
+
if (gold_wire->port_input)
{
RTLIL::Wire *w = miter_module->addWire("\\in_" + RTLIL::unescape_id(gold_wire->name), gold_wire->width);
@@ -384,6 +406,12 @@ struct MiterPass : public Pass {
log(" call 'flatten -wb; opt_expr -keepdc -undriven;;' on the miter circuit.\n");
log("\n");
log("\n");
+ log(" -cross\n");
+ log(" allow output ports on the gold module to match input ports on the\n");
+ log(" gate module. This is useful when the gold module contains additional\n");
+ log(" logic to drive some of the gate module inputs.\n");
+ log("\n");
+ log("\n");
log(" miter -assert [options] module [miter_name]\n");
log("\n");
log("Creates a miter circuit for property checking. All input ports are kept,\n");
diff --git a/passes/sat/mutate.cc b/passes/sat/mutate.cc
index 42eb0c6d0..02174be53 100644
--- a/passes/sat/mutate.cc
+++ b/passes/sat/mutate.cc
@@ -527,6 +527,8 @@ void mutate_list(Design *design, const mutate_opts_t &opts, const string &filena
}
log("Raw database size: %d\n", GetSize(database));
+ if (N > GetSize(database))
+ log_warning("%d mutations requested but only %d could be created!\n", N, GetSize(database));
if (N != 0) {
database_reduce(database, opts, opts.none ? N-1 : N, rng);
log("Reduced database size: %d\n", GetSize(database));
diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc
index df2725b3c..69f81e3df 100644
--- a/passes/sat/sat.cc
+++ b/passes/sat/sat.cc
@@ -65,11 +65,12 @@ struct SatHelper
int max_timestep, timeout;
bool gotTimeout;
- SatHelper(RTLIL::Design *design, RTLIL::Module *module, bool enable_undef) :
+ SatHelper(RTLIL::Design *design, RTLIL::Module *module, bool enable_undef, bool set_def_formal) :
design(design), module(module), sigmap(module), ct(design), satgen(ez.get(), &sigmap)
{
this->enable_undef = enable_undef;
satgen.model_undef = enable_undef;
+ satgen.def_formal = set_def_formal;
set_init_def = false;
set_init_undef = false;
set_init_zero = false;
@@ -254,7 +255,13 @@ struct SatHelper
if (initstate)
{
- RTLIL::SigSpec big_lhs, big_rhs;
+ RTLIL::SigSpec big_lhs, big_rhs, forced_def;
+
+ // Check for $anyinit cells that are forced to be defined
+ if (set_init_undef && satgen.def_formal)
+ for (auto cell : module->cells())
+ if (cell->type == ID($anyinit))
+ forced_def.append(sigmap(cell->getPort(ID::Q)));
for (auto wire : module->wires())
{
@@ -323,6 +330,7 @@ struct SatHelper
if (set_init_undef) {
RTLIL::SigSpec rem = satgen.initial_state.export_all();
rem.remove(big_lhs);
+ rem.remove(forced_def);
big_lhs.append(rem);
big_rhs.append(RTLIL::SigSpec(RTLIL::State::Sx, rem.size()));
}
@@ -758,6 +766,7 @@ struct SatHelper
if (last_timestep == -2)
log(" no model variables selected for display.\n");
+ fprintf(f, "#%d\n", last_timestep+1);
fclose(f);
}
@@ -932,6 +941,9 @@ struct SatPass : public Pass {
log(" -set-def-inputs\n");
log(" add -set-def constraints for all module inputs\n");
log("\n");
+ log(" -set-def-formal\n");
+ log(" add -set-def constraints for formal $anyinit, $anyconst, $anyseq cells\n");
+ log("\n");
log(" -show <signal>\n");
log(" show the model for the specified signal. if no -show option is\n");
log(" passed then a set of signals to be shown is automatically selected.\n");
@@ -1067,7 +1079,7 @@ struct SatPass : public Pass {
std::map<int, std::vector<std::string>> unsets_at, sets_def_at, sets_any_undef_at, sets_all_undef_at;
std::vector<std::string> shows, sets_def, sets_any_undef, sets_all_undef;
int loopcount = 0, seq_len = 0, maxsteps = 0, initsteps = 0, timeout = 0, prove_skip = 0;
- bool verify = false, fail_on_timeout = false, enable_undef = false, set_def_inputs = false;
+ bool verify = false, fail_on_timeout = false, enable_undef = false, set_def_inputs = false, set_def_formal = false;
bool ignore_div_by_zero = false, set_init_undef = false, set_init_zero = false, max_undef = false;
bool tempinduct = false, prove_asserts = false, show_inputs = false, show_outputs = false;
bool show_regs = false, show_public = false, show_all = false;
@@ -1140,6 +1152,11 @@ struct SatPass : public Pass {
set_def_inputs = true;
continue;
}
+ if (args[argidx] == "-set-def-formal") {
+ enable_undef = true;
+ set_def_formal = true;
+ continue;
+ }
if (args[argidx] == "-set" && argidx+2 < args.size()) {
std::string lhs = args[++argidx];
std::string rhs = args[++argidx];
@@ -1379,8 +1396,8 @@ struct SatPass : public Pass {
if (loopcount > 0 || max_undef)
log_cmd_error("The options -max, -all, and -max_undef are not supported for temporal induction proofs!\n");
- SatHelper basecase(design, module, enable_undef);
- SatHelper inductstep(design, module, enable_undef);
+ SatHelper basecase(design, module, enable_undef, set_def_formal);
+ SatHelper inductstep(design, module, enable_undef, set_def_formal);
basecase.sets = sets;
basecase.set_assumes = set_assumes;
@@ -1569,7 +1586,7 @@ struct SatPass : public Pass {
if (maxsteps > 0)
log_cmd_error("The options -maxsteps is only supported for temporal induction proofs!\n");
- SatHelper sathelper(design, module, enable_undef);
+ SatHelper sathelper(design, module, enable_undef, set_def_formal);
sathelper.sets = sets;
sathelper.set_assumes = set_assumes;
diff --git a/passes/sat/sim.cc b/passes/sat/sim.cc
index b68783f20..1cd1ebc71 100644
--- a/passes/sat/sim.cc
+++ b/passes/sat/sim.cc
@@ -813,18 +813,6 @@ struct SimInstance
std::string v = shared->fst->valueOf(item.second);
did_something |= set_state(item.first, Const::from_string(v));
}
- for (auto &it : ff_database)
- {
- ff_state_t &ff = it.second;
- SigSpec dsig = it.second.data.sig_d;
- Const value = get_state(dsig);
- if (dsig.is_wire()) {
- ff.past_d = value;
- if (ff.data.has_aload)
- ff.past_ad = value;
- did_something |= true;
- }
- }
for (auto cell : module->cells())
{
if (cell->is_mem_cell()) {
@@ -1019,6 +1007,16 @@ struct SimWorker : SimShared
top->update_ph3();
}
+ void initialize_stable_past()
+ {
+ if (debug)
+ log("\n-- ph1 (initialize) --\n");
+ top->update_ph1();
+ if (debug)
+ log("\n-- ph3 (initialize) --\n");
+ top->update_ph3();
+ }
+
void set_inports(pool<IdString> ports, State value)
{
for (auto portname : ports)
@@ -1191,6 +1189,7 @@ struct SimWorker : SimShared
if (initial) {
did_something |= top->setInitState();
+ initialize_stable_past();
initial = false;
}
if (did_something)
@@ -2015,7 +2014,7 @@ struct SimPass : public Pass {
log(" -r\n");
log(" read simulation results file\n");
log(" File formats supported: FST, VCD, AIW and WIT\n");
- log(" VCD support requires vcd2fst external tool to be present\n");
+ log(" VCD support requires vcd2fst external tool to be present\n");
log("\n");
log(" -map <filename>\n");
log(" read file with port and latch symbols, needed for AIGER witness input\n");
diff --git a/passes/techmap/flowmap.cc b/passes/techmap/flowmap.cc
index dfdbe6b88..579503a0b 100644
--- a/passes/techmap/flowmap.cc
+++ b/passes/techmap/flowmap.cc
@@ -1406,7 +1406,8 @@ struct FlowmapWorker
RTLIL::SigSpec lut_a, lut_y = node;
for (auto input_node : input_nodes)
lut_a.append(input_node);
- lut_a.append(RTLIL::Const(State::Sx, minlut - input_nodes.size()));
+ if ((int)input_nodes.size() < minlut)
+ lut_a.append(RTLIL::Const(State::Sx, minlut - input_nodes.size()));
RTLIL::Cell *lut = module->addLut(NEW_ID, lut_a, lut_y, lut_table);
mapped_nodes.insert(node);
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-25 21:57:59 +0000