Optimization Parameter Variations Leading to Functional Divergence in LSOracle Synthesized Designs

[DeLoSoCode]

Dear LSOracle Community,

I have encountered an inconsistency issue during synthesis using LSOracle. My current setup includes the following versions: Yosys 0.41+126, ABC 1.01, and Icarus Verilog version 13.0 (devel) (s20221226-221-g272771d18).

During synthesis, we deviated from the default synthesis process and employed a custom sequence of optimization passes. The commands used for the two synthesis processes are as follows:

1.!yosys -p "read_verilog /home/user/LSOracle_project/rtl.v; synth; write_verilog /home/user/LSOracle_project/ori_syn_yosys.v"
2.!yosys -p "read_verilog /home/user/LSOracle_project/rtl.v; prep -ifx; prep -ifx; hierarchy; qwp -ltr; proc -nomux; opt_expr -mux_bool; opt_clean -purge; opt_dff -nodffe; opt_mem_feedback; opt_dff -nosdff; opt_reduce -full; opt_mem_feedback; opt_mem; opt_expr -keepdc; opt_expr -undriven; wreduce; opt_dff -nodffe; opt_dff -nosdff; opt_dff; opt_expr -full; opt_dff -keepdc; opt_mem; opt_expr -full; opt_clean; opt_lut; opt_clean; opt_reduce -full; opt_mem_feedback; opt_expr; opt_dff -nodffe; opt_dff -nosdff; opt_expr -mux_bool; opt_dff; opt_expr -mux_bool; check; opt_clean -purge; write_verilog /home/user/LSOracle_project/syn_yosys.v"

The changes in the optimization sequence should not affect the consistency of the code.

Attached are the relevant files and steps to reproduce the issue:

（1）rtl.v: Our design file.
（2）syn_yosys.v: The synthesized file generated using the original optimization sequence (commands saved in ori.lso script; can be executed in Ubuntu with ./core/lsoracle -f /home/user/LSOracle_project/ori.lso).
（3）change_syn_yosys.v: The synthesized file generated using the custom optimization sequence (commands saved in change.lso script; can be executed in Ubuntu with ./core/lsoracle -f /home/user/LSOracle_project/change.lso).
（4）yosys_testbench.v: The testbench file used for functional simulation. We performed functional simulation verification on both syn_yosys.v and change_syn_yosys.v using the Icarus Verilog simulator. The simulation results were saved in file1.txt and file2.txt. Comparing file1.txt and file2.txt, we found inconsistencies in the functional simulation results between syn_yosys.v and change_syn_yosys.v. However, the functional simulation results for the same design file should be consistent, regardless of the optimization parameter selections. (The commands for this step are stored in simulation.sh; you can execute bash simulation.sh after obtaining syn_yosys.v and change_syn_yosys.v to verify whether the functional simulation results of the two synthesized files are consistent.)

I would appreciate it if you could help identify the root cause of this issue. Thank you very much for your assistance.
synth.zip