xprop, setundef: Mark xprop decoding bwmuxes, exclude them from setundef

This adds the xprop_decoder attribute to bwmuxes that drive the original
unencoded signals. Setundef is changed to ignore the x inputs of these
bwmuxes, so that they survive the prep script of SBY's formal flow. This
is required to make simulation (via sim) using the prep model show the
decoded x signals instead of 0/1 values made up by the solver.
This commit is contained in:
Jannis Harder
2023-01-11 18:07:16 +01:00
parent 673ad561b8
commit 5042600c0d
3 changed files with 12 additions and 2 deletions
+9 -1
View File
@@ -502,7 +502,15 @@ struct SetundefPass : public Pass {
}
}
module->rewrite_sigspecs(worker);
for (auto &it : module->cells_)
if (!it.second->get_bool_attribute(ID::xprop_decoder))
it.second->rewrite_sigspecs(worker);
for (auto &it : module->processes)
it.second->rewrite_sigspecs(worker);
for (auto &it : module->connections_) {
worker(it.first);
worker(it.second);
}
if (worker.next_bit_mode == MODE_ANYSEQ || worker.next_bit_mode == MODE_ANYCONST)
{