aboutsummaryrefslogtreecommitdiffstats
path: root/passes/sat
diff options
context:
space:
mode:
Diffstat (limited to 'passes/sat')
-rw-r--r--passes/sat/assertpmux.cc4
-rw-r--r--passes/sat/async2sync.cc336
-rw-r--r--passes/sat/clk2fflogic.cc451
-rw-r--r--passes/sat/cutpoint.cc2
-rw-r--r--passes/sat/eval.cc4
-rw-r--r--passes/sat/expose.cc2
-rw-r--r--passes/sat/fmcombine.cc5
-rw-r--r--passes/sat/fminit.cc2
-rw-r--r--passes/sat/freduce.cc3
-rw-r--r--passes/sat/miter.cc2
-rw-r--r--passes/sat/mutate.cc8
-rw-r--r--passes/sat/qbfsat.cc291
-rw-r--r--passes/sat/qbfsat.h253
-rw-r--r--passes/sat/sat.cc4
-rw-r--r--passes/sat/sim.cc678
-rw-r--r--passes/sat/supercover.cc2
16 files changed, 1201 insertions, 846 deletions
diff --git a/passes/sat/assertpmux.cc b/passes/sat/assertpmux.cc
index e9a10465e..abdcb2240 100644
--- a/passes/sat/assertpmux.cc
+++ b/passes/sat/assertpmux.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
@@ -88,7 +88,7 @@ struct AssertpmuxWorker
{
SigSpec output;
- for (auto muxuser : sigbit_muxusers.at(bit))
+ for (auto muxuser : sigbit_muxusers[bit])
{
Cell *cell = std::get<0>(muxuser);
int portidx = std::get<1>(muxuser);
diff --git a/passes/sat/async2sync.cc b/passes/sat/async2sync.cc
index 6fc480925..46c76eba9 100644
--- a/passes/sat/async2sync.cc
+++ b/passes/sat/async2sync.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
@@ -19,6 +19,8 @@
#include "kernel/yosys.h"
#include "kernel/sigtools.h"
+#include "kernel/ffinit.h"
+#include "kernel/ff.h"
USING_YOSYS_NAMESPACE
PRIVATE_NAMESPACE_BEGIN
@@ -39,8 +41,6 @@ struct Async2syncPass : public Pass {
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");
- log("Currently only $adff, $dffsr, and $dlatch cells are supported by this pass.\n");
- log("\n");
}
void execute(std::vector<std::string> args, RTLIL::Design *design) override
{
@@ -62,169 +62,213 @@ struct Async2syncPass : public Pass {
for (auto module : design->selected_modules())
{
SigMap sigmap(module);
- dict<SigBit, State> initbits;
- pool<SigBit> del_initbits;
-
- for (auto wire : module->wires())
- if (wire->attributes.count(ID::init) > 0)
- {
- Const initval = wire->attributes.at(ID::init);
- SigSpec initsig = sigmap(wire);
-
- for (int i = 0; i < GetSize(initval) && i < GetSize(initsig); i++)
- if (initval[i] == State::S0 || initval[i] == State::S1)
- initbits[initsig[i]] = initval[i];
- }
+ FfInitVals initvals(&sigmap, module);
for (auto cell : vector<Cell*>(module->selected_cells()))
{
- if (cell->type.in(ID($adff)))
- {
- // bool clk_pol = cell->parameters[ID::CLK_POLARITY].as_bool();
- bool arst_pol = cell->parameters[ID::ARST_POLARITY].as_bool();
- Const arst_val = cell->parameters[ID::ARST_VALUE];
-
- // SigSpec sig_clk = cell->getPort(ID::CLK);
- SigSpec sig_arst = cell->getPort(ID::ARST);
- SigSpec sig_d = cell->getPort(ID::D);
- SigSpec sig_q = cell->getPort(ID::Q);
-
- log("Replacing %s.%s (%s): ARST=%s, D=%s, Q=%s\n",
- log_id(module), log_id(cell), log_id(cell->type),
- log_signal(sig_arst), log_signal(sig_d), log_signal(sig_q));
-
- Const init_val;
- for (int i = 0; i < GetSize(sig_q); i++) {
- SigBit bit = sigmap(sig_q[i]);
- init_val.bits.push_back(initbits.count(bit) ? initbits.at(bit) : State::Sx);
- del_initbits.insert(bit);
- }
-
- Wire *new_d = module->addWire(NEW_ID, GetSize(sig_d));
- Wire *new_q = module->addWire(NEW_ID, GetSize(sig_q));
- new_q->attributes[ID::init] = init_val;
+ if (!RTLIL::builtin_ff_cell_types().count(cell->type))
+ continue;
- if (arst_pol) {
- module->addMux(NEW_ID, sig_d, arst_val, sig_arst, new_d);
- module->addMux(NEW_ID, new_q, arst_val, sig_arst, sig_q);
- } else {
- module->addMux(NEW_ID, arst_val, sig_d, sig_arst, new_d);
- module->addMux(NEW_ID, arst_val, new_q, sig_arst, sig_q);
- }
+ FfData ff(&initvals, cell);
- cell->setPort(ID::D, new_d);
- cell->setPort(ID::Q, new_q);
- cell->unsetPort(ID::ARST);
- cell->unsetParam(ID::ARST_POLARITY);
- cell->unsetParam(ID::ARST_VALUE);
- cell->type = ID($dff);
+ // Skip for $_FF_ and $ff cells.
+ if (ff.has_gclk)
continue;
- }
- if (cell->type.in(ID($dffsr)))
+ if (ff.has_clk)
{
- // bool clk_pol = cell->parameters[ID::CLK_POLARITY].as_bool();
- bool set_pol = cell->parameters[ID::SET_POLARITY].as_bool();
- bool clr_pol = cell->parameters[ID::CLR_POLARITY].as_bool();
-
- // SigSpec sig_clk = cell->getPort(ID::CLK);
- SigSpec sig_set = cell->getPort(ID::SET);
- SigSpec sig_clr = cell->getPort(ID::CLR);
- SigSpec sig_d = cell->getPort(ID::D);
- SigSpec sig_q = cell->getPort(ID::Q);
-
- log("Replacing %s.%s (%s): SET=%s, CLR=%s, D=%s, Q=%s\n",
- log_id(module), log_id(cell), log_id(cell->type),
- log_signal(sig_set), log_signal(sig_clr), log_signal(sig_d), log_signal(sig_q));
-
- Const init_val;
- for (int i = 0; i < GetSize(sig_q); i++) {
- SigBit bit = sigmap(sig_q[i]);
- init_val.bits.push_back(initbits.count(bit) ? initbits.at(bit) : State::Sx);
- del_initbits.insert(bit);
+ if (ff.has_sr) {
+ ff.unmap_ce_srst();
+
+ log("Replacing %s.%s (%s): SET=%s, CLR=%s, D=%s, Q=%s\n",
+ log_id(module), log_id(cell), log_id(cell->type),
+ log_signal(ff.sig_set), log_signal(ff.sig_clr), log_signal(ff.sig_d), log_signal(ff.sig_q));
+
+ initvals.remove_init(ff.sig_q);
+
+ Wire *new_d = module->addWire(NEW_ID, ff.width);
+ Wire *new_q = module->addWire(NEW_ID, ff.width);
+
+ SigSpec sig_set = ff.sig_set;
+ SigSpec sig_clr = ff.sig_clr;
+
+ if (!ff.pol_set) {
+ if (!ff.is_fine)
+ sig_set = module->Not(NEW_ID, sig_set);
+ else
+ sig_set = module->NotGate(NEW_ID, sig_set);
+ }
+
+ if (ff.pol_clr) {
+ if (!ff.is_fine)
+ sig_clr = module->Not(NEW_ID, sig_clr);
+ else
+ sig_clr = module->NotGate(NEW_ID, sig_clr);
+ }
+
+ if (!ff.is_fine) {
+ SigSpec tmp = module->Or(NEW_ID, ff.sig_d, sig_set);
+ module->addAnd(NEW_ID, tmp, sig_clr, new_d);
+
+ tmp = module->Or(NEW_ID, new_q, sig_set);
+ module->addAnd(NEW_ID, tmp, sig_clr, ff.sig_q);
+ } else {
+ SigSpec tmp = module->OrGate(NEW_ID, ff.sig_d, sig_set);
+ module->addAndGate(NEW_ID, tmp, sig_clr, new_d);
+
+ tmp = module->OrGate(NEW_ID, new_q, sig_set);
+ module->addAndGate(NEW_ID, tmp, sig_clr, ff.sig_q);
+ }
+
+ ff.sig_d = new_d;
+ ff.sig_q = new_q;
+ ff.has_sr = false;
+ } else if (ff.has_aload) {
+ ff.unmap_ce_srst();
+
+ log("Replacing %s.%s (%s): ALOAD=%s, AD=%s, D=%s, Q=%s\n",
+ log_id(module), log_id(cell), log_id(cell->type),
+ log_signal(ff.sig_aload), log_signal(ff.sig_ad), log_signal(ff.sig_d), log_signal(ff.sig_q));
+
+ initvals.remove_init(ff.sig_q);
+
+ Wire *new_d = module->addWire(NEW_ID, ff.width);
+ Wire *new_q = module->addWire(NEW_ID, ff.width);
+
+ if (ff.pol_aload) {
+ if (!ff.is_fine) {
+ module->addMux(NEW_ID, new_q, ff.sig_ad, ff.sig_aload, ff.sig_q);
+ module->addMux(NEW_ID, ff.sig_d, ff.sig_ad, ff.sig_aload, new_d);
+ } else {
+ module->addMuxGate(NEW_ID, new_q, ff.sig_ad, ff.sig_aload, ff.sig_q);
+ module->addMuxGate(NEW_ID, ff.sig_d, ff.sig_ad, ff.sig_aload, new_d);
+ }
+ } else {
+ if (!ff.is_fine) {
+ module->addMux(NEW_ID, ff.sig_ad, new_q, ff.sig_aload, ff.sig_q);
+ module->addMux(NEW_ID, ff.sig_ad, ff.sig_d, ff.sig_aload, new_d);
+ } else {
+ module->addMuxGate(NEW_ID, ff.sig_ad, new_q, ff.sig_aload, ff.sig_q);
+ module->addMuxGate(NEW_ID, ff.sig_ad, ff.sig_d, ff.sig_aload, new_d);
+ }
+ }
+
+ ff.sig_d = new_d;
+ ff.sig_q = new_q;
+ ff.has_aload = false;
+ } else if (ff.has_arst) {
+ ff.unmap_srst();
+
+ log("Replacing %s.%s (%s): ARST=%s, D=%s, Q=%s\n",
+ log_id(module), log_id(cell), log_id(cell->type),
+ log_signal(ff.sig_arst), log_signal(ff.sig_d), log_signal(ff.sig_q));
+
+ initvals.remove_init(ff.sig_q);
+
+ Wire *new_q = module->addWire(NEW_ID, ff.width);
+
+ if (ff.pol_arst) {
+ if (!ff.is_fine)
+ module->addMux(NEW_ID, new_q, ff.val_arst, ff.sig_arst, ff.sig_q);
+ else
+ module->addMuxGate(NEW_ID, new_q, ff.val_arst[0], ff.sig_arst, ff.sig_q);
+ } else {
+ if (!ff.is_fine)
+ module->addMux(NEW_ID, ff.val_arst, new_q, ff.sig_arst, ff.sig_q);
+ else
+ module->addMuxGate(NEW_ID, ff.val_arst[0], new_q, ff.sig_arst, ff.sig_q);
+ }
+
+ ff.sig_q = new_q;
+ ff.has_arst = false;
+ ff.has_srst = true;
+ ff.ce_over_srst = false;
+ ff.val_srst = ff.val_arst;
+ ff.sig_srst = ff.sig_arst;
+ ff.pol_srst = ff.pol_arst;
+ } else {
+ continue;
}
-
- Wire *new_d = module->addWire(NEW_ID, GetSize(sig_d));
- Wire *new_q = module->addWire(NEW_ID, GetSize(sig_q));
- new_q->attributes[ID::init] = init_val;
-
- if (!set_pol)
- sig_set = module->Not(NEW_ID, sig_set);
-
- if (clr_pol)
- sig_clr = module->Not(NEW_ID, sig_clr);
-
- SigSpec tmp = module->Or(NEW_ID, sig_d, sig_set);
- module->addAnd(NEW_ID, tmp, sig_clr, new_d);
-
- tmp = module->Or(NEW_ID, new_q, sig_set);
- module->addAnd(NEW_ID, tmp, sig_clr, sig_q);
-
- cell->setPort(ID::D, new_d);
- cell->setPort(ID::Q, new_q);
- cell->unsetPort(ID::SET);
- cell->unsetPort(ID::CLR);
- cell->unsetParam(ID::SET_POLARITY);
- cell->unsetParam(ID::CLR_POLARITY);
- cell->type = ID($dff);
- continue;
}
-
- if (cell->type.in(ID($dlatch)))
+ else
{
- bool en_pol = cell->parameters[ID::EN_POLARITY].as_bool();
-
- SigSpec sig_en = cell->getPort(ID::EN);
- SigSpec sig_d = cell->getPort(ID::D);
- SigSpec sig_q = cell->getPort(ID::Q);
-
+ // Latch.
log("Replacing %s.%s (%s): EN=%s, D=%s, Q=%s\n",
log_id(module), log_id(cell), log_id(cell->type),
- log_signal(sig_en), log_signal(sig_d), log_signal(sig_q));
-
- Const init_val;
- for (int i = 0; i < GetSize(sig_q); i++) {
- SigBit bit = sigmap(sig_q[i]);
- init_val.bits.push_back(initbits.count(bit) ? initbits.at(bit) : State::Sx);
- del_initbits.insert(bit);
+ log_signal(ff.sig_aload), log_signal(ff.sig_ad), log_signal(ff.sig_q));
+
+ initvals.remove_init(ff.sig_q);
+
+ Wire *new_q = module->addWire(NEW_ID, ff.width);
+ Wire *new_d;
+
+ if (ff.has_aload) {
+ new_d = module->addWire(NEW_ID, ff.width);
+ if (ff.pol_aload) {
+ if (!ff.is_fine)
+ module->addMux(NEW_ID, new_q, ff.sig_ad, ff.sig_aload, new_d);
+ else
+ module->addMuxGate(NEW_ID, new_q, ff.sig_ad, ff.sig_aload, new_d);
+ } else {
+ if (!ff.is_fine)
+ module->addMux(NEW_ID, ff.sig_ad, new_q, ff.sig_aload, new_d);
+ else
+ module->addMuxGate(NEW_ID, ff.sig_ad, new_q, ff.sig_aload, new_d);
+ }
+ } else {
+ new_d = new_q;
}
- Wire *new_q = module->addWire(NEW_ID, GetSize(sig_q));
- new_q->attributes[ID::init] = init_val;
-
- if (en_pol) {
- module->addMux(NEW_ID, new_q, sig_d, sig_en, sig_q);
+ if (ff.has_sr) {
+ SigSpec sig_set = ff.sig_set;
+ SigSpec sig_clr = ff.sig_clr;
+
+ if (!ff.pol_set) {
+ if (!ff.is_fine)
+ sig_set = module->Not(NEW_ID, sig_set);
+ else
+ sig_set = module->NotGate(NEW_ID, sig_set);
+ }
+
+ if (ff.pol_clr) {
+ if (!ff.is_fine)
+ sig_clr = module->Not(NEW_ID, sig_clr);
+ else
+ sig_clr = module->NotGate(NEW_ID, sig_clr);
+ }
+
+ if (!ff.is_fine) {
+ SigSpec tmp = module->Or(NEW_ID, new_d, sig_set);
+ module->addAnd(NEW_ID, tmp, sig_clr, ff.sig_q);
+ } else {
+ SigSpec tmp = module->OrGate(NEW_ID, new_d, sig_set);
+ module->addAndGate(NEW_ID, tmp, sig_clr, ff.sig_q);
+ }
+ } else if (ff.has_arst) {
+ if (ff.pol_arst) {
+ if (!ff.is_fine)
+ module->addMux(NEW_ID, new_d, ff.val_arst, ff.sig_arst, ff.sig_q);
+ else
+ module->addMuxGate(NEW_ID, new_d, ff.val_arst[0], ff.sig_arst, ff.sig_q);
+ } else {
+ if (!ff.is_fine)
+ module->addMux(NEW_ID, ff.val_arst, new_d, ff.sig_arst, ff.sig_q);
+ else
+ module->addMuxGate(NEW_ID, ff.val_arst[0], new_d, ff.sig_arst, ff.sig_q);
+ }
} else {
- module->addMux(NEW_ID, sig_d, new_q, sig_en, sig_q);
+ module->connect(ff.sig_q, new_d);
}
- cell->setPort(ID::D, sig_q);
- cell->setPort(ID::Q, new_q);
- cell->unsetPort(ID::EN);
- cell->unsetParam(ID::EN_POLARITY);
- cell->type = ID($ff);
- continue;
+ ff.sig_d = new_d;
+ ff.sig_q = new_q;
+ ff.has_aload = false;
+ ff.has_arst = false;
+ ff.has_sr = false;
+ ff.has_gclk = true;
}
+ ff.emit();
}
-
- for (auto wire : module->wires())
- if (wire->attributes.count(ID::init) > 0)
- {
- bool delete_initattr = true;
- Const initval = wire->attributes.at(ID::init);
- SigSpec initsig = sigmap(wire);
-
- for (int i = 0; i < GetSize(initval) && i < GetSize(initsig); i++)
- if (del_initbits.count(initsig[i]) > 0)
- initval[i] = State::Sx;
- else if (initval[i] != State::Sx)
- delete_initattr = false;
-
- if (delete_initattr)
- wire->attributes.erase(ID::init);
- else
- wire->attributes.at(ID::init) = initval;
- }
}
}
} Async2syncPass;
diff --git a/passes/sat/clk2fflogic.cc b/passes/sat/clk2fflogic.cc
index e5c5d0486..a292941c8 100644
--- a/passes/sat/clk2fflogic.cc
+++ b/passes/sat/clk2fflogic.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
@@ -19,6 +19,9 @@
#include "kernel/yosys.h"
#include "kernel/sigtools.h"
+#include "kernel/ffinit.h"
+#include "kernel/ff.h"
+#include "kernel/mem.h"
USING_YOSYS_NAMESPACE
PRIVATE_NAMESPACE_BEGIN
@@ -36,6 +39,30 @@ struct Clk2fflogicPass : public Pass {
log("multiple clocks.\n");
log("\n");
}
+ SigSpec wrap_async_control(Module *module, SigSpec sig, bool polarity) {
+ Wire *past_sig = module->addWire(NEW_ID, GetSize(sig));
+ module->addFf(NEW_ID, sig, past_sig);
+ if (polarity)
+ sig = module->Or(NEW_ID, sig, past_sig);
+ else
+ sig = module->And(NEW_ID, sig, past_sig);
+ if (polarity)
+ return sig;
+ else
+ return module->Not(NEW_ID, sig);
+ }
+ SigSpec wrap_async_control_gate(Module *module, SigSpec sig, bool polarity) {
+ Wire *past_sig = module->addWire(NEW_ID);
+ module->addFfGate(NEW_ID, sig, past_sig);
+ if (polarity)
+ sig = module->OrGate(NEW_ID, sig, past_sig);
+ else
+ sig = module->AndGate(NEW_ID, sig, past_sig);
+ if (polarity)
+ return sig;
+ else
+ return module->NotGate(NEW_ID, sig);
+ }
void execute(std::vector<std::string> args, RTLIL::Design *design) override
{
// bool flag_noinit = false;
@@ -56,348 +83,174 @@ struct Clk2fflogicPass : public Pass {
for (auto module : design->selected_modules())
{
SigMap sigmap(module);
- dict<SigBit, State> initbits;
- pool<SigBit> del_initbits;
-
- for (auto wire : module->wires())
- if (wire->attributes.count(ID::init) > 0)
- {
- Const initval = wire->attributes.at(ID::init);
- SigSpec initsig = sigmap(wire);
+ FfInitVals initvals(&sigmap, module);
- for (int i = 0; i < GetSize(initval) && i < GetSize(initsig); i++)
- if (initval[i] == State::S0 || initval[i] == State::S1)
- initbits[initsig[i]] = initval[i];
+ for (auto &mem : Mem::get_selected_memories(module))
+ {
+ for (int i = 0; i < GetSize(mem.rd_ports); i++) {
+ auto &port = mem.rd_ports[i];
+ if (port.clk_enable)
+ log_error("Read port %d of memory %s.%s is clocked. This is not supported by \"clk2fflogic\"! "
+ "Call \"memory\" with -nordff to avoid this error.\n", i, log_id(mem.memid), log_id(module));
}
- for (auto cell : vector<Cell*>(module->selected_cells()))
- {
- if (cell->type.in(ID($mem)))
+ for (int i = 0; i < GetSize(mem.wr_ports); i++)
{
- int abits = cell->getParam(ID::ABITS).as_int();
- int width = cell->getParam(ID::WIDTH).as_int();
- int rd_ports = cell->getParam(ID::RD_PORTS).as_int();
- int wr_ports = cell->getParam(ID::WR_PORTS).as_int();
-
- for (int i = 0; i < rd_ports; i++) {
- if (cell->getParam(ID::RD_CLK_ENABLE).extract(i).as_bool())
- log_error("Read port %d of memory %s.%s is clocked. This is not supported by \"clk2fflogic\"! "
- "Call \"memory\" with -nordff to avoid this error.\n", i, log_id(cell), log_id(module));
- }
-
- Const wr_clk_en_param = cell->getParam(ID::WR_CLK_ENABLE);
- Const wr_clk_pol_param = cell->getParam(ID::WR_CLK_POLARITY);
-
- SigSpec wr_clk_port = cell->getPort(ID::WR_CLK);
- SigSpec wr_en_port = cell->getPort(ID::WR_EN);
- SigSpec wr_addr_port = cell->getPort(ID::WR_ADDR);
- SigSpec wr_data_port = cell->getPort(ID::WR_DATA);
-
- for (int wport = 0; wport < wr_ports; wport++)
- {
- bool clken = wr_clk_en_param[wport] == State::S1;
- bool clkpol = wr_clk_pol_param[wport] == State::S1;
-
- if (!clken)
- continue;
+ auto &port = mem.wr_ports[i];
- SigBit clk = wr_clk_port[wport];
- SigSpec en = wr_en_port.extract(wport*width, width);
- SigSpec addr = wr_addr_port.extract(wport*abits, abits);
- SigSpec data = wr_data_port.extract(wport*width, width);
-
- log("Modifying write port %d on memory %s.%s: CLK=%s, A=%s, D=%s\n",
- wport, log_id(module), log_id(cell), log_signal(clk),
- log_signal(addr), log_signal(data));
-
- Wire *past_clk = module->addWire(NEW_ID);
- past_clk->attributes[ID::init] = clkpol ? State::S1 : State::S0;
- module->addFf(NEW_ID, clk, past_clk);
-
- SigSpec clock_edge_pattern;
-
- if (clkpol) {
- 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);
- }
+ if (!port.clk_enable)
+ continue;
- SigSpec clock_edge = module->Eqx(NEW_ID, {clk, SigSpec(past_clk)}, clock_edge_pattern);
+ log("Modifying write port %d on memory %s.%s: CLK=%s, A=%s, D=%s\n",
+ i, log_id(module), log_id(mem.memid), log_signal(port.clk),
+ log_signal(port.addr), log_signal(port.data));
- SigSpec en_q = module->addWire(NEW_ID, GetSize(en));
- module->addFf(NEW_ID, en, en_q);
-
- SigSpec addr_q = module->addWire(NEW_ID, GetSize(addr));
- module->addFf(NEW_ID, addr, addr_q);
-
- SigSpec data_q = module->addWire(NEW_ID, GetSize(data));
- module->addFf(NEW_ID, data, data_q);
+ Wire *past_clk = module->addWire(NEW_ID);
+ past_clk->attributes[ID::init] = port.clk_polarity ? State::S1 : State::S0;
+ module->addFf(NEW_ID, port.clk, past_clk);
- wr_clk_port[wport] = State::S0;
- wr_en_port.replace(wport*width, module->Mux(NEW_ID, Const(0, GetSize(en_q)), en_q, clock_edge));
- wr_addr_port.replace(wport*abits, addr_q);
- wr_data_port.replace(wport*width, data_q);
+ SigSpec clock_edge_pattern;
- wr_clk_en_param[wport] = State::S0;
- wr_clk_pol_param[wport] = State::S0;
+ if (port.clk_polarity) {
+ 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);
}
- cell->setParam(ID::WR_CLK_ENABLE, wr_clk_en_param);
- cell->setParam(ID::WR_CLK_POLARITY, wr_clk_pol_param);
+ SigSpec clock_edge = module->Eqx(NEW_ID, {port.clk, SigSpec(past_clk)}, clock_edge_pattern);
- cell->setPort(ID::WR_CLK, wr_clk_port);
- cell->setPort(ID::WR_EN, wr_en_port);
- cell->setPort(ID::WR_ADDR, wr_addr_port);
- cell->setPort(ID::WR_DATA, wr_data_port);
- }
+ SigSpec en_q = module->addWire(NEW_ID, GetSize(port.en));
+ module->addFf(NEW_ID, port.en, en_q);
- if (cell->type.in(ID($dlatch), ID($dlatchsr)))
- {
- bool enpol = cell->parameters[ID::EN_POLARITY].as_bool();
+ SigSpec addr_q = module->addWire(NEW_ID, GetSize(port.addr));
+ module->addFf(NEW_ID, port.addr, addr_q);
- SigSpec sig_en = cell->getPort(ID::EN);
- SigSpec sig_d = cell->getPort(ID::D);
- SigSpec sig_q = cell->getPort(ID::Q);
+ SigSpec data_q = module->addWire(NEW_ID, GetSize(port.data));
+ module->addFf(NEW_ID, port.data, data_q);
- log("Replacing %s.%s (%s): EN=%s, D=%s, Q=%s\n",
- log_id(module), log_id(cell), log_id(cell->type),
- log_signal(sig_en), log_signal(sig_d), log_signal(sig_q));
+ port.clk = State::S0;
+ port.en = module->Mux(NEW_ID, Const(0, GetSize(en_q)), en_q, clock_edge);
+ port.addr = addr_q;
+ port.data = data_q;
- Wire *past_q = module->addWire(NEW_ID, GetSize(sig_q));
- module->addFf(NEW_ID, sig_q, past_q);
+ port.clk_enable = false;
+ port.clk_polarity = false;
+ }
- if (cell->type == ID($dlatch))
- {
- if (enpol)
- module->addMux(NEW_ID, past_q, sig_d, sig_en, sig_q);
- else
- module->addMux(NEW_ID, sig_d, past_q, sig_en, sig_q);
- }
- else
- {
- SigSpec t;
- if (enpol)
- t = module->Mux(NEW_ID, past_q, sig_d, sig_en);
- else
- t = module->Mux(NEW_ID, sig_d, past_q, sig_en);
+ mem.emit();
+ }
- SigSpec s = cell->getPort(ID::SET);
- if (!cell->parameters[ID::SET_POLARITY].as_bool())
- s = module->Not(NEW_ID, s);
- t = module->Or(NEW_ID, t, s);
+ for (auto cell : vector<Cell*>(module->selected_cells()))
+ {
+ SigSpec qval;
+ if (RTLIL::builtin_ff_cell_types().count(cell->type)) {
+ FfData ff(&initvals, cell);
- SigSpec c = cell->getPort(ID::CLR);
- if (cell->parameters[ID::CLR_POLARITY].as_bool())
- c = module->Not(NEW_ID, c);
- module->addAnd(NEW_ID, t, c, sig_q);
+ if (ff.has_gclk) {
+ // Already a $ff or $_FF_ cell.
+ continue;
}
- Const initval;
- bool assign_initval = false;
- for (int i = 0; i < GetSize(sig_d); i++) {
- SigBit qbit = sigmap(sig_q[i]);
- if (initbits.count(qbit)) {
- initval.bits.push_back(initbits.at(qbit));
- del_initbits.insert(qbit);
- } else
- initval.bits.push_back(State::Sx);
- if (initval.bits.back() != State::Sx)
- assign_initval = true;
+ if (ff.has_clk) {
+ log("Replacing %s.%s (%s): CLK=%s, D=%s, Q=%s\n",
+ log_id(module), log_id(cell), log_id(cell->type),
+ log_signal(ff.sig_clk), log_signal(ff.sig_d), log_signal(ff.sig_q));
+ } else if (ff.has_aload) {
+ log("Replacing %s.%s (%s): EN=%s, D=%s, Q=%s\n",
+ log_id(module), log_id(cell), log_id(cell->type),
+ log_signal(ff.sig_aload), log_signal(ff.sig_ad), log_signal(ff.sig_q));
+ } else {
+ // $sr.
+ log("Replacing %s.%s (%s): SET=%s, CLR=%s, Q=%s\n",
+ log_id(module), log_id(cell), log_id(cell->type),
+ log_signal(ff.sig_set), log_signal(ff.sig_clr), log_signal(ff.sig_q));
}
- if (assign_initval)
- past_q->attributes[ID::init] = initval;
-
- module->remove(cell);
- continue;
- }
+ ff.remove();
- bool word_dff = cell->type.in(ID($dff), ID($adff), ID($dffsr));
- if (word_dff || cell->type.in(ID($_DFF_N_), ID($_DFF_P_),
- ID($_DFF_NN0_), ID($_DFF_NN1_), ID($_DFF_NP0_), ID($_DFF_NP1_),
- ID($_DFF_PP0_), ID($_DFF_PP1_), ID($_DFF_PN0_), ID($_DFF_PN1_),
- ID($_DFFSR_NNN_), ID($_DFFSR_NNP_), ID($_DFFSR_NPN_), ID($_DFFSR_NPP_),
- ID($_DFFSR_PNN_), ID($_DFFSR_PNP_), ID($_DFFSR_PPN_), ID($_DFFSR_PPP_)))
- {
- bool clkpol;
- SigSpec clk;
- if (word_dff) {
- clkpol = cell->parameters[ID::CLK_POLARITY].as_bool();
- clk = cell->getPort(ID::CLK);
- }
- else {
- if (cell->type.in(ID($_DFF_P_), ID($_DFF_N_),
- ID($_DFF_NN0_), ID($_DFF_NN1_), ID($_DFF_NP0_), ID($_DFF_NP1_),
- ID($_DFF_PP0_), ID($_DFF_PP1_), ID($_DFF_PN0_), ID($_DFF_PN1_)))
- clkpol = cell->type[6] == 'P';
- else if (cell->type.in(ID($_DFFSR_NNN_), ID($_DFFSR_NNP_), ID($_DFFSR_NPN_), ID($_DFFSR_NPP_),
- ID($_DFFSR_PNN_), ID($_DFFSR_PNP_), ID($_DFFSR_PPN_), ID($_DFFSR_PPP_)))
- clkpol = cell->type[8] == 'P';
- else log_abort();
- clk = cell->getPort(ID::C);
+ Wire *past_q = module->addWire(NEW_ID, 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);
- Wire *past_clk = module->addWire(NEW_ID);
- past_clk->attributes[ID::init] = clkpol ? State::S1 : State::S0;
-
- if (word_dff)
- module->addFf(NEW_ID, clk, past_clk);
- else
- module->addFfGate(NEW_ID, clk, past_clk);
+ if (ff.has_clk) {
+ ff.unmap_ce_srst();
- SigSpec sig_d = cell->getPort(ID::D);
- SigSpec sig_q = cell->getPort(ID::Q);
-
- log("Replacing %s.%s (%s): CLK=%s, D=%s, Q=%s\n",
- log_id(module), log_id(cell), log_id(cell->type),
- log_signal(clk), log_signal(sig_d), log_signal(sig_q));
-
- SigSpec clock_edge_pattern;
+ Wire *past_clk = module->addWire(NEW_ID);
+ initvals.set_init(past_clk, ff.pol_clk ? State::S1 : State::S0);
- if (clkpol) {
- 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);
- }
+ if (!ff.is_fine)
+ module->addFf(NEW_ID, ff.sig_clk, past_clk);
+ else
+ module->addFfGate(NEW_ID, ff.sig_clk, past_clk);
- SigSpec clock_edge = module->Eqx(NEW_ID, {clk, SigSpec(past_clk)}, clock_edge_pattern);
+ SigSpec clock_edge_pattern;
- Wire *past_d = module->addWire(NEW_ID, GetSize(sig_d));
- Wire *past_q = module->addWire(NEW_ID, GetSize(sig_q));
- if (word_dff) {
- module->addFf(NEW_ID, sig_d, past_d);
- module->addFf(NEW_ID, sig_q, past_q);
- }
- else {
- module->addFfGate(NEW_ID, sig_d, past_d);
- module->addFfGate(NEW_ID, sig_q, past_q);
- }
+ 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);
+ }
- if (cell->type == ID($adff))
- {
- SigSpec arst = cell->getPort(ID::ARST);
- SigSpec qval = module->Mux(NEW_ID, past_q, past_d, clock_edge);
- Const rstval = cell->parameters[ID::ARST_VALUE];
+ SigSpec clock_edge = module->Eqx(NEW_ID, {ff.sig_clk, SigSpec(past_clk)}, clock_edge_pattern);
- Wire *past_arst = module->addWire(NEW_ID);
- module->addFf(NEW_ID, arst, past_arst);
- if (cell->parameters[ID::ARST_POLARITY].as_bool())
- arst = module->LogicOr(NEW_ID, arst, past_arst);
+ Wire *past_d = module->addWire(NEW_ID, ff.width);
+ if (!ff.is_fine)
+ module->addFf(NEW_ID, ff.sig_d, past_d);
else
- arst = module->LogicAnd(NEW_ID, arst, past_arst);
+ module->addFfGate(NEW_ID, ff.sig_d, past_d);
- if (cell->parameters[ID::ARST_POLARITY].as_bool())
- module->addMux(NEW_ID, qval, rstval, arst, sig_q);
- else
- module->addMux(NEW_ID, rstval, qval, arst, sig_q);
- }
- else
- if (cell->type.in(ID($_DFF_NN0_), ID($_DFF_NN1_), ID($_DFF_NP0_), ID($_DFF_NP1_),
- ID($_DFF_PP0_), ID($_DFF_PP1_), ID($_DFF_PN0_), ID($_DFF_PN1_)))
- {
- SigSpec arst = cell->getPort(ID::R);
- SigSpec qval = module->MuxGate(NEW_ID, past_q, past_d, clock_edge);
- SigBit rstval = (cell->type[8] == '1');
-
- Wire *past_arst = module->addWire(NEW_ID);
- module->addFfGate(NEW_ID, arst, past_arst);
- if (cell->type[7] == 'P')
- arst = module->OrGate(NEW_ID, arst, past_arst);
- else
- arst = module->AndGate(NEW_ID, arst, past_arst);
+ if (!ff.val_init.is_fully_undef())
+ initvals.set_init(past_d, ff.val_init);
- if (cell->type[7] == 'P')
- module->addMuxGate(NEW_ID, qval, rstval, arst, sig_q);
+ if (!ff.is_fine)
+ qval = module->Mux(NEW_ID, past_q, past_d, clock_edge);
else
- module->addMuxGate(NEW_ID, rstval, qval, arst, sig_q);
+ qval = module->MuxGate(NEW_ID, past_q, past_d, clock_edge);
+ } else {
+ qval = past_q;
}
- else
- if (cell->type == ID($dffsr))
- {
- SigSpec qval = module->Mux(NEW_ID, past_q, past_d, clock_edge);
- SigSpec setval = cell->getPort(ID::SET);
- SigSpec clrval = cell->getPort(ID::CLR);
-
- if (!cell->parameters[ID::SET_POLARITY].as_bool())
- setval = module->Not(NEW_ID, setval);
-
- if (cell->parameters[ID::CLR_POLARITY].as_bool())
- clrval = module->Not(NEW_ID, clrval);
- qval = module->Or(NEW_ID, qval, setval);
- module->addAnd(NEW_ID, qval, clrval, sig_q);
- }
- else
- if (cell->type.in(ID($_DFFSR_NNN_), ID($_DFFSR_NNP_), ID($_DFFSR_NPN_), ID($_DFFSR_NPP_),
- ID($_DFFSR_PNN_), ID($_DFFSR_PNP_), ID($_DFFSR_PPN_), ID($_DFFSR_PPP_)))
- {
- SigSpec qval = module->MuxGate(NEW_ID, past_q, past_d, clock_edge);
- SigSpec setval = cell->getPort(ID::S);
- SigSpec clrval = cell->getPort(ID::R);
-
- if (cell->type[9] != 'P')
- setval = module->Not(NEW_ID, setval);
-
- if (cell->type[10] == 'P')
- clrval = module->Not(NEW_ID, clrval);
+ if (ff.has_aload) {
+ SigSpec sig_aload = wrap_async_control(module, ff.sig_aload, ff.pol_aload);
- qval = module->OrGate(NEW_ID, qval, setval);
- module->addAndGate(NEW_ID, qval, clrval, sig_q);
- }
- else if (cell->type == ID($dff))
- {
- module->addMux(NEW_ID, past_q, past_d, clock_edge, sig_q);
- }
- else
- {
- module->addMuxGate(NEW_ID, past_q, past_d, clock_edge, sig_q);
- }
-
- Const initval;
- bool assign_initval = false;
- for (int i = 0; i < GetSize(sig_d); i++) {
- SigBit qbit = sigmap(sig_q[i]);
- if (initbits.count(qbit)) {
- initval.bits.push_back(initbits.at(qbit));
- del_initbits.insert(qbit);
- } else
- initval.bits.push_back(State::Sx);
- if (initval.bits.back() != State::Sx)
- assign_initval = true;
+ 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);
}
- if (assign_initval) {
- past_d->attributes[ID::init] = initval;
- past_q->attributes[ID::init] = initval;
+ if (ff.has_sr) {
+ SigSpec setval = wrap_async_control(module, ff.sig_set, ff.pol_set);
+ SigSpec clrval = wrap_async_control(module, ff.sig_clr, ff.pol_clr);
+ 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) {
+ SigSpec arst = wrap_async_control(module, ff.sig_arst, ff.pol_arst);
+ 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);
}
-
- module->remove(cell);
- continue;
}
}
-
- for (auto wire : module->wires())
- if (wire->attributes.count(ID::init) > 0)
- {
- bool delete_initattr = true;
- Const initval = wire->attributes.at(ID::init);
- SigSpec initsig = sigmap(wire);
-
- for (int i = 0; i < GetSize(initval) && i < GetSize(initsig); i++)
- if (del_initbits.count(initsig[i]) > 0)
- initval[i] = State::Sx;
- else if (initval[i] != State::Sx)
- delete_initattr = false;
-
- if (delete_initattr)
- wire->attributes.erase(ID::init);
- else
- wire->attributes.at(ID::init) = initval;
- }
}
}
diff --git a/passes/sat/cutpoint.cc b/passes/sat/cutpoint.cc
index 6fc267d51..bca6a5ec6 100644
--- a/passes/sat/cutpoint.cc
+++ b/passes/sat/cutpoint.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
diff --git a/passes/sat/eval.cc b/passes/sat/eval.cc
index 085e7c5b8..05879426e 100644
--- a/passes/sat/eval.cc
+++ b/passes/sat/eval.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
@@ -18,7 +18,7 @@
*/
// [[CITE]] VlogHammer Verilog Regression Test Suite
-// http://www.clifford.at/yosys/vloghammer.html
+// https://yosyshq.net/yosys/vloghammer.html
#include "kernel/register.h"
#include "kernel/celltypes.h"
diff --git a/passes/sat/expose.cc b/passes/sat/expose.cc
index 2c65821cf..e7ec29ee4 100644
--- a/passes/sat/expose.cc
+++ b/passes/sat/expose.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
diff --git a/passes/sat/fmcombine.cc b/passes/sat/fmcombine.cc
index 5694a7473..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
@@ -114,8 +114,7 @@ struct FmcombineWorker
Cell *gold = import_prim_cell(cell, "_gold");
Cell *gate = import_prim_cell(cell, "_gate");
if (opts.initeq) {
- if (cell->type.in(ID($ff), ID($dff), ID($dffe),
- ID($dffsr), ID($adff), ID($dlatch), ID($dlatchsr))) {
+ 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);
diff --git a/passes/sat/fminit.cc b/passes/sat/fminit.cc
index c72e62548..5f4ec0068 100644
--- a/passes/sat/fminit.cc
+++ b/passes/sat/fminit.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
diff --git a/passes/sat/freduce.cc b/passes/sat/freduce.cc
index 762edfdfb..52e80f667 100644
--- a/passes/sat/freduce.cc
+++ b/passes/sat/freduce.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
@@ -27,6 +27,7 @@
#include <stdio.h>
#include <string.h>
#include <algorithm>
+#include <limits>
USING_YOSYS_NAMESPACE
PRIVATE_NAMESPACE_BEGIN
diff --git a/passes/sat/miter.cc b/passes/sat/miter.cc
index fe4a819f3..37efadfbd 100644
--- a/passes/sat/miter.cc
+++ b/passes/sat/miter.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
diff --git a/passes/sat/mutate.cc b/passes/sat/mutate.cc
index 15abee73e..42eb0c6d0 100644
--- a/passes/sat/mutate.cc
+++ b/passes/sat/mutate.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
@@ -439,7 +439,7 @@ void mutate_list(Design *design, const mutate_opts_t &opts, const string &filena
dict<SigBit, int> bit_user_cnt;
for (auto wire : module->wires()) {
- if (wire->name[0] == '\\' && wire->attributes.count(ID::src))
+ if (wire->name.isPublic() && wire->attributes.count(ID::src))
sigmap.add(wire);
}
@@ -468,7 +468,7 @@ void mutate_list(Design *design, const mutate_opts_t &opts, const string &filena
}
if (!bit.wire->name[0] != !sigbit.wire->name[0]) {
- if (bit.wire->name[0] == '\\')
+ if (bit.wire->name.isPublic())
sigmap.add(bit);
continue;
}
@@ -493,7 +493,7 @@ void mutate_list(Design *design, const mutate_opts_t &opts, const string &filena
entry.src.insert(s);
SigBit bit = sigmap(conn.second[i]);
- if (bit.wire && bit.wire->name[0] == '\\' && (cell->output(conn.first) || bit_user_cnt[bit] == 1)) {
+ if (bit.wire && bit.wire->name.isPublic() && (cell->output(conn.first) || bit_user_cnt[bit] == 1)) {
for (auto &s : bit.wire->get_strpool_attribute(ID::src))
entry.src.insert(s);
entry.wire = bit.wire->name;
diff --git a/passes/sat/qbfsat.cc b/passes/sat/qbfsat.cc
index 136259558..6db7d4b64 100644
--- a/passes/sat/qbfsat.cc
+++ b/passes/sat/qbfsat.cc
@@ -1,4 +1,4 @@
-/*
+/* -*- c++ -*-
* yosys -- Yosys Open SYnthesis Suite
*
* Copyright (C) 2020 Alberto Gonzalez <boqwxp@airmail.cc>
@@ -18,13 +18,8 @@
*/
#include "kernel/yosys.h"
-#include "kernel/celltypes.h"
#include "kernel/consteval.h"
-#include "kernel/log.h"
-#include "kernel/rtlil.h"
-#include "kernel/register.h"
-#include <algorithm>
-#include <numeric>
+#include "qbfsat.h"
USING_YOSYS_NAMESPACE
PRIVATE_NAMESPACE_BEGIN
@@ -36,156 +31,7 @@ static inline unsigned int difference(unsigned int a, unsigned int b) {
return a - b;
}
-struct QbfSolutionType {
- std::vector<std::string> stdout_lines;
- dict<pool<std::string>, std::string> hole_to_value;
- double solver_time;
- bool sat;
- bool unknown; //true if neither 'sat' nor 'unsat'
-
- QbfSolutionType() : solver_time(0.0), sat(false), unknown(true) {}
-};
-
-struct QbfSolveOptions {
- bool specialize, specialize_from_file, write_solution, nocleanup, dump_final_smt2, assume_outputs, assume_neg;
- bool nooptimize, nobisection;
- bool sat, unsat, show_smtbmc;
- enum Solver{Z3, Yices, CVC4} solver;
- enum OptimizationLevel{O0, O1, O2} oflag;
- int timeout;
- std::string specialize_soln_file;
- std::string write_soln_soln_file;
- std::string dump_final_smt2_file;
- size_t argidx;
- QbfSolveOptions() : specialize(false), specialize_from_file(false), write_solution(false),
- nocleanup(false), dump_final_smt2(false), assume_outputs(false), assume_neg(false),
- nooptimize(false), nobisection(false), sat(false), unsat(false), show_smtbmc(false),
- solver(Yices), oflag(O0), timeout(0), argidx(0) {};
-};
-
-std::string get_solver_name(const QbfSolveOptions &opt) {
- if (opt.solver == opt.Solver::Z3)
- return "z3";
- else if (opt.solver == opt.Solver::Yices)
- return "yices";
- else if (opt.solver == opt.Solver::CVC4)
- return "cvc4";
- else
- log_cmd_error("unknown solver specified.\n");
- return "";
-}
-
-void recover_solution(QbfSolutionType &sol) {
- YS_REGEX_TYPE sat_regex = YS_REGEX_COMPILE("Status: PASSED");
- YS_REGEX_TYPE unsat_regex = YS_REGEX_COMPILE("Solver Error.*model is not available");
- YS_REGEX_TYPE unsat_regex2 = YS_REGEX_COMPILE("Status: FAILED");
- YS_REGEX_TYPE timeout_regex = YS_REGEX_COMPILE("No solution found! \\(timeout\\)");
- YS_REGEX_TYPE timeout_regex2 = YS_REGEX_COMPILE("No solution found! \\(interrupted\\)");
- YS_REGEX_TYPE unknown_regex = YS_REGEX_COMPILE("No solution found! \\(unknown\\)");
- YS_REGEX_TYPE unknown_regex2 = YS_REGEX_COMPILE("Unexpected EOF response from solver");
- YS_REGEX_TYPE memout_regex = YS_REGEX_COMPILE("Solver Error:.*error \"out of memory\"");
- YS_REGEX_TYPE hole_value_regex = YS_REGEX_COMPILE_WITH_SUBS("Value for anyconst in [a-zA-Z0-9_]* \\(([^:]*:[^\\)]*)\\): (.*)");
-#ifndef NDEBUG
- YS_REGEX_TYPE hole_loc_regex = YS_REGEX_COMPILE("[^:]*:[0-9]+.[0-9]+-[0-9]+.[0-9]+");
- YS_REGEX_TYPE hole_val_regex = YS_REGEX_COMPILE("[0-9]+");
-#endif
- YS_REGEX_MATCH_TYPE m;
- bool sat_regex_found = false;
- bool unsat_regex_found = false;
- dict<std::string, bool> hole_value_recovered;
- for (const std::string &x : sol.stdout_lines) {
- if(YS_REGEX_NS::regex_search(x, m, hole_value_regex)) {
- std::string loc = m[1].str();
- std::string val = m[2].str();
-#ifndef NDEBUG
- log_assert(YS_REGEX_NS::regex_search(loc, hole_loc_regex));
- log_assert(YS_REGEX_NS::regex_search(val, hole_val_regex));
-#endif
- auto locs = split_tokens(loc, "|");
- pool<std::string> loc_pool(locs.begin(), locs.end());
- sol.hole_to_value[loc_pool] = val;
- }
- else if (YS_REGEX_NS::regex_search(x, sat_regex)) {
- sat_regex_found = true;
- sol.sat = true;
- sol.unknown = false;
- }
- else if (YS_REGEX_NS::regex_search(x, unsat_regex)) {
- unsat_regex_found = true;
- sol.sat = false;
- sol.unknown = false;
- }
- else if (YS_REGEX_NS::regex_search(x, memout_regex)) {
- sol.unknown = true;
- log_warning("solver ran out of memory\n");
- }
- else if (YS_REGEX_NS::regex_search(x, timeout_regex)) {
- sol.unknown = true;
- log_warning("solver timed out\n");
- }
- else if (YS_REGEX_NS::regex_search(x, timeout_regex2)) {
- sol.unknown = true;
- log_warning("solver timed out\n");
- }
- else if (YS_REGEX_NS::regex_search(x, unknown_regex)) {
- sol.unknown = true;
- log_warning("solver returned \"unknown\"\n");
- }
- else if (YS_REGEX_NS::regex_search(x, unsat_regex2)) {
- unsat_regex_found = true;
- sol.sat = false;
- sol.unknown = false;
- }
- else if (YS_REGEX_NS::regex_search(x, unknown_regex2)) {
- sol.unknown = true;
- }
- }
-#ifndef NDEBUG
- log_assert(!sol.unknown && sol.sat? sat_regex_found : true);
- log_assert(!sol.unknown && !sol.sat? unsat_regex_found : true);
-#endif
-}
-
-dict<std::pair<pool<std::string>, int>, RTLIL::SigBit> get_hole_loc_idx_sigbit_map(RTLIL::Module *module, const QbfSolutionType &sol) {
- dict<std::pair<pool<std::string>, int>, RTLIL::SigBit> hole_loc_idx_to_sigbit;
- pool<RTLIL::SigBit> anyconst_sigbits;
- dict<RTLIL::SigBit, RTLIL::SigBit> anyconst_sigbit_to_wire_sigbit;
-
- for (auto cell : module->cells()) {
- pool<std::string> cell_src = cell->get_strpool_attribute(ID::src);
- auto pos = sol.hole_to_value.find(cell_src);
- if (pos != sol.hole_to_value.end() && cell->type.in("$anyconst", "$anyseq")) {
- RTLIL::SigSpec port_y = cell->getPort(ID::Y);
- for (int i = GetSize(port_y) - 1; i >= 0; --i) {
- hole_loc_idx_to_sigbit[std::make_pair(pos->first, i)] = port_y[i];
- anyconst_sigbits.insert(port_y[i]);
- }
- }
- }
-
- for (auto &conn : module->connections()) {
- auto lhs = conn.first;
- auto rhs = conn.second;
- for (auto i = 0; i < GetSize(rhs); ++i) {
- if (anyconst_sigbits[rhs[i]]) {
- auto pos = anyconst_sigbit_to_wire_sigbit.find(rhs[i]);
- if (pos != anyconst_sigbit_to_wire_sigbit.end())
- log_cmd_error("conflicting names for hole $anyconst sigbit %s\n", log_signal(rhs[i]));
- anyconst_sigbit_to_wire_sigbit[rhs[i]] = lhs[i];
- }
- }
- }
-
- for (auto &it : hole_loc_idx_to_sigbit) {
- auto pos = anyconst_sigbit_to_wire_sigbit.find(it.second);
- if (pos != anyconst_sigbit_to_wire_sigbit.end())
- it.second = pos->second;
- }
-
- return hole_loc_idx_to_sigbit;
-}
-
-pool<std::string> validate_design_and_get_inputs(RTLIL::Module *module, const QbfSolveOptions &opt) {
+pool<std::string> validate_design_and_get_inputs(RTLIL::Module *module, bool assume_outputs) {
bool found_input = false;
bool found_hole = false;
bool found_1bit_output = false;
@@ -213,53 +59,16 @@ pool<std::string> validate_design_and_get_inputs(RTLIL::Module *module, const Qb
log_cmd_error("Did not find any existentially-quantified variables. Use 'sat' instead.\n");
if (!found_1bit_output && !found_assert_assume)
log_cmd_error("Did not find any single-bit outputs or $assert/$assume cells. Is this a miter circuit?\n");
- if (!found_assert_assume && !opt.assume_outputs)
+ if (!found_assert_assume && !assume_outputs)
log_cmd_error("Did not find any $assert/$assume cells. Single-bit outputs were found, but `-assume-outputs` was not specified.\n");
return input_wires;
}
-void write_solution(RTLIL::Module *module, const QbfSolutionType &sol, const std::string &file) {
- std::ofstream fout(file.c_str());
- if (!fout)
- log_cmd_error("could not open solution file for writing.\n");
-
- //There is a question here: How exactly shall we identify holes?
- //There are at least two reasonable options:
- //1. By the source location of the $anyconst cells
- //2. By the name(s) of the wire(s) connected to each SigBit of the $anyconst cell->getPort(ID::Y) SigSpec.
- //
- //Option 1 has the benefit of being very precise. There is very limited potential for confusion, as long
- //as the source attribute has been set. However, if the source attribute is not set, this won't work.
- //More importantly, we want to have the ability to port hole assignments to other modules with compatible
- //hole names and widths. Obviously in those cases source locations of the $anyconst cells will not match.
- //
- //Option 2 has the benefits previously described, but wire names can be changed automatically by
- //optimization or techmapping passes, especially when (ex/im)porting from BLIF for optimization with ABC.
- //
- //The approach taken here is to allow both options. We write the assignment information for each bit of
- //the solution on a separate line. Each line is of one of two forms:
- //
- //location bit name = value
- //location bit name [offset] = value
- //
- //where '[', ']', and '=' are literal symbols, "location" is the $anyconst cell source location attribute,
- //"bit" is the index of the $anyconst cell, "name" is the `wire->name` field of the SigBit corresponding
- //to the current bit of the $anyconst cell->getPort(ID::Y), "offset" is the `offset` field of that same
- //SigBit, and "value", which is either '0' or '1', represents the assignment for that bit.
- dict<std::pair<pool<std::string>, int>, RTLIL::SigBit> hole_loc_idx_to_sigbit = get_hole_loc_idx_sigbit_map(module, sol);
- for (auto &x : sol.hole_to_value) {
- std::string src_as_str = std::accumulate(x.first.begin(), x.first.end(), std::string(), [](const std::string &a, const std::string &b){return a + "|" + b;});
- for (auto i = 0; i < GetSize(x.second); ++i)
- fout << src_as_str.c_str() << " " << i << " " << log_signal(hole_loc_idx_to_sigbit[std::make_pair(x.first, i)]) << " = " << x.second[GetSize(x.second) - 1 - i] << std::endl;
- }
-}
-
void specialize_from_file(RTLIL::Module *module, const std::string &file) {
YS_REGEX_TYPE hole_bit_assn_regex = YS_REGEX_COMPILE_WITH_SUBS("^(.+) ([0-9]+) ([^ ]+) \\[([0-9]+)] = ([01])$");
YS_REGEX_TYPE hole_assn_regex = YS_REGEX_COMPILE_WITH_SUBS("^(.+) ([0-9]+) ([^ ]+) = ([01])$"); //if no index specified
YS_REGEX_MATCH_TYPE bit_m, m;
- //(hole_loc, hole_bit, hole_name, hole_offset) -> (value, found)
dict<pool<std::string>, RTLIL::Cell*> anyconst_loc_to_cell;
dict<RTLIL::SigBit, RTLIL::State> hole_assignments;
@@ -318,7 +127,7 @@ void specialize_from_file(RTLIL::Module *module, const std::string &file) {
}
void specialize(RTLIL::Module *module, const QbfSolutionType &sol, bool quiet = false) {
- dict<std::pair<pool<std::string>, int>, RTLIL::SigBit> hole_loc_idx_to_sigbit = get_hole_loc_idx_sigbit_map(module, sol);
+ auto hole_loc_idx_to_sigbit = sol.get_hole_loc_idx_sigbit_map(module);
pool<RTLIL::Cell *> anyconsts_to_remove;
for (auto cell : module->cells())
if (cell->type == "$anyconst")
@@ -348,30 +157,10 @@ void specialize(RTLIL::Module *module, const QbfSolutionType &sol, bool quiet =
}
}
-void dump_model(RTLIL::Module *module, const QbfSolutionType &sol) {
- log("Satisfiable model:\n");
- dict<std::pair<pool<std::string>, int>, RTLIL::SigBit> hole_loc_idx_to_sigbit = get_hole_loc_idx_sigbit_map(module, sol);
- for (auto &it : sol.hole_to_value) {
- pool<std::string> hole_loc = it.first;
- std::string hole_value = it.second;
-
- for (unsigned int i = 0; i < hole_value.size(); ++i) {
- int bit_idx = GetSize(hole_value) - 1 - i;
- auto it = hole_loc_idx_to_sigbit.find(std::make_pair(hole_loc, i));
- log_assert(it != hole_loc_idx_to_sigbit.end());
-
- RTLIL::SigBit hole_sigbit = it->second;
- log("\t%s = 1'b%c\n", log_signal(hole_sigbit), hole_value[bit_idx]);
- }
- }
-}
-
void allconstify_inputs(RTLIL::Module *module, const pool<std::string> &input_wires) {
for (auto &n : input_wires) {
RTLIL::Wire *input = module->wire(n);
-#ifndef NDEBUG
log_assert(input != nullptr);
-#endif
RTLIL::Cell *allconst = module->addCell("$allconst$" + n, "$allconst");
allconst->setParam(ID(WIDTH), input->width);
@@ -383,7 +172,7 @@ void allconstify_inputs(RTLIL::Module *module, const pool<std::string> &input_wi
module->fixup_ports();
}
-void assume_miter_outputs(RTLIL::Module *module, const QbfSolveOptions &opt) {
+void assume_miter_outputs(RTLIL::Module *module, bool assume_neg) {
std::vector<RTLIL::Wire *> wires_to_assume;
for (auto w : module->wires())
if (w->port_output && w->width == 1)
@@ -398,7 +187,7 @@ void assume_miter_outputs(RTLIL::Module *module, const QbfSolveOptions &opt) {
log("\n");
}
- if (opt.assume_neg) {
+ if (assume_neg) {
for (unsigned int i = 0; i < wires_to_assume.size(); ++i) {
RTLIL::SigSpec n_wire = module->LogicNot(wires_to_assume[i]->name.str() + "__n__qbfsat", wires_to_assume[i], false, wires_to_assume[i]->get_src_attribute());
wires_to_assume[i] = n_wire.as_wire();
@@ -418,9 +207,7 @@ void assume_miter_outputs(RTLIL::Module *module, const QbfSolveOptions &opt) {
wires_to_assume.swap(buf);
}
-#ifndef NDEBUG
log_assert(wires_to_assume.size() == 1);
-#endif
module->addAssume("$assume_qbfsat_miter_outputs", wires_to_assume[0], RTLIL::S1);
}
@@ -428,10 +215,17 @@ QbfSolutionType call_qbf_solver(RTLIL::Module *mod, const QbfSolveOptions &opt,
//Execute and capture stdout from `yosys-smtbmc -s z3 -t 1 -g --binary [--dump-smt2 <file>]`
QbfSolutionType ret;
const std::string yosys_smtbmc_exe = proc_self_dirname() + "yosys-smtbmc";
- const std::string smt2_command = "write_smt2 -stbv -wires " + tempdir_name + "/problem" + (iter_num != 0? stringf("%d", iter_num) : "") + ".smt2";
const std::string smtbmc_warning = "z3: WARNING:";
- const std::string smtbmc_cmd = yosys_smtbmc_exe + " -s " + (get_solver_name(opt)) + (opt.timeout != 0? stringf(" --timeout %d", opt.timeout) : "") + " -t 1 -g --binary " + (opt.dump_final_smt2? "--dump-smt2 " + opt.dump_final_smt2_file + " " : "") + tempdir_name + "/problem" + (iter_num != 0? stringf("%d", iter_num) : "") + ".smt2 2>&1";
-
+ const std::string smtbmc_cmd = stringf("%s -s %s %s -t 1 -g --binary %s %s/problem%d.smt2 2>&1",
+ yosys_smtbmc_exe.c_str(), opt.get_solver_name().c_str(),
+ (opt.timeout != 0? stringf("--timeout %d", opt.timeout) : "").c_str(),
+ (opt.dump_final_smt2? "--dump-smt2 " + opt.dump_final_smt2_file : "").c_str(),
+ tempdir_name.c_str(), iter_num);
+
+ std::string smt2_command = "write_smt2 -stbv -wires ";
+ for (auto &solver_opt : opt.solver_options)
+ smt2_command += stringf("-solver-option %s %s ", solver_opt.first.c_str(), solver_opt.second.c_str());
+ smt2_command += stringf("%s/problem%d.smt2", tempdir_name.c_str(), iter_num);
Pass::call(mod->design, smt2_command);
auto process_line = [&ret, &smtbmc_warning, &opt, &quiet](const std::string &line) {
@@ -451,13 +245,13 @@ QbfSolutionType call_qbf_solver(RTLIL::Module *mod, const QbfSolveOptions &opt,
ret.solver_time = (end - begin) / 1e9f;
if (!quiet) log("Solver finished in %.3f seconds.\n", ret.solver_time);
- recover_solution(ret);
+ ret.recover_solution();
return ret;
}
QbfSolutionType qbf_solve(RTLIL::Module *mod, const QbfSolveOptions &opt) {
QbfSolutionType ret, best_soln;
- const std::string tempdir_name = make_temp_dir("/tmp/yosys-z3-XXXXXX");
+ const std::string tempdir_name = make_temp_dir("/tmp/yosys-qbfsat-XXXXXX");
RTLIL::Module *module = mod;
RTLIL::Design *design = module->design;
std::string module_name = module->name.str();
@@ -468,10 +262,10 @@ QbfSolutionType qbf_solve(RTLIL::Module *mod, const QbfSolveOptions &opt) {
Pass::call(design, "design -push-copy");
//Replace input wires with wires assigned $allconst cells:
- pool<std::string> input_wires = validate_design_and_get_inputs(module, opt);
+ pool<std::string> input_wires = validate_design_and_get_inputs(module, opt.assume_outputs);
allconstify_inputs(module, input_wires);
if (opt.assume_outputs)
- assume_miter_outputs(module, opt);
+ assume_miter_outputs(module, opt.assume_neg);
//Find the wire to be optimized, if any:
for (auto wire : module->wires()) {
@@ -628,6 +422,13 @@ QbfSolveOptions parse_args(const std::vector<std::string> &args) {
}
continue;
}
+ else if (args[opt.argidx] == "-solver-option") {
+ if (args.size() <= opt.argidx + 2)
+ log_cmd_error("solver option name and value not fully specified.\n");
+ opt.solver_options.emplace(args[opt.argidx+1], args[opt.argidx+2]);
+ opt.argidx += 2;
+ continue;
+ }
else if (args[opt.argidx] == "-timeout") {
if (args.size() <= opt.argidx + 1)
log_cmd_error("timeout not specified.\n");
@@ -699,33 +500,6 @@ QbfSolveOptions parse_args(const std::vector<std::string> &args) {
return opt;
}
-void print_proof_failed()
-{
- log("\n");
- log(" ______ ___ ___ _ _ _ _ \n");
- log(" (_____ \\ / __) / __) (_) | | | |\n");
- log(" _____) )___ ___ ___ _| |__ _| |__ _____ _| | _____ __| | |\n");
- log(" | ____/ ___) _ \\ / _ (_ __) (_ __|____ | | || ___ |/ _ |_|\n");
- log(" | | | | | |_| | |_| || | | | / ___ | | || ____( (_| |_ \n");
- log(" |_| |_| \\___/ \\___/ |_| |_| \\_____|_|\\_)_____)\\____|_|\n");
- log("\n");
-}
-
-void print_qed()
-{
- log("\n");
- log(" /$$$$$$ /$$$$$$$$ /$$$$$$$ \n");
- log(" /$$__ $$ | $$_____/ | $$__ $$ \n");
- log(" | $$ \\ $$ | $$ | $$ \\ $$ \n");
- log(" | $$ | $$ | $$$$$ | $$ | $$ \n");
- log(" | $$ | $$ | $$__/ | $$ | $$ \n");
- log(" | $$/$$ $$ | $$ | $$ | $$ \n");
- log(" | $$$$$$/ /$$| $$$$$$$$ /$$| $$$$$$$//$$\n");
- log(" \\____ $$$|__/|________/|__/|_______/|__/\n");
- log(" \\__/ \n");
- log("\n");
-}
-
struct QbfSatPass : public Pass {
QbfSatPass() : Pass("qbfsat", "solve a 2QBF-SAT problem in the circuit") { }
void help() override
@@ -767,9 +541,14 @@ struct QbfSatPass : public Pass {
log("\n");
log(" -solver <solver>\n");
log(" Use a particular solver. Choose one of: \"z3\", \"yices\", and \"cvc4\".\n");
+ log(" (default: yices)\n");
+ log("\n");
+ log(" -solver-option <name> <value>\n");
+ log(" Set the specified solver option in the SMT-LIBv2 problem file.\n");
log("\n");
log(" -timeout <value>\n");
log(" Set the per-iteration timeout in seconds.\n");
+ log(" (default: no timeout)\n");
log("\n");
log(" -O0, -O1, -O2\n");
log(" Control the use of ABC to simplify the QBF-SAT problem before solving.\n");
@@ -827,12 +606,12 @@ struct QbfSatPass : public Pass {
else if (ret.sat) {
print_qed();
if (opt.write_solution) {
- write_solution(module, ret, opt.write_soln_soln_file);
+ ret.write_solution(module, opt.write_soln_soln_file);
}
if (opt.specialize) {
specialize(module, ret);
} else {
- dump_model(module, ret);
+ ret.dump_model(module);
}
if (opt.unsat)
log_cmd_error("expected problem to be UNSAT\n");
diff --git a/passes/sat/qbfsat.h b/passes/sat/qbfsat.h
new file mode 100644
index 000000000..c96c6f818
--- /dev/null
+++ b/passes/sat/qbfsat.h
@@ -0,0 +1,253 @@
+/* -*- c++ -*-
+ * yosys -- Yosys Open SYnthesis Suite
+ *
+ * Copyright (C) 2020 Alberto Gonzalez <boqwxp@airmail.cc>
+ *
+ * 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.
+ *
+ */
+
+#ifndef QBFSAT_H
+#define QBFSAT_H
+
+#include "kernel/yosys.h"
+#include <numeric>
+
+YOSYS_NAMESPACE_BEGIN
+
+struct QbfSolveOptions {
+ bool specialize = false, specialize_from_file = false, write_solution = false, nocleanup = false;
+ bool dump_final_smt2 = false, assume_outputs = false, assume_neg = false, nooptimize = false;
+ bool nobisection = false, sat = false, unsat = false, show_smtbmc = false;
+ enum Solver{Z3, Yices, CVC4} solver = Yices;
+ enum OptimizationLevel{O0, O1, O2} oflag = O0;
+ dict<std::string, std::string> solver_options;
+ int timeout = 0;
+ std::string specialize_soln_file = "";
+ std::string write_soln_soln_file = "";
+ std::string dump_final_smt2_file = "";
+ size_t argidx = 0;
+
+ std::string get_solver_name() const {
+ if (solver == Solver::Z3)
+ return "z3";
+ else if (solver == Solver::Yices)
+ return "yices";
+ else if (solver == Solver::CVC4)
+ return "cvc4";
+
+ log_cmd_error("unknown solver specified.\n");
+ return "";
+ }
+};
+
+struct QbfSolutionType {
+ std::vector<std::string> stdout_lines = {};
+ dict<pool<std::string>, std::string> hole_to_value = {};
+ double solver_time = 0;
+ bool sat = false;
+ bool unknown = true; //true if neither 'sat' nor 'unsat'
+
+ dict<std::pair<pool<std::string>, int>, RTLIL::SigBit> get_hole_loc_idx_sigbit_map(RTLIL::Module *module) const {
+ dict<std::pair<pool<std::string>, int>, RTLIL::SigBit> hole_loc_idx_to_sigbit;
+ pool<RTLIL::SigBit> anyconst_sigbits;
+ dict<RTLIL::SigBit, RTLIL::SigBit> anyconst_sigbit_to_wire_sigbit;
+
+ for (auto cell : module->cells()) {
+ pool<std::string> cell_src = cell->get_strpool_attribute(ID::src);
+ auto pos = hole_to_value.find(cell_src);
+ if (pos != hole_to_value.end() && cell->type.in("$anyconst", "$anyseq")) {
+ RTLIL::SigSpec port_y = cell->getPort(ID::Y);
+ for (int i = GetSize(port_y) - 1; i >= 0; --i) {
+ hole_loc_idx_to_sigbit[std::make_pair(pos->first, i)] = port_y[i];
+ anyconst_sigbits.insert(port_y[i]);
+ }
+ }
+ }
+
+ for (auto &conn : module->connections()) {
+ auto lhs = conn.first;
+ auto rhs = conn.second;
+ for (auto i = 0; i < GetSize(rhs); ++i) {
+ if (anyconst_sigbits[rhs[i]]) {
+ auto pos = anyconst_sigbit_to_wire_sigbit.find(rhs[i]);
+ if (pos != anyconst_sigbit_to_wire_sigbit.end())
+ log_cmd_error("conflicting names for hole $anyconst sigbit %s\n", log_signal(rhs[i]));
+ anyconst_sigbit_to_wire_sigbit[rhs[i]] = lhs[i];
+ }
+ }
+ }
+
+ for (auto &it : hole_loc_idx_to_sigbit) {
+ auto pos = anyconst_sigbit_to_wire_sigbit.find(it.second);
+ if (pos != anyconst_sigbit_to_wire_sigbit.end())
+ it.second = pos->second;
+ }
+
+ return hole_loc_idx_to_sigbit;
+ }
+
+ void dump_model(RTLIL::Module *module) const {
+ log("Satisfiable model:\n");
+ auto hole_loc_idx_to_sigbit = get_hole_loc_idx_sigbit_map(module);
+ for (auto &it : hole_to_value) {
+ pool<std::string> hole_loc = it.first;
+ std::string hole_value = it.second;
+
+ for (unsigned int i = 0; i < hole_value.size(); ++i) {
+ int bit_idx = GetSize(hole_value) - 1 - i;
+ auto it = hole_loc_idx_to_sigbit.find(std::make_pair(hole_loc, i));
+ log_assert(it != hole_loc_idx_to_sigbit.end());
+
+ RTLIL::SigBit hole_sigbit = it->second;
+ log("\t%s = 1'b%c\n", log_signal(hole_sigbit), hole_value[bit_idx]);
+ }
+ }
+ }
+
+ void write_solution(RTLIL::Module *module, const std::string &file) const {
+ std::ofstream fout(file.c_str());
+ if (!fout)
+ log_cmd_error("could not open solution file for writing.\n");
+
+ //There is a question here: How exactly shall we identify holes?
+ //There are at least two reasonable options:
+ //1. By the source location of the $anyconst cells
+ //2. By the name(s) of the wire(s) connected to each SigBit of the $anyconst cell->getPort(ID::Y) SigSpec.
+ //
+ //Option 1 has the benefit of being very precise. There is very limited potential for confusion, as long
+ //as the source attribute has been set. However, if the source attribute is not set, this won't work.
+ //More importantly, we want to have the ability to port hole assignments to other modules with compatible
+ //hole names and widths. Obviously in those cases source locations of the $anyconst cells will not match.
+ //
+ //Option 2 has the benefits previously described, but wire names can be changed automatically by
+ //optimization or techmapping passes, especially when (ex/im)porting from BLIF for optimization with ABC.
+ //
+ //The approach taken here is to allow both options. We write the assignment information for each bit of
+ //the solution on a separate line. Each line is of one of two forms:
+ //
+ //location bit name = value
+ //location bit name [offset] = value
+ //
+ //where '[', ']', and '=' are literal symbols, "location" is the $anyconst cell source location attribute,
+ //"bit" is the index of the $anyconst cell, "name" is the `wire->name` field of the SigBit corresponding
+ //to the current bit of the $anyconst cell->getPort(ID::Y), "offset" is the `offset` field of that same
+ //SigBit, and "value", which is either '0' or '1', represents the assignment for that bit.
+ auto hole_loc_idx_to_sigbit = get_hole_loc_idx_sigbit_map(module);
+ for (auto &x : hole_to_value) {
+ std::string src_as_str = std::accumulate(x.first.begin(), x.first.end(), std::string(), [](const std::string &a, const std::string &b){return a + "|" + b;});
+ for (auto i = 0; i < GetSize(x.second); ++i)
+ fout << src_as_str.c_str() << " " << i << " " << log_signal(hole_loc_idx_to_sigbit[std::make_pair(x.first, i)]) << " = " << x.second[GetSize(x.second) - 1 - i] << std::endl;
+ }
+ }
+
+ void recover_solution() {
+ YS_REGEX_TYPE sat_regex = YS_REGEX_COMPILE("Status: PASSED");
+ YS_REGEX_TYPE unsat_regex = YS_REGEX_COMPILE("Solver Error.*model is not available");
+ YS_REGEX_TYPE unsat_regex2 = YS_REGEX_COMPILE("Status: FAILED");
+ YS_REGEX_TYPE timeout_regex = YS_REGEX_COMPILE("No solution found! \\(timeout\\)");
+ YS_REGEX_TYPE timeout_regex2 = YS_REGEX_COMPILE("No solution found! \\(interrupted\\)");
+ YS_REGEX_TYPE unknown_regex = YS_REGEX_COMPILE("No solution found! \\(unknown\\)");
+ YS_REGEX_TYPE unknown_regex2 = YS_REGEX_COMPILE("Unexpected EOF response from solver");
+ YS_REGEX_TYPE memout_regex = YS_REGEX_COMPILE("Solver Error:.*error \"out of memory\"");
+ YS_REGEX_TYPE hole_value_regex = YS_REGEX_COMPILE_WITH_SUBS("Value for anyconst in [a-zA-Z0-9_]* \\(([^:]*:[^\\)]*)\\): (.*)");
+#ifndef NDEBUG
+ YS_REGEX_TYPE hole_loc_regex = YS_REGEX_COMPILE("[^:]*:[0-9]+.[0-9]+-[0-9]+.[0-9]+");
+ YS_REGEX_TYPE hole_val_regex = YS_REGEX_COMPILE("[0-9]+");
+#endif
+ YS_REGEX_MATCH_TYPE m;
+ bool sat_regex_found = false;
+ bool unsat_regex_found = false;
+ dict<std::string, bool> hole_value_recovered;
+ for (const std::string &x : stdout_lines) {
+ if(YS_REGEX_NS::regex_search(x, m, hole_value_regex)) {
+ std::string loc = m[1].str();
+ std::string val = m[2].str();
+#ifndef NDEBUG
+ log_assert(YS_REGEX_NS::regex_search(loc, hole_loc_regex));
+ log_assert(YS_REGEX_NS::regex_search(val, hole_val_regex));
+#endif
+ auto locs = split_tokens(loc, "|");
+ pool<std::string> loc_pool(locs.begin(), locs.end());
+ hole_to_value[loc_pool] = val;
+ }
+ else if (YS_REGEX_NS::regex_search(x, sat_regex)) {
+ sat_regex_found = true;
+ sat = true;
+ unknown = false;
+ }
+ else if (YS_REGEX_NS::regex_search(x, unsat_regex)) {
+ unsat_regex_found = true;
+ sat = false;
+ unknown = false;
+ }
+ else if (YS_REGEX_NS::regex_search(x, memout_regex)) {
+ unknown = true;
+ log_warning("solver ran out of memory\n");
+ }
+ else if (YS_REGEX_NS::regex_search(x, timeout_regex)) {
+ unknown = true;
+ log_warning("solver timed out\n");
+ }
+ else if (YS_REGEX_NS::regex_search(x, timeout_regex2)) {
+ unknown = true;
+ log_warning("solver timed out\n");
+ }
+ else if (YS_REGEX_NS::regex_search(x, unknown_regex)) {
+ unknown = true;
+ log_warning("solver returned \"unknown\"\n");
+ }
+ else if (YS_REGEX_NS::regex_search(x, unsat_regex2)) {
+ unsat_regex_found = true;
+ sat = false;
+ unknown = false;
+ }
+ else if (YS_REGEX_NS::regex_search(x, unknown_regex2)) {
+ unknown = true;
+ }
+ }
+ log_assert(!unknown && sat? sat_regex_found : true);
+ log_assert(!unknown && !sat? unsat_regex_found : true);
+ }
+};
+
+void print_proof_failed()
+{
+ log("\n");
+ log(" ______ ___ ___ _ _ _ _ \n");
+ log(" (_____ \\ / __) / __) (_) | | | |\n");
+ log(" _____) )___ ___ ___ _| |__ _| |__ _____ _| | _____ __| | |\n");
+ log(" | ____/ ___) _ \\ / _ (_ __) (_ __|____ | | || ___ |/ _ |_|\n");
+ log(" | | | | | |_| | |_| || | | | / ___ | | || ____( (_| |_ \n");
+ log(" |_| |_| \\___/ \\___/ |_| |_| \\_____|_|\\_)_____)\\____|_|\n");
+ log("\n");
+}
+
+void print_qed()
+{
+ log("\n");
+ log(" /$$$$$$ /$$$$$$$$ /$$$$$$$ \n");
+ log(" /$$__ $$ | $$_____/ | $$__ $$ \n");
+ log(" | $$ \\ $$ | $$ | $$ \\ $$ \n");
+ log(" | $$ | $$ | $$$$$ | $$ | $$ \n");
+ log(" | $$ | $$ | $$__/ | $$ | $$ \n");
+ log(" | $$/$$ $$ | $$ | $$ | $$ \n");
+ log(" | $$$$$$/ /$$| $$$$$$$$ /$$| $$$$$$$//$$\n");
+ log(" \\____ $$$|__/|________/|__/|_______/|__/\n");
+ log(" \\__/ \n");
+ log("\n");
+}
+
+YOSYS_NAMESPACE_END
+
+#endif
diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc
index d7bf125d1..df2725b3c 100644
--- a/passes/sat/sat.cc
+++ b/passes/sat/sat.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
@@ -1365,7 +1365,7 @@ struct SatPass : public Pass {
if (show_public) {
for (auto wire : module->wires())
- if (wire->name[0] == '\\')
+ if (wire->name.isPublic())
shows.push_back(wire->name.str());
}
diff --git a/passes/sat/sim.cc b/passes/sat/sim.cc
index fb496ff87..a7c109374 100644
--- a/passes/sat/sim.cc
+++ b/passes/sat/sim.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
@@ -20,10 +20,50 @@
#include "kernel/yosys.h"
#include "kernel/sigtools.h"
#include "kernel/celltypes.h"
+#include "kernel/mem.h"
+#include "kernel/fstdata.h"
+
+#include <ctime>
USING_YOSYS_NAMESPACE
PRIVATE_NAMESPACE_BEGIN
+enum class SimulationMode {
+ sim,
+ cmp,
+ gold,
+ gate,
+};
+
+static const std::map<std::string, int> g_units =
+{
+ { "", -9 }, // default is ns
+ { "s", 0 },
+ { "ms", -3 },
+ { "us", -6 },
+ { "ns", -9 },
+ { "ps", -12 },
+ { "fs", -15 },
+ { "as", -18 },
+ { "zs", -21 },
+};
+
+static double stringToTime(std::string str)
+{
+ if (str=="END") return -1;
+
+ char *endptr;
+ long value = strtol(str.c_str(), &endptr, 10);
+
+ if (g_units.find(endptr)==g_units.end())
+ log_error("Cannot parse '%s', bad unit '%s'\n", str.c_str(), endptr);
+
+ if (value < 0)
+ log_error("Time value '%s' must be positive\n", str.c_str());
+
+ return value * pow(10.0, g_units.at(endptr));
+}
+
struct SimShared
{
bool debug = false;
@@ -31,6 +71,11 @@ struct SimShared
bool writeback = false;
bool zinit = false;
int rstlen = 1;
+ FstData *fst = nullptr;
+ double start_time = 0;
+ double stop_time = -1;
+ SimulationMode sim_mode = SimulationMode::sim;
+ bool cycles_set = false;
};
void zinit(State &v)
@@ -48,7 +93,8 @@ void zinit(Const &v)
struct SimInstance
{
SimShared *shared;
-
+
+ std::string scope;
Module *module;
Cell *instance;
@@ -62,6 +108,7 @@ struct SimInstance
pool<SigBit> dirty_bits;
pool<Cell*> dirty_cells;
+ pool<IdString> dirty_memories;
pool<SimInstance*, hash_ptr_ops> dirty_children;
struct ff_state_t
@@ -72,21 +119,27 @@ struct SimInstance
struct mem_state_t
{
- Const past_wr_clk;
- Const past_wr_en;
- Const past_wr_addr;
- Const past_wr_data;
+ Mem *mem;
+ std::vector<Const> past_wr_clk;
+ std::vector<Const> past_wr_en;
+ std::vector<Const> past_wr_addr;
+ std::vector<Const> past_wr_data;
Const data;
};
dict<Cell*, ff_state_t> ff_database;
- dict<Cell*, mem_state_t> mem_database;
+ dict<IdString, mem_state_t> mem_database;
pool<Cell*> formal_database;
+ dict<Cell*, IdString> mem_cells;
+
+ std::vector<Mem> memories;
dict<Wire*, pair<int, Const>> vcd_database;
+ dict<Wire*, pair<fstHandle, Const>> fst_database;
+ dict<Wire*, fstHandle> fst_handles;
- SimInstance(SimShared *shared, Module *module, Cell *instance = nullptr, SimInstance *parent = nullptr) :
- shared(shared), module(module), instance(instance), parent(parent), sigmap(module)
+ SimInstance(SimShared *shared, std::string scope, Module *module, Cell *instance = nullptr, SimInstance *parent = nullptr) :
+ shared(shared), scope(scope), module(module), instance(instance), parent(parent), sigmap(module)
{
log_assert(module);
@@ -108,6 +161,13 @@ struct SimInstance
}
}
+ if ((shared->fst) && !(shared->hide_internal && wire->name[0] == '$')) {
+ fstHandle id = shared->fst->getHandle(scope + "." + RTLIL::unescape_id(wire->name));
+ if (id==0 && wire->name.isPublic())
+ log_warning("Unable to found wire %s in input file.\n", (scope + "." + RTLIL::unescape_id(wire->name)).c_str());
+ fst_handles[wire] = id;
+ }
+
if (wire->attributes.count(ID::init)) {
Const initval = wire->attributes.at(ID::init);
for (int i = 0; i < GetSize(sig) && i < GetSize(initval); i++)
@@ -118,12 +178,25 @@ struct SimInstance
}
}
+ memories = Mem::get_all_memories(module);
+ for (auto &mem : memories) {
+ auto &mdb = mem_database[mem.memid];
+ mdb.mem = &mem;
+ for (auto &port : mem.wr_ports) {
+ mdb.past_wr_clk.push_back(Const(State::Sx));
+ mdb.past_wr_en.push_back(Const(State::Sx, GetSize(port.en)));
+ mdb.past_wr_addr.push_back(Const(State::Sx, GetSize(port.addr)));
+ mdb.past_wr_data.push_back(Const(State::Sx, GetSize(port.data)));
+ }
+ mdb.data = mem.get_init_data();
+ }
+
for (auto cell : module->cells())
{
Module *mod = module->design->module(cell->type);
if (mod != nullptr) {
- dirty_children.insert(new SimInstance(shared, mod, cell, this));
+ dirty_children.insert(new SimInstance(shared, scope + "." + RTLIL::unescape_id(cell->name), mod, cell, this));
}
for (auto &port : cell->connections()) {
@@ -143,29 +216,9 @@ struct SimInstance
ff_database[cell] = ff;
}
- if (cell->type == ID($mem))
+ if (cell->is_mem_cell())
{
- mem_state_t mem;
-
- mem.past_wr_clk = Const(State::Sx, GetSize(cell->getPort(ID::WR_CLK)));
- mem.past_wr_en = Const(State::Sx, GetSize(cell->getPort(ID::WR_EN)));
- mem.past_wr_addr = Const(State::Sx, GetSize(cell->getPort(ID::WR_ADDR)));
- mem.past_wr_data = Const(State::Sx, GetSize(cell->getPort(ID::WR_DATA)));
-
- mem.data = cell->getParam(ID::INIT);
- int sz = cell->getParam(ID::SIZE).as_int() * cell->getParam(ID::WIDTH).as_int();
-
- if (GetSize(mem.data) > sz)
- mem.data.bits.resize(sz);
-
- while (GetSize(mem.data) < sz)
- mem.data.bits.push_back(State::Sx);
-
- mem_database[cell] = mem;
- }
- if (cell->type.in(ID($memwr),ID($memrd)))
- {
- log_error("$memrd and $memwr cells have to be merged to stand-alone $mem cells (execute memory_collect pass)\n");
+ mem_cells[cell] = cell->parameters.at(ID::MEMID).decode_string();
}
if (cell->type.in(ID($assert), ID($cover), ID($assume))) {
formal_database.insert(cell);
@@ -188,7 +241,8 @@ struct SimInstance
for (auto &it : mem_database) {
mem_state_t &mem = it.second;
- zinit(mem.past_wr_en);
+ for (auto &val : mem.past_wr_en)
+ zinit(val);
zinit(mem.data);
}
}
@@ -259,37 +313,9 @@ struct SimInstance
if (formal_database.count(cell))
return;
- if (mem_database.count(cell))
+ if (mem_cells.count(cell))
{
- mem_state_t &mem = mem_database.at(cell);
-
- int num_rd_ports = cell->getParam(ID::RD_PORTS).as_int();
-
- int size = cell->getParam(ID::SIZE).as_int();
- int offset = cell->getParam(ID::OFFSET).as_int();
- int abits = cell->getParam(ID::ABITS).as_int();
- int width = cell->getParam(ID::WIDTH).as_int();
-
- if (cell->getParam(ID::RD_CLK_ENABLE).as_bool())
- log_error("Memory %s.%s has clocked read ports. Run 'memory' with -nordff.\n", log_id(module), log_id(cell));
-
- SigSpec rd_addr_sig = cell->getPort(ID::RD_ADDR);
- SigSpec rd_data_sig = cell->getPort(ID::RD_DATA);
-
- for (int port_idx = 0; port_idx < num_rd_ports; port_idx++)
- {
- Const addr = get_state(rd_addr_sig.extract(port_idx*abits, abits));
- Const data = Const(State::Sx, width);
-
- if (addr.is_fully_def()) {
- int index = addr.as_int() - offset;
- if (index >= 0 && index < size)
- data = mem.data.extract(index*width, width);
- }
-
- set_state(rd_data_sig.extract(port_idx*width, width), data);
- }
-
+ dirty_memories.insert(mem_cells[cell]);
return;
}
@@ -297,7 +323,7 @@ struct SimInstance
{
auto child = children.at(cell);
for (auto &conn: cell->connections())
- if (cell->input(conn.first)) {
+ if (cell->input(conn.first) && GetSize(conn.second)) {
Const value = get_state(conn.second);
child->set_state(child->module->wire(conn.first), value);
}
@@ -339,6 +365,12 @@ struct SimInstance
return;
}
+ // (A,S -> Y) cells
+ if (has_a && !has_b && !has_c && !has_d && has_s && has_y) {
+ set_state(sig_y, CellTypes::eval(cell, get_state(sig_a), get_state(sig_s)));
+ return;
+ }
+
// (A,B,S -> Y) cells
if (has_a && has_b && !has_c && !has_d && has_s && has_y) {
set_state(sig_y, CellTypes::eval(cell, get_state(sig_a), get_state(sig_b), get_state(sig_s)));
@@ -352,6 +384,29 @@ struct SimInstance
log_error("Unsupported cell type: %s (%s.%s)\n", log_id(cell->type), log_id(module), log_id(cell));
}
+ void update_memory(IdString id) {
+ auto &mdb = mem_database[id];
+ auto &mem = *mdb.mem;
+
+ for (int port_idx = 0; port_idx < GetSize(mem.rd_ports); port_idx++)
+ {
+ auto &port = mem.rd_ports[port_idx];
+ Const addr = get_state(port.addr);
+ Const data = Const(State::Sx, mem.width << port.wide_log2);
+
+ if (port.clk_enable)
+ log_error("Memory %s.%s has clocked read ports. Run 'memory' with -nordff.\n", log_id(module), log_id(mem.memid));
+
+ if (addr.is_fully_def()) {
+ int index = addr.as_int() - mem.start_offset;
+ if (index >= 0 && index < mem.size)
+ data = mdb.data.extract(index*mem.width, mem.width << port.wide_log2);
+ }
+
+ set_state(port.data, data);
+ }
+ }
+
void update_ph1()
{
pool<Cell*> queue_cells;
@@ -383,6 +438,10 @@ struct SimInstance
continue;
}
+ for (auto &memid : dirty_memories)
+ update_memory(memid);
+ dirty_memories.clear();
+
for (auto wire : queue_outports)
if (instance->hasPort(wire->name)) {
Const value = get_state(wire);
@@ -426,50 +485,40 @@ struct SimInstance
for (auto &it : mem_database)
{
- Cell *cell = it.first;
- mem_state_t &mem = it.second;
-
- int num_wr_ports = cell->getParam(ID::WR_PORTS).as_int();
-
- int size = cell->getParam(ID::SIZE).as_int();
- int offset = cell->getParam(ID::OFFSET).as_int();
- int abits = cell->getParam(ID::ABITS).as_int();
- int width = cell->getParam(ID::WIDTH).as_int();
+ mem_state_t &mdb = it.second;
+ auto &mem = *mdb.mem;
- Const wr_clk_enable = cell->getParam(ID::WR_CLK_ENABLE);
- Const wr_clk_polarity = cell->getParam(ID::WR_CLK_POLARITY);
- Const current_wr_clk = get_state(cell->getPort(ID::WR_CLK));
-
- for (int port_idx = 0; port_idx < num_wr_ports; port_idx++)
+ for (int port_idx = 0; port_idx < GetSize(mem.wr_ports); port_idx++)
{
+ auto &port = mem.wr_ports[port_idx];
Const addr, data, enable;
- if (wr_clk_enable[port_idx] == State::S0)
+ if (!port.clk_enable)
{
- addr = get_state(cell->getPort(ID::WR_ADDR).extract(port_idx*abits, abits));
- data = get_state(cell->getPort(ID::WR_DATA).extract(port_idx*width, width));
- enable = get_state(cell->getPort(ID::WR_EN).extract(port_idx*width, width));
+ addr = get_state(port.addr);
+ data = get_state(port.data);
+ enable = get_state(port.en);
}
else
{
- if (wr_clk_polarity[port_idx] == State::S1 ?
- (mem.past_wr_clk[port_idx] == State::S1 || current_wr_clk[port_idx] != State::S1) :
- (mem.past_wr_clk[port_idx] == State::S0 || current_wr_clk[port_idx] != State::S0))
+ if (port.clk_polarity ?
+ (mdb.past_wr_clk[port_idx] == State::S1 || get_state(port.clk) != State::S1) :
+ (mdb.past_wr_clk[port_idx] == State::S0 || get_state(port.clk) != State::S0))
continue;
- addr = mem.past_wr_addr.extract(port_idx*abits, abits);
- data = mem.past_wr_data.extract(port_idx*width, width);
- enable = mem.past_wr_en.extract(port_idx*width, width);
+ addr = mdb.past_wr_addr[port_idx];
+ data = mdb.past_wr_data[port_idx];
+ enable = mdb.past_wr_en[port_idx];
}
if (addr.is_fully_def())
{
- int index = addr.as_int() - offset;
- if (index >= 0 && index < size)
- for (int i = 0; i < width; i++)
- if (enable[i] == State::S1 && mem.data.bits.at(index*width+i) != data[i]) {
- mem.data.bits.at(index*width+i) = data[i];
- dirty_cells.insert(cell);
+ int index = addr.as_int() - mem.start_offset;
+ if (index >= 0 && index < mem.size)
+ for (int i = 0; i < (mem.width << port.wide_log2); i++)
+ if (enable[i] == State::S1 && mdb.data.bits.at(index*mem.width+i) != data[i]) {
+ mdb.data.bits.at(index*mem.width+i) = data[i];
+ dirty_memories.insert(mem.memid);
did_something = true;
}
}
@@ -500,13 +549,15 @@ struct SimInstance
for (auto &it : mem_database)
{
- Cell *cell = it.first;
mem_state_t &mem = it.second;
- mem.past_wr_clk = get_state(cell->getPort(ID::WR_CLK));
- mem.past_wr_en = get_state(cell->getPort(ID::WR_EN));
- mem.past_wr_addr = get_state(cell->getPort(ID::WR_ADDR));
- mem.past_wr_data = get_state(cell->getPort(ID::WR_DATA));
+ for (int i = 0; i < GetSize(mem.mem->wr_ports); i++) {
+ auto &port = mem.mem->wr_ports[i];
+ mem.past_wr_clk[i] = get_state(port.clk);
+ mem.past_wr_en[i] = get_state(port.en);
+ mem.past_wr_addr[i] = get_state(port.addr);
+ mem.past_wr_data[i] = get_state(port.data);
+ }
}
for (auto cell : formal_database)
@@ -561,17 +612,14 @@ struct SimInstance
for (auto &it : mem_database)
{
- Cell *cell = it.first;
mem_state_t &mem = it.second;
- Const initval = mem.data;
-
- while (GetSize(initval) >= 2) {
- if (initval[GetSize(initval)-1] != State::Sx) break;
- if (initval[GetSize(initval)-2] != State::Sx) break;
- initval.bits.pop_back();
- }
-
- cell->setParam(ID::INIT, initval);
+ mem.mem->clear_inits();
+ MemInit minit;
+ minit.addr = mem.mem->start_offset;
+ minit.data = mem.data;
+ minit.en = Const(State::S1, mem.mem->width);
+ mem.mem->inits.push_back(minit);
+ mem.mem->emit();
}
for (auto it : children)
@@ -626,13 +674,125 @@ struct SimInstance
for (auto child : children)
child.second->write_vcd_step(f);
}
+
+ void write_fst_header(struct fstContext *f)
+ {
+ fstWriterSetScope(f, FST_ST_VCD_MODULE, stringf("%s",log_id(name())).c_str(), nullptr);
+ for (auto wire : module->wires())
+ {
+ if (shared->hide_internal && wire->name[0] == '$')
+ continue;
+
+ fstHandle id = fstWriterCreateVar(f, FST_VT_VCD_WIRE, FST_VD_IMPLICIT, GetSize(wire),
+ stringf("%s%s", wire->name[0] == '$' ? "\\" : "", log_id(wire)).c_str(), 0);
+ fst_database[wire] = make_pair(id, Const());
+ }
+
+ for (auto child : children)
+ child.second->write_fst_header(f);
+
+ fstWriterSetUpscope(f);
+ }
+
+ void write_fst_step(struct fstContext *f)
+ {
+ for (auto &it : fst_database)
+ {
+ Wire *wire = it.first;
+ Const value = get_state(wire);
+ fstHandle id = it.second.first;
+
+ if (it.second.second == value)
+ continue;
+
+ it.second.second = value;
+ std::stringstream ss;
+ for (int i = GetSize(value)-1; i >= 0; i--) {
+ switch (value[i]) {
+ case State::S0: ss << "0"; break;
+ case State::S1: ss << "1"; break;
+ case State::Sx: ss << "x"; break;
+ default: ss << "z";
+ }
+ }
+ fstWriterEmitValueChange(f, id, ss.str().c_str());
+ }
+
+ for (auto child : children)
+ child.second->write_fst_step(f);
+ }
+
+ void setInitState(uint64_t time)
+ {
+ for (auto &it : ff_database)
+ {
+ Cell *cell = it.first;
+
+ SigSpec qsig = cell->getPort(ID::Q);
+ if (qsig.is_wire()) {
+ IdString name = qsig.as_wire()->name;
+ fstHandle id = shared->fst->getHandle(scope + "." + RTLIL::unescape_id(name));
+ if (id==0 && name.isPublic())
+ log_warning("Unable to found wire %s in input file.\n", (scope + "." + RTLIL::unescape_id(name)).c_str());
+ if (id!=0) {
+ Const fst_val = Const::from_string(shared->fst->valueAt(id, time));
+ set_state(qsig, fst_val);
+ }
+ }
+ }
+ for (auto child : children)
+ child.second->setInitState(time);
+ }
+
+ bool checkSignals(uint64_t time)
+ {
+ bool retVal = false;
+ for(auto &item : fst_handles) {
+ if (item.second==0) continue; // Ignore signals not found
+ Const fst_val = Const::from_string(shared->fst->valueAt(item.second, time));
+ Const sim_val = get_state(item.first);
+ if (sim_val.size()!=fst_val.size())
+ log_error("Signal '%s' size is different in gold and gate.\n", log_id(item.first));
+ if (shared->sim_mode == SimulationMode::sim) {
+ // No checks performed when using stimulus
+ } else if (shared->sim_mode == SimulationMode::gate && !fst_val.is_fully_def()) { // FST data contains X
+ for(int i=0;i<fst_val.size();i++) {
+ if (fst_val[i]!=State::Sx && fst_val[i]!=sim_val[i]) {
+ log_warning("Signal '%s' in file %s in simulation %s\n", log_id(item.first), log_signal(fst_val), log_signal(sim_val));
+ retVal = true;
+ break;
+ }
+ }
+ } else if (shared->sim_mode == SimulationMode::gold && !sim_val.is_fully_def()) { // sim data contains X
+ for(int i=0;i<sim_val.size();i++) {
+ if (sim_val[i]!=State::Sx && fst_val[i]!=sim_val[i]) {
+ log_warning("Signal '%s' in file %s in simulation %s\n", log_id(item.first), log_signal(fst_val), log_signal(sim_val));
+ retVal = true;
+ break;
+ }
+ }
+ } else {
+ if (fst_val!=sim_val) {
+ log_warning("Signal '%s' in file %s in simulation '%s'\n", log_id(item.first), log_signal(fst_val), log_signal(sim_val));
+ retVal = true;
+ }
+ }
+ }
+ for (auto child : children)
+ retVal |= child.second->checkSignals(time);
+ return retVal;
+ }
};
struct SimWorker : SimShared
{
SimInstance *top = nullptr;
std::ofstream vcdfile;
+ struct fstContext *fstfile = nullptr;
pool<IdString> clock, clockn, reset, resetn;
+ std::string timescale;
+ std::string sim_filename;
+ std::string scope;
~SimWorker()
{
@@ -641,8 +801,16 @@ struct SimWorker : SimShared
void write_vcd_header()
{
- if (!vcdfile.is_open())
- return;
+ vcdfile << stringf("$version %s $end\n", yosys_version_str);
+
+ std::time_t t = std::time(nullptr);
+ char mbstr[255];
+ if (std::strftime(mbstr, sizeof(mbstr), "%c", std::localtime(&t))) {
+ vcdfile << stringf("$date ") << mbstr << stringf(" $end\n");
+ }
+
+ if (!timescale.empty())
+ vcdfile << stringf("$timescale %s $end\n", timescale.c_str());
int id = 1;
top->write_vcd_header(vcdfile, id);
@@ -652,13 +820,53 @@ struct SimWorker : SimShared
void write_vcd_step(int t)
{
- if (!vcdfile.is_open())
- return;
-
vcdfile << stringf("#%d\n", t);
top->write_vcd_step(vcdfile);
}
+ void write_fst_header()
+ {
+ std::time_t t = std::time(nullptr);
+ fstWriterSetDate(fstfile, asctime(std::localtime(&t)));
+ fstWriterSetVersion(fstfile, yosys_version_str);
+ if (!timescale.empty())
+ fstWriterSetTimescaleFromString(fstfile, timescale.c_str());
+
+ fstWriterSetPackType(fstfile, FST_WR_PT_FASTLZ);
+ fstWriterSetRepackOnClose(fstfile, 1);
+
+ top->write_fst_header(fstfile);
+ }
+
+ void write_fst_step(int t)
+ {
+ fstWriterEmitTimeChange(fstfile, t);
+
+ top->write_fst_step(fstfile);
+ }
+
+ void write_output_header()
+ {
+ if (vcdfile.is_open())
+ write_vcd_header();
+ if (fstfile)
+ write_fst_header();
+ }
+
+ void write_output_step(int t)
+ {
+ if (vcdfile.is_open())
+ write_vcd_step(t);
+ if (fstfile)
+ write_fst_step(t);
+ }
+
+ void write_output_end()
+ {
+ if (fstfile)
+ fstWriterClose(fstfile);
+ }
+
void update()
{
while (1)
@@ -697,7 +905,7 @@ struct SimWorker : SimShared
void run(Module *topmod, int numcycles)
{
log_assert(top == nullptr);
- top = new SimInstance(this, topmod);
+ top = new SimInstance(this, scope, topmod);
if (debug)
log("\n===== 0 =====\n");
@@ -712,24 +920,25 @@ struct SimWorker : SimShared
update();
- write_vcd_header();
- write_vcd_step(0);
+ write_output_header();
+ write_output_step(0);
for (int cycle = 0; cycle < numcycles; cycle++)
{
if (debug)
log("\n===== %d =====\n", 10*cycle + 5);
-
+ else
+ log("Simulating cycle %d.\n", (cycle*2)+1);
set_inports(clock, State::S0);
set_inports(clockn, State::S1);
update();
- write_vcd_step(10*cycle + 5);
+ write_output_step(10*cycle + 5);
if (debug)
log("\n===== %d =====\n", 10*cycle + 10);
else
- log("Simulating cycle %d.\n", cycle+1);
+ log("Simulating cycle %d.\n", (cycle*2)+2);
set_inports(clock, State::S1);
set_inports(clockn, State::S0);
@@ -740,16 +949,137 @@ struct SimWorker : SimShared
}
update();
- write_vcd_step(10*cycle + 10);
+ write_output_step(10*cycle + 10);
}
- write_vcd_step(10*numcycles + 2);
+ write_output_step(10*numcycles + 2);
+
+ write_output_end();
if (writeback) {
pool<Module*> wbmods;
top->writeback(wbmods);
}
}
+
+ void run_cosim(Module *topmod, int numcycles)
+ {
+ log_assert(top == nullptr);
+ fst = new FstData(sim_filename);
+
+ if (scope.empty())
+ log_error("Scope must be defined for co-simulation.\n");
+
+ top = new SimInstance(this, scope, topmod);
+
+ std::vector<fstHandle> fst_clock;
+
+ for (auto portname : clock)
+ {
+ Wire *w = topmod->wire(portname);
+ if (!w)
+ log_error("Can't find port %s on module %s.\n", log_id(portname), log_id(top->module));
+ if (!w->port_input)
+ log_error("Clock port %s on module %s is not input.\n", log_id(portname), log_id(top->module));
+ fstHandle id = fst->getHandle(scope + "." + RTLIL::unescape_id(portname));
+ if (id==0)
+ log_error("Can't find port %s.%s in FST.\n", scope.c_str(), log_id(portname));
+ fst_clock.push_back(id);
+ }
+ for (auto portname : clockn)
+ {
+ Wire *w = topmod->wire(portname);
+ if (!w)
+ log_error("Can't find port %s on module %s.\n", log_id(portname), log_id(top->module));
+ if (!w->port_input)
+ log_error("Clock port %s on module %s is not input.\n", log_id(portname), log_id(top->module));
+ fstHandle id = fst->getHandle(scope + "." + RTLIL::unescape_id(portname));
+ if (id==0)
+ log_error("Can't find port %s.%s in FST.\n", scope.c_str(), log_id(portname));
+ fst_clock.push_back(id);
+ }
+ if (fst_clock.size()==0)
+ log_error("No clock signals defined for input file\n");
+
+ SigMap sigmap(topmod);
+ std::map<Wire*,fstHandle> inputs;
+
+ for (auto wire : topmod->wires()) {
+ if (wire->port_input) {
+ fstHandle id = fst->getHandle(scope + "." + RTLIL::unescape_id(wire->name));
+ if (id==0)
+ log_error("Unable to find required '%s' signal in file\n",(scope + "." + RTLIL::unescape_id(wire->name)).c_str());
+ inputs[wire] = id;
+ }
+ }
+
+ uint64_t startCount = 0;
+ uint64_t stopCount = 0;
+ if (start_time==0) {
+ if (start_time < fst->getStartTime())
+ log_warning("Start time is before simulation file start time\n");
+ startCount = fst->getStartTime();
+ } else if (start_time==-1)
+ startCount = fst->getEndTime();
+ else {
+ startCount = start_time / fst->getTimescale();
+ if (startCount > fst->getEndTime()) {
+ startCount = fst->getEndTime();
+ log_warning("Start time is after simulation file end time\n");
+ }
+ }
+ if (stop_time==0) {
+ if (stop_time < fst->getStartTime())
+ log_warning("Stop time is before simulation file start time\n");
+ stopCount = fst->getStartTime();
+ } else if (stop_time==-1)
+ stopCount = fst->getEndTime();
+ else {
+ stopCount = stop_time / fst->getTimescale();
+ if (stopCount > fst->getEndTime()) {
+ stopCount = fst->getEndTime();
+ log_warning("Stop time is after simulation file end time\n");
+ }
+ }
+ if (stopCount<startCount) {
+ log_error("Stop time is before start time\n");
+ }
+ auto samples = fst->getAllEdges(fst_clock, startCount, stopCount);
+
+ // Limit to number of cycles if provided
+ if (cycles_set && ((size_t)(numcycles *2) < samples.size()))
+ samples.erase(samples.begin() + (numcycles*2), samples.end());
+
+ // Add setup time (start time)
+ if (samples.empty() || samples.front()!=startCount)
+ samples.insert(samples.begin(), startCount);
+
+ fst->reconstructAllAtTimes(samples);
+ bool initial = true;
+ int cycle = 0;
+ log("Co-simulation from %lu%s to %lu%s\n", (unsigned long)startCount, fst->getTimescaleString(), (unsigned long)stopCount, fst->getTimescaleString());
+ for(auto &time : samples) {
+ log("Co-simulating cycle %d [%lu%s].\n", cycle, (unsigned long)time, fst->getTimescaleString());
+ for(auto &item : inputs) {
+ std::string v = fst->valueAt(item.second, time);
+ top->set_state(item.first, Const::from_string(v));
+ }
+ if (initial) {
+ top->setInitState(time);
+ initial = false;
+ }
+ update();
+
+ bool status = top->checkSignals(time);
+ if (status)
+ log_error("Signal difference\n");
+ cycle++;
+ }
+ if (writeback) {
+ pool<Module*> wbmods;
+ top->writeback(wbmods);
+ }
+ }
};
struct SimPass : public Pass {
@@ -765,6 +1095,9 @@ struct SimPass : public Pass {
log(" -vcd <filename>\n");
log(" write the simulation results to the given VCD file\n");
log("\n");
+ log(" -fst <filename>\n");
+ log(" write the simulation results to the given FST file\n");
+ log("\n");
log(" -clock <portname>\n");
log(" name of top-level clock input\n");
log("\n");
@@ -783,15 +1116,45 @@ struct SimPass : public Pass {
log(" -zinit\n");
log(" zero-initialize all uninitialized regs and memories\n");
log("\n");
+ log(" -timescale <string>\n");
+ log(" include the specified timescale declaration in the vcd\n");
+ log("\n");
log(" -n <integer>\n");
- log(" number of cycles to simulate (default: 20)\n");
+ log(" number of clock cycles to simulate (default: 20)\n");
log("\n");
log(" -a\n");
- log(" include all nets in VCD output, not just those with public names\n");
+ log(" use all nets in VCD/FST operations, not just those with public names\n");
log("\n");
log(" -w\n");
log(" writeback mode: use final simulation state as new init state\n");
log("\n");
+ log(" -r\n");
+ log(" read simulation results file (file formats supported: FST)\n");
+ log("\n");
+ log(" -scope\n");
+ log(" scope of simulation top model\n");
+ log("\n");
+ log(" -at <time>\n");
+ log(" sets start and stop time\n");
+ log("\n");
+ log(" -start <time>\n");
+ log(" start co-simulation in arbitary time (default 0)\n");
+ log("\n");
+ log(" -stop <time>\n");
+ log(" stop co-simulation in arbitary time (default END)\n");
+ log("\n");
+ log(" -sim\n");
+ log(" simulation with stimulus from FST (default)\n");
+ log("\n");
+ log(" -sim-cmp\n");
+ log(" co-simulation expect exact match\n");
+ log("\n");
+ log(" -sim-gold\n");
+ log(" co-simulation, x in simulation can match any value in FST\n");
+ log("\n");
+ log(" -sim-gate\n");
+ log(" co-simulation, x in FST can match any value in simulation\n");
+ log("\n");
log(" -d\n");
log(" enable debug output\n");
log("\n");
@@ -800,17 +1163,27 @@ struct SimPass : public Pass {
{
SimWorker worker;
int numcycles = 20;
+ bool start_set = false, stop_set = false, at_set = false;
log_header(design, "Executing SIM pass (simulate the circuit).\n");
size_t argidx;
for (argidx = 1; argidx < args.size(); argidx++) {
if (args[argidx] == "-vcd" && argidx+1 < args.size()) {
- worker.vcdfile.open(args[++argidx].c_str());
+ std::string vcd_filename = args[++argidx];
+ rewrite_filename(vcd_filename);
+ worker.vcdfile.open(vcd_filename.c_str());
+ continue;
+ }
+ if (args[argidx] == "-fst" && argidx+1 < args.size()) {
+ std::string fst_filename = args[++argidx];
+ rewrite_filename(fst_filename);
+ worker.fstfile = (struct fstContext *)fstWriterCreate(fst_filename.c_str(),1);
continue;
}
if (args[argidx] == "-n" && argidx+1 < args.size()) {
numcycles = atoi(args[++argidx].c_str());
+ worker.cycles_set = true;
continue;
}
if (args[argidx] == "-rstlen" && argidx+1 < args.size()) {
@@ -833,6 +1206,10 @@ struct SimPass : public Pass {
worker.resetn.insert(RTLIL::escape_id(args[++argidx]));
continue;
}
+ if (args[argidx] == "-timescale" && argidx+1 < args.size()) {
+ worker.timescale = args[++argidx];
+ continue;
+ }
if (args[argidx] == "-a") {
worker.hide_internal = false;
continue;
@@ -849,9 +1226,55 @@ struct SimPass : public Pass {
worker.zinit = true;
continue;
}
+ if (args[argidx] == "-r" && argidx+1 < args.size()) {
+ std::string sim_filename = args[++argidx];
+ rewrite_filename(sim_filename);
+ worker.sim_filename = sim_filename;
+ continue;
+ }
+ if (args[argidx] == "-scope" && argidx+1 < args.size()) {
+ worker.scope = args[++argidx];
+ continue;
+ }
+ if (args[argidx] == "-start" && argidx+1 < args.size()) {
+ worker.start_time = stringToTime(args[++argidx]);
+ start_set = true;
+ continue;
+ }
+ if (args[argidx] == "-stop" && argidx+1 < args.size()) {
+ worker.stop_time = stringToTime(args[++argidx]);
+ stop_set = true;
+ continue;
+ }
+ if (args[argidx] == "-at" && argidx+1 < args.size()) {
+ worker.start_time = stringToTime(args[++argidx]);
+ worker.stop_time = worker.start_time;
+ at_set = true;
+ continue;
+ }
+ if (args[argidx] == "-sim") {
+ worker.sim_mode = SimulationMode::sim;
+ continue;
+ }
+ if (args[argidx] == "-sim-cmp") {
+ worker.sim_mode = SimulationMode::cmp;
+ continue;
+ }
+ if (args[argidx] == "-sim-gold") {
+ worker.sim_mode = SimulationMode::gold;
+ continue;
+ }
+ if (args[argidx] == "-sim-gate") {
+ worker.sim_mode = SimulationMode::gate;
+ continue;
+ }
break;
}
extra_args(args, argidx, design);
+ if (at_set && (start_set || stop_set || worker.cycles_set))
+ log_error("'at' option can only be defined separate of 'start','stop' and 'n'\n");
+ if (stop_set && worker.cycles_set)
+ log_error("'stop' and 'n' can only be used exclusively'\n");
Module *top_mod = nullptr;
@@ -867,7 +1290,10 @@ struct SimPass : public Pass {
top_mod = mods.front();
}
- worker.run(top_mod, numcycles);
+ if (worker.sim_filename.empty())
+ worker.run(top_mod, numcycles);
+ else
+ worker.run_cosim(top_mod, numcycles);
}
} SimPass;
diff --git a/passes/sat/supercover.cc b/passes/sat/supercover.cc
index aacc044fb..38dbd3cf9 100644
--- a/passes/sat/supercover.cc
+++ b/passes/sat/supercover.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
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-06 16:02:18 +0000