aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--backends/blif/blif.cc6
-rw-r--r--backends/smt2/smt2.cc10
-rw-r--r--frontends/blif/blifparse.cc12
-rw-r--r--kernel/celltypes.h3
-rw-r--r--kernel/rtlil.cc25
-rw-r--r--kernel/rtlil.h2
-rw-r--r--kernel/satgen.h2
-rw-r--r--manual/CHAPTER_CellLib.tex4
-rw-r--r--passes/sat/miter.cc38
-rw-r--r--passes/techmap/simplemap.cc20
-rw-r--r--techlibs/common/simlib.v13
-rw-r--r--techlibs/common/techmap.v2
12 files changed, 118 insertions, 19 deletions
diff --git a/backends/blif/blif.cc b/backends/blif/blif.cc
index 6a379e67f..0dc17c92a 100644
--- a/backends/blif/blif.cc
+++ b/backends/blif/blif.cc
@@ -315,6 +315,12 @@ struct BlifDumper
continue;
}
+ if (!config->icells_mode && cell->type == "$_FF_") {
+ f << stringf(".latch %s %s%s\n", cstr(cell->getPort("\\D")), cstr(cell->getPort("\\Q")),
+ cstr_init(cell->getPort("\\Q")));
+ continue;
+ }
+
if (!config->icells_mode && cell->type == "$_DFF_N_") {
f << stringf(".latch %s %s fe %s%s\n", cstr(cell->getPort("\\D")), cstr(cell->getPort("\\Q")),
cstr(cell->getPort("\\C")), cstr_init(cell->getPort("\\Q")));
diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index 9a25f3a23..487f5befb 100644
--- a/backends/smt2/smt2.cc
+++ b/backends/smt2/smt2.cc
@@ -379,7 +379,7 @@ struct Smt2Worker
return;
}
- if (cell->type == "$_DFF_P_" || cell->type == "$_DFF_N_")
+ if (cell->type.in("$_FF_", "$_DFF_P_", "$_DFF_N_"))
{
registers.insert(cell);
decls.push_back(stringf("(declare-fun |%s#%d| (|%s_s|) Bool) ; %s\n",
@@ -407,7 +407,7 @@ struct Smt2Worker
if (bvmode)
{
- if (cell->type == "$dff")
+ if (cell->type.in("$ff", "$dff"))
{
registers.insert(cell);
decls.push_back(stringf("(declare-fun |%s#%d| (|%s_s|) (_ BitVec %d)) ; %s\n",
@@ -596,7 +596,7 @@ struct Smt2Worker
pool<SigBit> reg_bits;
for (auto cell : module->cells())
- if (cell->type.in("$_DFF_P_", "$_DFF_N_", "$dff")) {
+ if (cell->type.in("$ff", "$dff", "$_FF_", "$_DFF_P_", "$_DFF_N_")) {
// not using sigmap -- we want the net directly at the dff output
for (auto bit : cell->getPort("\\Q"))
reg_bits.insert(bit);
@@ -674,14 +674,14 @@ struct Smt2Worker
for (auto cell : this_regs)
{
- if (cell->type == "$_DFF_P_" || cell->type == "$_DFF_N_")
+ if (cell->type.in("$_FF_", "$_DFF_P_", "$_DFF_N_"))
{
std::string expr_d = get_bool(cell->getPort("\\D"));
std::string expr_q = get_bool(cell->getPort("\\Q"), "next_state");
trans.push_back(stringf(" (= %s %s) ; %s %s\n", expr_d.c_str(), expr_q.c_str(), get_id(cell), log_signal(cell->getPort("\\Q"))));
}
- if (cell->type == "$dff")
+ if (cell->type.in("$ff", "$dff"))
{
std::string expr_d = get_bv(cell->getPort("\\D"));
std::string expr_q = get_bv(cell->getPort("\\Q"), "next_state");
diff --git a/frontends/blif/blifparse.cc b/frontends/blif/blifparse.cc
index 3717a1e5e..f154f7c04 100644
--- a/frontends/blif/blifparse.cc
+++ b/frontends/blif/blifparse.cc
@@ -256,9 +256,13 @@ void parse_blif(RTLIL::Design *design, std::istream &f, std::string dff_name, bo
cell = module->addDlatch(NEW_ID, blif_wire(clock), blif_wire(d), blif_wire(q), false);
else {
no_latch_clock:
- cell = module->addCell(NEW_ID, dff_name);
- cell->setPort("\\D", blif_wire(d));
- cell->setPort("\\Q", blif_wire(q));
+ if (dff_name.empty()) {
+ cell = module->addFf(NEW_ID, blif_wire(d), blif_wire(q));
+ } else {
+ cell = module->addCell(NEW_ID, dff_name);
+ cell->setPort("\\D", blif_wire(d));
+ cell->setPort("\\Q", blif_wire(q));
+ }
}
obj_attributes = &cell->attributes;
@@ -477,7 +481,7 @@ struct BlifFrontend : public Frontend {
}
extra_args(f, filename, args, argidx);
- parse_blif(design, *f, "\\DFF", true, sop_mode);
+ parse_blif(design, *f, "", true, sop_mode);
}
} BlifFrontend;
diff --git a/kernel/celltypes.h b/kernel/celltypes.h
index 900c12d01..8e3f86f69 100644
--- a/kernel/celltypes.h
+++ b/kernel/celltypes.h
@@ -130,6 +130,7 @@ struct CellTypes
IdString CTRL_IN = "\\CTRL_IN", CTRL_OUT = "\\CTRL_OUT";
setup_type("$sr", {SET, CLR}, {Q});
+ setup_type("$ff", {D}, {Q});
setup_type("$dff", {CLK, D}, {Q});
setup_type("$dffe", {CLK, EN, D}, {Q});
setup_type("$dffsr", {CLK, SET, CLR, D}, {Q});
@@ -184,6 +185,8 @@ struct CellTypes
for (auto c2 : list_np)
setup_type(stringf("$_SR_%c%c_", c1, c2), {S, R}, {Q});
+ setup_type("$_FF_", {D}, {Q});
+
for (auto c1 : list_np)
setup_type(stringf("$_DFF_%c_", c1), {C, D}, {Q});
diff --git a/kernel/rtlil.cc b/kernel/rtlil.cc
index 32efe4f0d..b0cda67b4 100644
--- a/kernel/rtlil.cc
+++ b/kernel/rtlil.cc
@@ -866,6 +866,13 @@ namespace {
return;
}
+ if (cell->type == "$ff") {
+ port("\\D", param("\\WIDTH"));
+ port("\\Q", param("\\WIDTH"));
+ check_expected();
+ return;
+ }
+
if (cell->type == "$dff") {
param_bool("\\CLK_POLARITY");
port("\\CLK", 1);
@@ -1069,6 +1076,7 @@ namespace {
if (cell->type == "$_SR_PN_") { check_gate("SRQ"); return; }
if (cell->type == "$_SR_PP_") { check_gate("SRQ"); return; }
+ if (cell->type == "$_FF_") { check_gate("DQ"); return; }
if (cell->type == "$_DFF_N_") { check_gate("DQC"); return; }
if (cell->type == "$_DFF_P_") { check_gate("DQC"); return; }
@@ -1830,6 +1838,15 @@ RTLIL::Cell* RTLIL::Module::addSr(RTLIL::IdString name, RTLIL::SigSpec sig_set,
return cell;
}
+RTLIL::Cell* RTLIL::Module::addFf(RTLIL::IdString name, RTLIL::SigSpec sig_d, RTLIL::SigSpec sig_q)
+{
+ RTLIL::Cell *cell = addCell(name, "$ff");
+ cell->parameters["\\WIDTH"] = sig_q.size();
+ cell->setPort("\\D", sig_d);
+ cell->setPort("\\Q", sig_q);
+ return cell;
+}
+
RTLIL::Cell* RTLIL::Module::addDff(RTLIL::IdString name, RTLIL::SigSpec sig_clk, RTLIL::SigSpec sig_d, RTLIL::SigSpec sig_q, bool clk_polarity)
{
RTLIL::Cell *cell = addCell(name, "$dff");
@@ -1912,6 +1929,14 @@ RTLIL::Cell* RTLIL::Module::addDlatchsr(RTLIL::IdString name, RTLIL::SigSpec sig
return cell;
}
+RTLIL::Cell* RTLIL::Module::addFfGate(RTLIL::IdString name, RTLIL::SigSpec sig_d, RTLIL::SigSpec sig_q)
+{
+ RTLIL::Cell *cell = addCell(name, "$_FF_");
+ cell->setPort("\\D", sig_d);
+ cell->setPort("\\Q", sig_q);
+ return cell;
+}
+
RTLIL::Cell* RTLIL::Module::addDffGate(RTLIL::IdString name, RTLIL::SigSpec sig_clk, RTLIL::SigSpec sig_d, RTLIL::SigSpec sig_q, bool clk_polarity)
{
RTLIL::Cell *cell = addCell(name, stringf("$_DFF_%c_", clk_polarity ? 'P' : 'N'));
diff --git a/kernel/rtlil.h b/kernel/rtlil.h
index a426e0bdd..058f6acf4 100644
--- a/kernel/rtlil.h
+++ b/kernel/rtlil.h
@@ -1008,6 +1008,7 @@ public:
RTLIL::Cell* addEquiv (RTLIL::IdString name, RTLIL::SigSpec sig_a, RTLIL::SigSpec sig_b, RTLIL::SigSpec sig_y);
RTLIL::Cell* addSr (RTLIL::IdString name, RTLIL::SigSpec sig_set, RTLIL::SigSpec sig_clr, RTLIL::SigSpec sig_q, bool set_polarity = true, bool clr_polarity = true);
+ RTLIL::Cell* addFf (RTLIL::IdString name, RTLIL::SigSpec sig_d, RTLIL::SigSpec sig_q);
RTLIL::Cell* addDff (RTLIL::IdString name, RTLIL::SigSpec sig_clk, RTLIL::SigSpec sig_d, RTLIL::SigSpec sig_q, bool clk_polarity = true);
RTLIL::Cell* addDffe (RTLIL::IdString name, RTLIL::SigSpec sig_clk, RTLIL::SigSpec sig_en, RTLIL::SigSpec sig_d, RTLIL::SigSpec sig_q, bool clk_polarity = true, bool en_polarity = true);
RTLIL::Cell* addDffsr (RTLIL::IdString name, RTLIL::SigSpec sig_clk, RTLIL::SigSpec sig_set, RTLIL::SigSpec sig_clr,
@@ -1032,6 +1033,7 @@ public:
RTLIL::Cell* addAoi4Gate (RTLIL::IdString name, RTLIL::SigBit sig_a, RTLIL::SigBit sig_b, RTLIL::SigBit sig_c, RTLIL::SigBit sig_d, RTLIL::SigBit sig_y);
RTLIL::Cell* addOai4Gate (RTLIL::IdString name, RTLIL::SigBit sig_a, RTLIL::SigBit sig_b, RTLIL::SigBit sig_c, RTLIL::SigBit sig_d, RTLIL::SigBit sig_y);
+ RTLIL::Cell* addFfGate (RTLIL::IdString name, RTLIL::SigSpec sig_d, RTLIL::SigSpec sig_q);
RTLIL::Cell* addDffGate (RTLIL::IdString name, RTLIL::SigSpec sig_clk, RTLIL::SigSpec sig_d, RTLIL::SigSpec sig_q, bool clk_polarity = true);
RTLIL::Cell* addDffeGate (RTLIL::IdString name, RTLIL::SigSpec sig_clk, RTLIL::SigSpec sig_en, RTLIL::SigSpec sig_d, RTLIL::SigSpec sig_q, bool clk_polarity = true, bool en_polarity = true);
RTLIL::Cell* addDffsrGate (RTLIL::IdString name, RTLIL::SigSpec sig_clk, RTLIL::SigSpec sig_set, RTLIL::SigSpec sig_clr,
diff --git a/kernel/satgen.h b/kernel/satgen.h
index 0a65b490c..792bb3ed7 100644
--- a/kernel/satgen.h
+++ b/kernel/satgen.h
@@ -1293,7 +1293,7 @@ struct SatGen
return true;
}
- if (timestep > 0 && (cell->type == "$dff" || cell->type == "$_DFF_N_" || cell->type == "$_DFF_P_"))
+ if (timestep > 0 && cell->type.in("$ff", "$dff", "$_FF_", "$_DFF_N_", "$_DFF_P_"))
{
if (timestep == 1)
{
diff --git a/manual/CHAPTER_CellLib.tex b/manual/CHAPTER_CellLib.tex
index bd73ae23c..7778fe8fd 100644
--- a/manual/CHAPTER_CellLib.tex
+++ b/manual/CHAPTER_CellLib.tex
@@ -437,6 +437,10 @@ Add information about {\tt \$alu}, {\tt \$macc}, {\tt \$fa}, and {\tt \$lcu} cel
\end{fixme}
\begin{fixme}
+Add information about {\tt \$ff} and {\tt \$\_FF\_} cells.
+\end{fixme}
+
+\begin{fixme}
Add information about {\tt \$dffe}, {\tt \$dffsr}, {\tt \$dlatch}, and {\tt \$dlatchsr} cells.
\end{fixme}
diff --git a/passes/sat/miter.cc b/passes/sat/miter.cc
index 4854e19bf..341a6bac8 100644
--- a/passes/sat/miter.cc
+++ b/passes/sat/miter.cc
@@ -312,18 +312,42 @@ void create_miter_assert(struct Pass *that, std::vector<std::string> args, RTLIL
log_pop();
}
- SigSpec or_signals;
+ SigSpec assert_signals, assume_signals;
vector<Cell*> cell_list = module->cells();
- for (auto cell : cell_list) {
+ for (auto cell : cell_list)
+ {
+ if (!cell->type.in("$assert", "$assume"))
+ continue;
+
+ SigBit is_active = module->Nex(NEW_ID, cell->getPort("\\A"), State::S1);
+ SigBit is_enabled = module->Eqx(NEW_ID, cell->getPort("\\EN"), State::S1);
+
if (cell->type == "$assert") {
- SigBit is_active = module->Nex(NEW_ID, cell->getPort("\\A"), State::S1);
- SigBit is_enabled = module->Eqx(NEW_ID, cell->getPort("\\EN"), State::S1);
- or_signals.append(module->And(NEW_ID, is_active, is_enabled));
- module->remove(cell);
+ assert_signals.append(module->And(NEW_ID, is_active, is_enabled));
+ } else {
+ assume_signals.append(module->And(NEW_ID, is_active, is_enabled));
}
+
+ module->remove(cell);
}
- module->addReduceOr(NEW_ID, or_signals, trigger);
+ if (assume_signals.empty())
+ {
+ module->addReduceOr(NEW_ID, assert_signals, trigger);
+ }
+ else
+ {
+ Wire *assume_q = module->addWire(NEW_ID);
+ assume_q->attributes["\\init"] = State::S1;
+ assume_signals.append(assume_q);
+
+ SigSpec assume_nok = module->ReduceOr(NEW_ID, assume_signals);
+ SigSpec assume_ok = module->Not(NEW_ID, assume_nok);
+ module->addFf(NEW_ID, assume_ok, assume_q);
+
+ SigSpec assert_fail = module->ReduceOr(NEW_ID, assert_signals);
+ module->addAnd(NEW_ID, assert_fail, assume_ok, trigger);
+ }
if (flag_flatten) {
log_push();
diff --git a/passes/techmap/simplemap.cc b/passes/techmap/simplemap.cc
index 0fb647344..c6b932bdc 100644
--- a/passes/techmap/simplemap.cc
+++ b/passes/techmap/simplemap.cc
@@ -388,6 +388,23 @@ void simplemap_sr(RTLIL::Module *module, RTLIL::Cell *cell)
}
}
+void simplemap_ff(RTLIL::Module *module, RTLIL::Cell *cell)
+{
+ int width = cell->parameters.at("\\WIDTH").as_int();
+
+ RTLIL::SigSpec sig_d = cell->getPort("\\D");
+ RTLIL::SigSpec sig_q = cell->getPort("\\Q");
+
+ std::string gate_type = "$_FF_";
+
+ for (int i = 0; i < width; i++) {
+ RTLIL::Cell *gate = module->addCell(NEW_ID, gate_type);
+ gate->add_strpool_attribute("\\src", cell->get_strpool_attribute("\\src"));
+ gate->setPort("\\D", sig_d[i]);
+ gate->setPort("\\Q", sig_q[i]);
+ }
+}
+
void simplemap_dff(RTLIL::Module *module, RTLIL::Cell *cell)
{
int width = cell->parameters.at("\\WIDTH").as_int();
@@ -532,6 +549,7 @@ void simplemap_get_mappers(std::map<RTLIL::IdString, void(*)(RTLIL::Module*, RTL
mappers["$slice"] = simplemap_slice;
mappers["$concat"] = simplemap_concat;
mappers["$sr"] = simplemap_sr;
+ mappers["$ff"] = simplemap_ff;
mappers["$dff"] = simplemap_dff;
mappers["$dffe"] = simplemap_dffe;
mappers["$dffsr"] = simplemap_dffsr;
@@ -569,7 +587,7 @@ struct SimplemapPass : public Pass {
log(" $not, $pos, $and, $or, $xor, $xnor\n");
log(" $reduce_and, $reduce_or, $reduce_xor, $reduce_xnor, $reduce_bool\n");
log(" $logic_not, $logic_and, $logic_or, $mux, $tribuf\n");
- log(" $sr, $dff, $dffsr, $adff, $dlatch\n");
+ log(" $sr, $ff, $dff, $dffsr, $adff, $dlatch\n");
log("\n");
}
virtual void execute(std::vector<std::string> args, RTLIL::Design *design)
diff --git a/techlibs/common/simlib.v b/techlibs/common/simlib.v
index 922a47cab..db818269b 100644
--- a/techlibs/common/simlib.v
+++ b/techlibs/common/simlib.v
@@ -1383,6 +1383,19 @@ endmodule
`endif
// --------------------------------------------------------
+module \$ff (D, Q);
+
+parameter WIDTH = 0;
+
+input [WIDTH-1:0] D;
+output [WIDTH-1:0] Q;
+
+assign D = Q;
+
+endmodule
+
+// --------------------------------------------------------
+
module \$dff (CLK, D, Q);
parameter WIDTH = 0;
diff --git a/techlibs/common/techmap.v b/techlibs/common/techmap.v
index 90c4ed7eb..d7ec3947e 100644
--- a/techlibs/common/techmap.v
+++ b/techlibs/common/techmap.v
@@ -64,7 +64,7 @@ module _90_simplemap_various;
endmodule
(* techmap_simplemap *)
-(* techmap_celltype = "$sr $dff $dffe $adff $dffsr $dlatch" *)
+(* techmap_celltype = "$sr $ff $dff $dffe $adff $dffsr $dlatch" *)
module _90_simplemap_registers;
endmodule
generated by cgit v1.2.3 (git 2.25.1) at 2025-01-15 12:16:51 +0000