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

Merge pull request #3579 from jix/split_public_untested 

xprop: Add -split-public option
This commit is contained in:
Claire Xen 2022-12-08 20:05:56 +01:00 committed by GitHub
parent aeba966475 172a8e79f0
commit 4f36a86fff
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
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_inputs = false;
bool split_outputs = false; bool split_outputs = false;
bool split_public = false;
bool assume_encoding = false; bool assume_encoding = false;
bool assert_encoding = false; bool assert_encoding = false;
bool assume_def_inputs = false; bool assume_def_inputs = false;
@ -1018,6 +1019,31 @@ struct XpropWorker
module->fixup_ports(); 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() void encode_remaining()
{ {
pool<Wire *> enc_undriven_wires; 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(" the corresponding bit in <portname>_d is ignored for inputs and\n");
log(" guaranteed to be 0 for outputs.\n"); log(" guaranteed to be 0 for outputs.\n");
log("\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(" -assume-encoding\n");
log(" Add encoding invariants as assumptions. This can speed up formal\n"); log(" Add encoding invariants as assumptions. This can speed up formal\n");
log(" verification tasks.\n"); log(" verification tasks.\n");
@ -1129,6 +1162,10 @@ struct XpropPass : public Pass {
options.split_outputs = true; options.split_outputs = true;
continue; continue;
} }
if (args[argidx] == "-split-public") {
options.split_public = true;
continue;
}
if (args[argidx] == "-assume-encoding") { if (args[argidx] == "-assume-encoding") {
options.assume_encoding = true; options.assume_encoding = true;
continue; continue;
@ -1188,6 +1225,8 @@ struct XpropPass : public Pass {
worker.process_cells(); worker.process_cells();
log_debug("Splitting ports.\n"); log_debug("Splitting ports.\n");
worker.split_ports(); worker.split_ports();
log_debug("Splitting public signals.\n");
worker.split_public();
log_debug("Encode remaining signals.\n"); log_debug("Encode remaining signals.\n");
worker.encode_remaining(); worker.encode_remaining();