summaryrefslogtreecommitdiff
path: root/passes/cmds/chformal.cc
diff options
context:
space:
mode:
Diffstat (limited to 'passes/cmds/chformal.cc')
-rw-r--r--passes/cmds/chformal.cc282
1 files changed, 282 insertions, 0 deletions
diff --git a/passes/cmds/chformal.cc b/passes/cmds/chformal.cc
new file mode 100644
index 00000000..522758ea
--- /dev/null
+++ b/passes/cmds/chformal.cc
@@ -0,0 +1,282 @@
+/*
+ * yosys -- Yosys Open SYnthesis Suite
+ *
+ * Copyright (C) 2012 Clifford Wolf <clifford@clifford.at>
+ *
+ * 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.
+ *
+ */
+
+#include "kernel/yosys.h"
+#include "kernel/sigtools.h"
+
+USING_YOSYS_NAMESPACE
+PRIVATE_NAMESPACE_BEGIN
+
+struct ChformalPass : public Pass {
+ ChformalPass() : Pass("chformal", "change formal constraints of the design") { }
+ void help() YS_OVERRIDE
+ {
+ // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
+ log("\n");
+ log(" chformal [types] [mode] [options] [selection]\n");
+ log("\n");
+ log("Make changes to the formal constraints of the design. The [types] options\n");
+ log("the type of constraint to operate on. If none of the folling options is given,\n");
+ log("the command will operate on all constraint types:\n");
+ log("\n");
+ log(" -assert $assert cells, representing assert(...) constraints\n");
+ log(" -assume $assume cells, representing assume(...) constraints\n");
+ log(" -live $live cells, representing assert(s_eventually ...)\n");
+ log(" -fair $fair cells, representing assume(s_eventually ...)\n");
+ log(" -cover $cover cells, representing cover() statements\n");
+ log("\n");
+ log("Exactly one of the following modes must be specified:\n");
+ log("\n");
+ log(" -remove\n");
+ log(" remove the cells and thus constraints from the design\n");
+ log("\n");
+ log(" -early\n");
+ log(" bypass FFs that only delay the activation of a constraint\n");
+ log("\n");
+ log(" -delay <N>\n");
+ log(" delay activation of the constraint by <N> clock cycles\n");
+ log("\n");
+ log(" -skip <N>\n");
+ log(" ignore activation of the constraint in the first <N> clock cycles\n");
+ log("\n");
+ log(" -assert2assume\n");
+ log(" -assume2assert\n");
+ log(" -live2fair\n");
+ log(" -fair2live\n");
+ log(" change the roles of cells as indicated. this options can be combined\n");
+ log("\n");
+ }
+ void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
+ {
+ bool assert2assume = false;
+ bool assume2assert = false;
+ bool live2fair = false;
+ bool fair2live = false;
+
+ pool<IdString> constr_types;
+ char mode = 0;
+ int mode_arg = 0;
+
+ size_t argidx;
+ for (argidx = 1; argidx < args.size(); argidx++)
+ {
+ if (args[argidx] == "-assert") {
+ constr_types.insert("$assert");
+ continue;
+ }
+ if (args[argidx] == "-assume") {
+ constr_types.insert("$assume");
+ continue;
+ }
+ if (args[argidx] == "-live") {
+ constr_types.insert("$live");
+ continue;
+ }
+ if (args[argidx] == "-fair") {
+ constr_types.insert("$fair");
+ continue;
+ }
+ if (args[argidx] == "-cover") {
+ constr_types.insert("$cover");
+ continue;
+ }
+ if (mode == 0 && args[argidx] == "-remove") {
+ mode = 'r';
+ continue;
+ }
+ if (mode == 0 && args[argidx] == "-early") {
+ mode = 'e';
+ continue;
+ }
+ if (mode == 0 && args[argidx] == "-delay" && argidx+1 < args.size()) {
+ mode = 'd';
+ mode_arg = atoi(args[++argidx].c_str());
+ continue;
+ }
+ if (mode == 0 && args[argidx] == "-skip" && argidx+1 < args.size()) {
+ mode = 's';
+ mode_arg = atoi(args[++argidx].c_str());
+ continue;
+ }
+ if ((mode == 0 || mode == 'c') && args[argidx] == "-assert2assume") {
+ assert2assume = true;
+ mode = 'c';
+ continue;
+ }
+ if ((mode == 0 || mode == 'c') && args[argidx] == "-assume2assert") {
+ assume2assert = true;
+ mode = 'c';
+ continue;
+ }
+ if ((mode == 0 || mode == 'c') && args[argidx] == "-live2fair") {
+ live2fair = true;
+ mode = 'c';
+ continue;
+ }
+ if ((mode == 0 || mode == 'c') && args[argidx] == "-fair2live") {
+ fair2live = true;
+ mode = 'c';
+ continue;
+ }
+ break;
+ }
+ extra_args(args, argidx, design);
+
+ if (constr_types.empty()) {
+ constr_types.insert("$assert");
+ constr_types.insert("$assume");
+ constr_types.insert("$live");
+ constr_types.insert("$fair");
+ constr_types.insert("$cover");
+ }
+
+ if (mode == 0)
+ log_cmd_error("Mode option is missing.\n");
+
+ for (auto module : design->selected_modules())
+ {
+ vector<Cell*> constr_cells;
+
+ for (auto cell : module->selected_cells())
+ if (constr_types.count(cell->type))
+ constr_cells.push_back(cell);
+
+ if (mode == 'r')
+ {
+ for (auto cell : constr_cells)
+ module->remove(cell);
+ }
+ else
+ if (mode == 'e')
+ {
+ SigMap sigmap(module);
+ dict<SigBit, pair<SigBit, pair<SigBit, bool>>> ffmap;
+ pool<SigBit> init_zero, init_one;
+
+ for (auto wire : module->wires())
+ {
+ if (wire->attributes.count("\\init") == 0)
+ continue;
+
+ SigSpec initsig = sigmap(wire);
+ Const initval = wire->attributes.at("\\init");
+
+ for (int i = 0; i < GetSize(initsig) && i < GetSize(initval); i++) {
+ if (initval[i] == State::S0)
+ init_zero.insert(initsig[i]);
+ if (initval[i] == State::S1)
+ init_one.insert(initsig[i]);
+ }
+ }
+
+ for (auto cell : module->selected_cells())
+ {
+ if (cell->type == "$ff") {
+ SigSpec D = sigmap(cell->getPort("\\D"));
+ SigSpec Q = sigmap(cell->getPort("\\Q"));
+ for (int i = 0; i < GetSize(D); i++)
+ ffmap[Q[i]] = make_pair(D[i], make_pair(State::Sm, false));
+ }
+ if (cell->type == "$dff") {
+ SigSpec D = sigmap(cell->getPort("\\D"));
+ SigSpec Q = sigmap(cell->getPort("\\Q"));
+ SigSpec C = sigmap(cell->getPort("\\CLK"));
+ bool clockpol = cell->getParam("\\CLK_POLARITY").as_bool();
+ for (int i = 0; i < GetSize(D); i++)
+ ffmap[Q[i]] = make_pair(D[i], make_pair(C, clockpol));
+ }
+ }
+
+ for (auto cell : constr_cells)
+ while (true)
+ {
+ SigSpec A = sigmap(cell->getPort("\\A"));
+ SigSpec EN = sigmap(cell->getPort("\\EN"));
+
+ if (ffmap.count(A) == 0 || ffmap.count(EN) == 0)
+ break;
+
+ if (!init_zero.count(EN)) {
+ if (cell->type == "$cover") break;
+ if (cell->type.in("$assert", "$assume") && !init_one.count(A)) break;
+ }
+
+ const auto &A_map = ffmap.at(A);
+ const auto &EN_map = ffmap.at(EN);
+
+ if (A_map.second != EN_map.second)
+ break;
+
+ cell->setPort("\\A", A_map.first);
+ cell->setPort("\\EN", EN_map.first);
+ }
+ }
+ else
+ if (mode == 'd')
+ {
+ for (auto cell : constr_cells)
+ for (int i = 0; i < mode_arg; i++)
+ {
+ SigSpec orig_a = cell->getPort("\\A");
+ SigSpec orig_en = cell->getPort("\\EN");
+
+ Wire *new_a = module->addWire(NEW_ID);
+ Wire *new_en = module->addWire(NEW_ID);
+ new_en->attributes["\\init"] = State::S0;
+
+ module->addFf(NEW_ID, orig_a, new_a);
+ module->addFf(NEW_ID, orig_en, new_en);
+
+ cell->setPort("\\A", new_a);
+ cell->setPort("\\EN", new_en);
+ }
+ }
+ else
+ if (mode == 's')
+ {
+ SigSpec en = State::S1;
+
+ for (int i = 0; i < mode_arg; i++) {
+ Wire *w = module->addWire(NEW_ID);
+ w->attributes["\\init"] = State::S0;
+ module->addFf(NEW_ID, en, w);
+ en = w;
+ }
+
+ for (auto cell : constr_cells)
+ cell->setPort("\\EN", module->LogicAnd(NEW_ID, en, cell->getPort("\\EN")));
+ }
+ else
+ if (mode == 'c')
+ {
+ for (auto cell : constr_cells)
+ if (assert2assume && cell->type == "$assert")
+ cell->type = "$assume";
+ else if (assume2assert && cell->type == "$assume")
+ cell->type = "$assert";
+ else if (live2fair && cell->type == "$live")
+ cell->type = "$fair";
+ else if (fair2live && cell->type == "$fair")
+ cell->type = "$live";
+ }
+ }
+ }
+} ChformalPass;
+
+PRIVATE_NAMESPACE_END
generated by cgit v1.2.3 (git 2.25.1) at 2024-04-25 21:19:28 +0000