diff --git a/passes/cmds/xprop.cc b/passes/cmds/xprop.cc index c2a1b5c44..fa1976b34 100644 --- a/passes/cmds/xprop.cc +++ b/passes/cmds/xprop.cc @@ -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 enc_undriven_wires; @@ -1083,6 +1109,13 @@ struct XpropPass : public Pass { log(" the corresponding bit in _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 _d) and one carrying the mask of which\n"); + log(" bits are x (named _x). When a bit in the _x is set\n"); + log(" the corresponding bit in _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();