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

xprop: Add -split-public option

This commit is contained in:
Jannis Harder 2022-12-08 20:00:01 +01:00
parent aeba966475
commit 172a8e79f0
1 changed files with 39 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

39
passes/cmds/xprop.cc
View File

@ -33,6 +33,7 @@ struct XpropOptions
{
bool split_inputs = false;
bool split_outputs = false;
bool split_public = false;
bool assume_encoding = false;
bool assert_encoding = false;
bool assume_def_inputs = false;
@ -1018,6 +1019,31 @@ struct XpropWorker
module->fixup_ports();
}
void split_public()
{
if (!options.split_public)
return;
for (auto wire : module->selected_wires()) {
if (wire->port_input || wire->port_output || !wire->name.isPublic())
continue;
auto name_d = module->uniquify(stringf("%s_d", wire->name.c_str()));
auto name_x = module->uniquify(stringf("%s_x", wire->name.c_str()));
auto wire_d = module->addWire(name_d, GetSize(wire));
auto wire_x = module->addWire(name_x, GetSize(wire));
auto enc = encoded(wire);
module->connect(wire_d, enc.is_1);
module->connect(wire_x, enc.is_x);
module->wires_.erase(wire->name);
wire->attributes.erase(ID::fsm_encoding);
wire->name = NEW_ID_SUFFIX(wire->name.c_str());
module->wires_[wire->name] = wire;
}
}
void encode_remaining()
{
pool<Wire *> enc_undriven_wires;
@ -1083,6 +1109,13 @@ struct XpropPass : public Pass {
log(" the corresponding bit in <portname>_d is ignored for inputs and\n");
log(" guaranteed to be 0 for outputs.\n");
log("\n");
log(" -split-public\n");
log(" Replace each public non-port wire with two new wires, one carrying the\n");
log(" defined values (named <wirename>_d) and one carrying the mask of which\n");
log(" bits are x (named <wirename>_x). When a bit in the <portname>_x is set\n");
log(" the corresponding bit in <wirename>_d is guaranteed to be 0 for\n");
log(" outputs.\n");
log("\n");
log(" -assume-encoding\n");
log(" Add encoding invariants as assumptions. This can speed up formal\n");
log(" verification tasks.\n");
@ -1129,6 +1162,10 @@ struct XpropPass : public Pass {
options.split_outputs = true;
continue;
}
if (args[argidx] == "-split-public") {
options.split_public = true;
continue;
}
if (args[argidx] == "-assume-encoding") {
options.assume_encoding = true;
continue;
@ -1188,6 +1225,8 @@ struct XpropPass : public Pass {
worker.process_cells();
log_debug("Splitting ports.\n");
worker.split_ports();
log_debug("Splitting public signals.\n");
worker.split_public();
log_debug("Encode remaining signals.\n");
worker.encode_remaining();