From ed0e14820ed7790d88504800dc5b59a4194a6992 Mon Sep 17 00:00:00 2001
From: Jannis Harder <me@jix.one>
Date: Mon, 28 Nov 2022 14:48:58 +0100
Subject: sat: Add -set-def-formal option to force defined $any* outputs
---
kernel/satgen.cc | 27 +++++++++++++++++++++++----
kernel/satgen.h | 1 +
passes/sat/sat.cc | 28 ++++++++++++++++++++++------
3 files changed, 46 insertions(+), 10 deletions(-)
diff --git a/kernel/satgen.cc b/kernel/satgen.cc
index 05eeca76e..2a1fd1711 100644
--- a/kernel/satgen.cc
+++ b/kernel/satgen.cc
@@ -1187,6 +1187,10 @@ bool SatGen::importCell(RTLIL::Cell *cell, int timestep)
if (timestep == 1)
{
initial_state.add((*sigmap)(cell->getPort(ID::Q)));
+ if (model_undef && def_formal) {
+ std::vector<int> undef_q = importUndefSigSpec(cell->getPort(ID::Q), timestep);
+ ez->assume(ez->NOT(ez->vec_reduce_or(undef_q)));
+ }
}
else
{
@@ -1254,13 +1258,18 @@ bool SatGen::importCell(RTLIL::Cell *cell, int timestep)
if (cell->type == ID($anyconst))
{
- if (timestep < 2)
+ if (timestep < 2) {
+ if (model_undef && def_formal) {
+ std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
+ ez->assume(ez->NOT(ez->vec_reduce_or(undef_y)));
+ }
return true;
+ }
std::vector<int> d = importDefSigSpec(cell->getPort(ID::Y), timestep-1);
std::vector<int> q = importDefSigSpec(cell->getPort(ID::Y), timestep);
- std::vector<int> qq = model_undef ? ez->vec_var(q.size()) : q;
+ std::vector<int> qq = (model_undef && !def_formal) ? ez->vec_var(q.size()) : q;
ez->assume(ez->vec_eq(d, qq));
if (model_undef)
@@ -1268,14 +1277,24 @@ bool SatGen::importCell(RTLIL::Cell *cell, int timestep)
std::vector<int> undef_d = importUndefSigSpec(cell->getPort(ID::Y), timestep-1);
std::vector<int> undef_q = importUndefSigSpec(cell->getPort(ID::Y), timestep);
- ez->assume(ez->vec_eq(undef_d, undef_q));
- undefGating(q, qq, undef_q);
+ if (def_formal) {
+ for (auto &undef_q_bit : undef_q)
+ ez->SET(ez->CONST_FALSE, undef_q_bit);
+ } else {
+ ez->assume(ez->vec_eq(undef_d, undef_q));
+ undefGating(q, qq, undef_q);
+ }
}
return true;
}
if (cell->type == ID($anyseq))
{
+ if (model_undef && def_formal) {
+ std::vector<int> undef_q = importUndefSigSpec(cell->getPort(ID::Y), timestep);
+ for (auto &undef_q_bit : undef_q)
+ ez->SET(ez->CONST_FALSE, undef_q_bit);
+ }
return true;
}
diff --git a/kernel/satgen.h b/kernel/satgen.h
index da2cec222..8a89ff9db 100644
--- a/kernel/satgen.h
+++ b/kernel/satgen.h
@@ -73,6 +73,7 @@ struct SatGen
std::map<std::pair<std::string, int>, bool> initstates;
bool ignore_div_by_zero;
bool model_undef;
+ bool def_formal = false;
SatGen(ezSAT *ez, SigMap *sigmap, std::string prefix = std::string()) :
ez(ez), sigmap(sigmap), prefix(prefix), ignore_div_by_zero(false), model_undef(false)
diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc
index e10517d72..69f81e3df 100644
--- a/passes/sat/sat.cc
+++ b/passes/sat/sat.cc
@@ -65,11 +65,12 @@ struct SatHelper
int max_timestep, timeout;
bool gotTimeout;
- SatHelper(RTLIL::Design *design, RTLIL::Module *module, bool enable_undef) :
+ SatHelper(RTLIL::Design *design, RTLIL::Module *module, bool enable_undef, bool set_def_formal) :
design(design), module(module), sigmap(module), ct(design), satgen(ez.get(), &sigmap)
{
this->enable_undef = enable_undef;
satgen.model_undef = enable_undef;
+ satgen.def_formal = set_def_formal;
set_init_def = false;
set_init_undef = false;
set_init_zero = false;
@@ -254,7 +255,13 @@ struct SatHelper
if (initstate)
{
- RTLIL::SigSpec big_lhs, big_rhs;
+ RTLIL::SigSpec big_lhs, big_rhs, forced_def;
+
+ // Check for $anyinit cells that are forced to be defined
+ if (set_init_undef && satgen.def_formal)
+ for (auto cell : module->cells())
+ if (cell->type == ID($anyinit))
+ forced_def.append(sigmap(cell->getPort(ID::Q)));
for (auto wire : module->wires())
{
@@ -323,6 +330,7 @@ struct SatHelper
if (set_init_undef) {
RTLIL::SigSpec rem = satgen.initial_state.export_all();
rem.remove(big_lhs);
+ rem.remove(forced_def);
big_lhs.append(rem);
big_rhs.append(RTLIL::SigSpec(RTLIL::State::Sx, rem.size()));
}
@@ -933,6 +941,9 @@ struct SatPass : public Pass {
log(" -set-def-inputs\n");
log(" add -set-def constraints for all module inputs\n");
log("\n");
+ log(" -set-def-formal\n");
+ log(" add -set-def constraints for formal $anyinit, $anyconst, $anyseq cells\n");
+ log("\n");
log(" -show <signal>\n");
log(" show the model for the specified signal. if no -show option is\n");
log(" passed then a set of signals to be shown is automatically selected.\n");
@@ -1068,7 +1079,7 @@ struct SatPass : public Pass {
std::map<int, std::vector<std::string>> unsets_at, sets_def_at, sets_any_undef_at, sets_all_undef_at;
std::vector<std::string> shows, sets_def, sets_any_undef, sets_all_undef;
int loopcount = 0, seq_len = 0, maxsteps = 0, initsteps = 0, timeout = 0, prove_skip = 0;
- bool verify = false, fail_on_timeout = false, enable_undef = false, set_def_inputs = false;
+ bool verify = false, fail_on_timeout = false, enable_undef = false, set_def_inputs = false, set_def_formal = false;
bool ignore_div_by_zero = false, set_init_undef = false, set_init_zero = false, max_undef = false;
bool tempinduct = false, prove_asserts = false, show_inputs = false, show_outputs = false;
bool show_regs = false, show_public = false, show_all = false;
@@ -1141,6 +1152,11 @@ struct SatPass : public Pass {
set_def_inputs = true;
continue;
}
+ if (args[argidx] == "-set-def-formal") {
+ enable_undef = true;
+ set_def_formal = true;
+ continue;
+ }
if (args[argidx] == "-set" && argidx+2 < args.size()) {
std::string lhs = args[++argidx];
std::string rhs = args[++argidx];
@@ -1380,8 +1396,8 @@ struct SatPass : public Pass {
if (loopcount > 0 || max_undef)
log_cmd_error("The options -max, -all, and -max_undef are not supported for temporal induction proofs!\n");
- SatHelper basecase(design, module, enable_undef);
- SatHelper inductstep(design, module, enable_undef);
+ SatHelper basecase(design, module, enable_undef, set_def_formal);
+ SatHelper inductstep(design, module, enable_undef, set_def_formal);
basecase.sets = sets;
basecase.set_assumes = set_assumes;
@@ -1570,7 +1586,7 @@ struct SatPass : public Pass {
if (maxsteps > 0)
log_cmd_error("The options -maxsteps is only supported for temporal induction proofs!\n");
- SatHelper sathelper(design, module, enable_undef);
+ SatHelper sathelper(design, module, enable_undef, set_def_formal);
sathelper.sets = sets;
sathelper.set_assumes = set_assumes;
--
cgit v1.2.3