riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity

sat: Add -set-def-formal option to force defined $any* outputs

This commit is contained in:
Jannis Harder 2022-11-28 14:48:58 +01:00
parent 23e26ff661
commit ed0e14820e
3 changed files with 46 additions and 10 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

23
kernel/satgen.cc
View File

@ -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);
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;
}

1
kernel/satgen.h
View File

@ -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)

28
passes/sat/sat.cc
View File

@ -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;