synth command produces a non-equivalent circuit for a complex, fuzzed Verilog design #5428
Description
Version
0.56+30
On which OS did this happen?
Linux
Reproduction Steps
Thank you very much for your suggestions. This time I added flatten to my commands, but a problem similar to issue #5413 still occurred:
When I used the standard if command, the design failed the equivalence check. However, this error was avoided when we used a version that adds Hypergraph Partitioning functionality on top of the standard if command. By partitioning the circuit with the KaHyPar library and then performing the mapping under those partition constraints, the resulting netlist preserved all necessary logic and thus passed the equivalence check.
We performed an in-depth minimization attempt on this test case and came to the following key conclusions, which may be very helpful in locating the root cause of the problem:
The bug is related to the state of internal logic. The bug is only triggered when the logic cone of certain key registers (especially reg14) is treated as "internal logic" (i.e., it does not directly drive a primary output port). If reg14 is connected to a primary output, the bug disappears. This indicates that an internal logic cone with a specific structure and set of dependencies is the key to triggering this issue.
Read the original design
read_verilog /media/user/d/ZBY/test/circuit_04830.v
hierarchy -auto-top
proc
flatten
Save the pre-processed design
design -save original
Execute synthesis
synth -lut 6
Save the ABC-processed circuit as a Verilog variant file
write_verilog /media/user/d/QXY10/QXY/my-yosys-project/result/20251015_141308/variants/circuit_04830_variant.v
Save the synthesized design to a file
write_verilog -noattr -noexpr /media/user/d/QXY10/QXY/my-yosys-project/result/20251015_141308/circuit_04830_synth.v
Save the synthesized design
design -save synthesized
Prepare for equivalence check - use the correct copy method
design -reset
design -copy-from original -as gold top
design -copy-from synthesized -as gate top
Equivalence check
equiv_make gold gate equiv
equiv_simple
equiv_induct
equiv_status
Load the synthesized design for subsequent checks
design -load synthesized
Structural check
check
Statistics
stat
yosys_04830_if_and_hypergraph.zip
This time, I am providing the version that adds Hypergraph Partitioning functionality on top of the standard if command. This process involves partitioning the circuit using the KaHyPar library via hypergraph partitioning, and then performing the mapping under the resulting partition constraints.
We understand that because this introduces an external library, it may increase the difficulty for you to reproduce this part of the flow. However, the final results of both methods should be equivalent. Our reasoning is that we do not change the function of the nodes, but only reorganize them, and the core mapping algorithm itself remains unchanged.
detailed_theory.ipynb
I also used the other equivalence checking command you provided:
miter -equiv -flatten -make_assert -make_outputs gold gate miter
sat -verify -prove-asserts -seq 1 -show-inputs -show-outputs miter
Both runs succeeded using this command. However, I believe that using this command to check a sequential circuit with state machines is not rigorous enough. Therefore, I believe this bug must be occurring during the ABC stage.
Expected Behavior
They should all be equivalent.
Actual Behavior
When we used the if command, a non-equivalence situation occurred.