4 Commits

Author	SHA1	Message	Date
Jannis Harder	5042600c0d	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.	2023-01-11 18:07:16 +01:00
Jannis Harder	4a0ed35aab	xprop: Improve signal splitting code ... Avoid splitting output ports twice when combining -split-outputs with -split-public and clean up the corresponding code.	2022-12-12 17:51:01 +01:00
Jannis Harder	172a8e79f0	xprop: Add -split-public option	2022-12-08 20:00:01 +01:00
Jannis Harder	ce708122a5	New xprop pass to encode 3-valued x-propagation using 2-valued logic	2022-11-30 19:01:28 +01:00