aboutsummaryrefslogtreecommitdiffstats
path: root/passes
diff options
context:
space:
mode:
Diffstat (limited to 'passes')
-rw-r--r--passes/cmds/show.cc1
-rw-r--r--passes/fsm/fsm_detect.cc1
-rw-r--r--passes/hierarchy/submod.cc1
-rw-r--r--passes/opt/opt_clean.cc2
-rw-r--r--passes/sat/Makefile.inc1
-rw-r--r--passes/sat/formalff.cc192
-rw-r--r--passes/sat/sim.cc2
7 files changed, 199 insertions, 1 deletions
diff --git a/passes/cmds/show.cc b/passes/cmds/show.cc
index 43deba47b..4d5605932 100644
--- a/passes/cmds/show.cc
+++ b/passes/cmds/show.cc
@@ -574,6 +574,7 @@ struct ShowWorker
{
ct.setup_internals();
ct.setup_internals_mem();
+ ct.setup_internals_anyinit();
ct.setup_stdcells();
ct.setup_stdcells_mem();
ct.setup_design(design);
diff --git a/passes/fsm/fsm_detect.cc b/passes/fsm/fsm_detect.cc
index a2d38a0bd..f829714c4 100644
--- a/passes/fsm/fsm_detect.cc
+++ b/passes/fsm/fsm_detect.cc
@@ -280,6 +280,7 @@ struct FsmDetectPass : public Pass {
CellTypes ct;
ct.setup_internals();
+ ct.setup_internals_anyinit();
ct.setup_internals_mem();
ct.setup_stdcells();
ct.setup_stdcells_mem();
diff --git a/passes/hierarchy/submod.cc b/passes/hierarchy/submod.cc
index 845dc850f..c0c40671d 100644
--- a/passes/hierarchy/submod.cc
+++ b/passes/hierarchy/submod.cc
@@ -260,6 +260,7 @@ struct SubmodWorker
}
ct.setup_internals();
+ ct.setup_internals_anyinit();
ct.setup_internals_mem();
ct.setup_stdcells();
ct.setup_stdcells_mem();
diff --git a/passes/opt/opt_clean.cc b/passes/opt/opt_clean.cc
index cb2c261c4..dde7c5299 100644
--- a/passes/opt/opt_clean.cc
+++ b/passes/opt/opt_clean.cc
@@ -633,6 +633,7 @@ struct OptCleanPass : public Pass {
keep_cache.reset(design);
ct_reg.setup_internals_mem();
+ ct_reg.setup_internals_anyinit();
ct_reg.setup_stdcells_mem();
ct_all.setup(design);
@@ -694,6 +695,7 @@ struct CleanPass : public Pass {
keep_cache.reset(design);
ct_reg.setup_internals_mem();
+ ct_reg.setup_internals_anyinit();
ct_reg.setup_stdcells_mem();
ct_all.setup(design);
diff --git a/passes/sat/Makefile.inc b/passes/sat/Makefile.inc
index da6d49433..ebe3dc536 100644
--- a/passes/sat/Makefile.inc
+++ b/passes/sat/Makefile.inc
@@ -10,6 +10,7 @@ OBJS += passes/sat/expose.o
OBJS += passes/sat/assertpmux.o
OBJS += passes/sat/clk2fflogic.o
OBJS += passes/sat/async2sync.o
+OBJS += passes/sat/formalff.o
OBJS += passes/sat/supercover.o
OBJS += passes/sat/fmcombine.o
OBJS += passes/sat/mutate.o
diff --git a/passes/sat/formalff.cc b/passes/sat/formalff.cc
new file mode 100644
index 000000000..fe6f98c16
--- /dev/null
+++ b/passes/sat/formalff.cc
@@ -0,0 +1,192 @@
+/*
+ * yosys -- Yosys Open SYnthesis Suite
+ *
+ * Copyright (C) 2022 Jannis Harder <jix@yosyshq.com> <me@jix.one>
+ *
+ * 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"
+#include "kernel/ffinit.h"
+#include "kernel/ff.h"
+
+USING_YOSYS_NAMESPACE
+PRIVATE_NAMESPACE_BEGIN
+
+struct FormalFfPass : public Pass {
+ FormalFfPass() : Pass("formalff", "prepare FFs for formal") { }
+ void help() override
+ {
+ // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
+ log("\n");
+ log(" formalff [options] [selection]\n");
+ log("\n");
+ log("This pass transforms clocked flip-flops to prepare a design for formal\n");
+ log("verification. If a design contains latches and/or multiple different clocks run\n");
+ log("the async2sync or clk2fflogic passes before using this pass.\n");
+ log("\n");
+ log(" -clk2ff\n");
+ log(" Replace all clocked flip-flops with $ff cells that use the implicit\n");
+ log(" global clock. This assumes, without checking, that the design uses a\n");
+ log(" single global clock. If that is not the case, the clk2fflogic pass\n");
+ log(" should be used instead.\n");
+ log("\n");
+ log(" -ff2anyinit\n");
+ log(" Replace uninitialized bits of $ff cells with $anyinit cells. An\n");
+ log(" $anyinit cell behaves exactly like an $ff cell with an undefined\n");
+ log(" initialization value. The difference is that $anyinit inhibits\n");
+ log(" don't-care optimizations and is used to track solver-provided values\n");
+ log(" in witness traces.\n");
+ log("\n");
+ log(" If combined with -clk2ff this also affects newly created $ff cells.\n");
+ log("\n");
+ log(" -anyinit2ff\n");
+ log(" Replaces $anyinit cells with uninitialized $ff cells. This performs the\n");
+ log(" reverse of -ff2anyinit and can be used, before running a backend pass\n");
+ log(" (or similar) that is not yet aware of $anyinit cells.\n");
+ log("\n");
+ log(" Note that after running -anyinit2ff, in general, performing don't-care\n");
+ log(" optimizations is not sound in a formal verification setting.\n");
+ log("\n");
+ log(" -fine\n");
+ log(" Emit fine-grained $_FF_ cells instead of coarse-grained $ff cells for\n");
+ log(" -anyinit2ff. Cannot be combined with -clk2ff or -ff2anyinit.\n");
+ log("\n");
+
+ // TODO: An option to check whether all FFs use the same clock before changing it to the global clock
+ }
+ void execute(std::vector<std::string> args, RTLIL::Design *design) override
+ {
+ bool flag_clk2ff = false;
+ bool flag_ff2anyinit = false;
+ bool flag_anyinit2ff = false;
+ bool flag_fine = false;
+
+ log_header(design, "Executing FORMALFF pass.\n");
+
+ size_t argidx;
+ for (argidx = 1; argidx < args.size(); argidx++)
+ {
+ if (args[argidx] == "-clk2ff") {
+ flag_clk2ff = true;
+ continue;
+ }
+ if (args[argidx] == "-ff2anyinit") {
+ flag_ff2anyinit = true;
+ continue;
+ }
+ if (args[argidx] == "-anyinit2ff") {
+ flag_anyinit2ff = true;
+ continue;
+ }
+ if (args[argidx] == "-fine") {
+ flag_fine = true;
+ continue;
+ }
+ break;
+ }
+ extra_args(args, argidx, design);
+
+ if (!(flag_clk2ff || flag_ff2anyinit || flag_anyinit2ff))
+ log_cmd_error("One of the options -clk2ff, -ff2anyinit, or -anyinit2ff must be specified.\n");
+
+ if (flag_ff2anyinit && flag_anyinit2ff)
+ log_cmd_error("The options -ff2anyinit and -anyinit2ff are exclusive.\n");
+
+ if (flag_fine && !flag_anyinit2ff)
+ log_cmd_error("The option -fine requries the -anyinit2ff option.\n");
+
+ if (flag_fine && flag_clk2ff)
+ log_cmd_error("The options -fine and -clk2ff are exclusive.\n");
+
+ for (auto module : design->selected_modules())
+ {
+ SigMap sigmap(module);
+ FfInitVals initvals(&sigmap, module);
+
+
+ for (auto cell : module->selected_cells())
+ {
+ if (flag_anyinit2ff && cell->type == ID($anyinit))
+ {
+ FfData ff(&initvals, cell);
+ ff.remove();
+ ff.is_anyinit = false;
+ ff.is_fine = flag_fine;
+ if (flag_fine)
+ for (int i = 0; i < ff.width; i++)
+ ff.slice({i}).emit();
+ else
+ ff.emit();
+
+ continue;
+ }
+
+ if (!RTLIL::builtin_ff_cell_types().count(cell->type))
+ continue;
+
+ FfData ff(&initvals, cell);
+ bool emit = false;
+
+ if (flag_clk2ff && ff.has_clk) {
+ if (ff.sig_clk.is_fully_const())
+ log_error("Const CLK on %s (%s) from module %s, run async2sync first.\n",
+ log_id(cell), log_id(cell->type), log_id(module));
+
+ ff.unmap_ce_srst();
+ ff.has_clk = false;
+ ff.has_gclk = true;
+ emit = true;
+ }
+
+ if (!ff.has_gclk) {
+ continue;
+ }
+
+ if (flag_ff2anyinit && !ff.val_init.is_fully_def())
+ {
+ ff.remove();
+ emit = false;
+
+ int cursor = 0;
+ while (cursor < ff.val_init.size())
+ {
+ bool is_anyinit = ff.val_init[cursor] == State::Sx;
+ std::vector<int> bits;
+ bits.push_back(cursor++);
+ while (cursor < ff.val_init.size() && (ff.val_init[cursor] == State::Sx) == is_anyinit)
+ bits.push_back(cursor++);
+
+ if ((int)bits.size() == ff.val_init.size()) {
+ // This check is only to make the private names more helpful for debugging
+ ff.is_anyinit = true;
+ emit = true;
+ break;
+ }
+
+ auto slice = ff.slice(bits);
+ slice.is_anyinit = is_anyinit;
+ slice.emit();
+ }
+ }
+
+ if (emit)
+ ff.emit();
+ }
+ }
+ }
+} FormalFfPass;
+
+PRIVATE_NAMESPACE_END
diff --git a/passes/sat/sim.cc b/passes/sat/sim.cc
index 53644c6b7..ea64dce06 100644
--- a/passes/sat/sim.cc
+++ b/passes/sat/sim.cc
@@ -231,7 +231,7 @@ struct SimInstance
}
}
- if (RTLIL::builtin_ff_cell_types().count(cell->type)) {
+ if (RTLIL::builtin_ff_cell_types().count(cell->type) || cell->type == ID($anyinit)) {
FfData ff_data(nullptr, cell);
ff_state_t ff;
ff.past_d = Const(State::Sx, ff_data.width);
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-01 21:11:24 +0000