Functional Inconsistencies in Verilog Synthesis Due to Non-Default Optimization Paths in LSOracle

[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 -memx; hierarchy; qwp -grid N; proc -noopt; opt_expr; opt_mem_feedback; opt_share; opt_expr -mux_undef; opt_merge; opt_expr -undriven; opt_expr -full; opt_merge; opt_expr -fine; opt_mem_widen; opt_expr -full; opt_expr -noclkinv; opt_mem_priority; opt_dff -nosdff; opt_ffinv; opt_reduce -fine; opt_expr -full; opt_expr -full; opt_lut_ins; opt_expr -undriven; opt_expr -mux_undef; opt_ffinv; opt_expr -noclkinv; wreduce; opt_mem_feedback; opt_expr -keepdc; opt_clean -purge; wreduce; opt_ffinv; opt_lut_ins; opt_lut; opt_reduce -full; opt_reduce -fine; opt_reduce -fine; opt_expr -fine; opt_expr -mux_undef; opt_ffinv; opt_clean; opt_expr -mux_undef; opt_reduce -full; opt_lut; opt_expr -mux_undef; opt_mem_widen; opt_expr; opt_expr -mux_undef; wreduce; opt_lut; opt_expr; opt_lut; opt_expr -mux_undef; opt_demorgan; opt_dff -nodffe; opt_reduce -fine; opt_demorgan; opt_expr -undriven; opt_dff -sat; opt_mem_priority; wreduce; opt_expr -undriven; opt_mem_widen; opt_dff; opt_reduce; opt_mem_feedback; opt_reduce -full; opt_expr -full; opt_clean -purge; opt_reduce -full; opt_expr; opt_expr -keepdc; opt_lut_ins; opt_lut; opt_mem_feedback; opt_demorgan; opt_expr -keepdc; opt_expr -keepdc; opt_reduce -full; opt_expr -mux_undef; opt_merge; opt_mem_widen; opt_clean -purge; opt_expr -mux_bool; opt_expr -keepdc; opt_expr -noclkinv; opt_lut_ins; opt_expr -full; opt_expr -full; wreduce; opt_expr -keepdc; opt_mem; opt_clean -purge; opt_mem_feedback; opt_dff; opt_mem_feedback; opt_mem_feedback; opt_mem_widen; opt_expr; opt_merge -share_all; opt_expr -noclkinv; opt_dff; opt_mem_feedback; opt_merge -share_all; opt_mem_feedback; opt_ffinv; opt_mem_priority; opt_expr -full; opt_dff -nosdff; opt_reduce -fine; opt_lut_ins; opt_expr -keepdc; opt_merge -share_all; opt_expr -noclkinv; opt_reduce -full; opt_dff; check; wreduce; opt_expr; wreduce; opt_reduce -fine; opt_expr -keepdc; wreduce; opt_dff -keepdc; opt_expr -noclkinv; opt_reduce -fine; opt_reduce -full; opt_mem_widen; opt_muxtree; opt_ffinv; opt_clean -purge; opt_dff -nodffe; opt_expr; opt_lut; opt_expr -mux_bool; opt_lut; opt_demorgan; opt_reduce; opt_ffinv; opt_ffinv; opt_mem_priority; opt_clean; opt_reduce; opt_expr -undriven; opt_expr -fine; opt_expr -undriven; opt_reduce -fine; opt_clean -purge; opt_expr -mux_undef; opt_lut; opt_reduce -full; opt_expr -keepdc; opt_expr -mux_bool; opt_dff; opt_lut; opt_merge; opt_expr -undriven; opt_ffinv; opt_expr -keepdc; opt_clean -purge; wreduce; opt_ffinv; fsm -export; opt_expr -keepdc; opt_expr -full; opt_merge -share_all; opt_expr -full; opt_clean -purge; opt_expr -mux_undef; opt_lut; opt_lut; opt_dff; wreduce; opt_expr -fine; opt_expr -full; opt_expr -full; opt_reduce -fine; opt_merge -share_all; opt_lut_ins; opt_expr -noclkinv; opt_mem_widen; opt_reduce -fine; opt_reduce -full; opt_mem_feedback; opt_lut_ins; opt_expr -mux_undef; opt_dff; opt_expr -noclkinv; opt_clean -purge; wreduce; opt_reduce -fine; opt_expr -fine; opt_lut; opt_merge; opt_mem_priority; opt_expr -mux_undef; opt_expr; opt_ffinv; opt_ffinv; opt_expr -undriven; opt_mem_priority; opt_clean -purge; opt_reduce -fine; opt_reduce -full; wreduce; opt_dff; opt_mem_widen; opt_expr -full; wreduce; opt_expr -keepdc; opt_ffinv; check; opt_dff -nodffe; wreduce; opt_clean; opt_expr -mux_undef; opt_dff -nodffe; opt_ffinv; opt_expr -undriven; opt_lut; opt_mem_widen; opt_mem_feedback; opt_ffinv; opt_expr -undriven; opt_ffinv; opt_expr -keepdc; opt_mem_priority; opt_expr -noclkinv; opt_expr; opt_expr -undriven; opt_mem_priority; opt_mem_feedback; opt_expr; opt_expr -full; opt_reduce -fine; opt_lut_ins; opt_demorgan; opt_clean; opt_reduce -full; opt_reduce; opt_expr -undriven; opt_dff -nosdff; opt_ffinv; opt_expr; opt_expr -keepdc; wreduce; opt_expr -undriven; opt_expr -mux_undef; opt_clean -purge; opt_mem; opt_merge; opt_expr -noclkinv; opt_mem_widen; opt_clean -purge; opt_reduce -full; opt_muxtree; opt_dff -sat; opt_merge; opt_merge -share_all; opt_expr -keepdc; opt_expr -mux_undef; opt_expr -fine; opt_lut; opt_share; opt_reduce -full; opt_reduce -full; opt_lut_ins; opt_mem_widen; opt_reduce -fine; opt_lut; opt_demorgan; opt_expr -undriven; wreduce; opt_expr -noclkinv; opt_lut; opt_expr -mux_bool; opt_expr -mux_bool; opt_demorgan; opt_expr -keepdc; opt_dff -nosdff; opt_expr -mux_undef; opt_expr; wreduce; opt_clean -purge; opt_expr; opt_expr -mux_undef; opt_dff; opt_expr; opt_mem_widen; opt_expr -mux_undef; opt_clean -purge; opt_expr -full; opt_dff; opt_demorgan; opt_expr -full; opt_expr -keepdc; opt_mem_feedback; opt_mem_feedback; wreduce; opt_lut_ins; opt_expr -noclkinv; opt_ffinv; opt_reduce -full; opt_dff -keepdc; opt_expr -mux_bool; opt_reduce -full; opt_lut; opt_expr -keepdc; opt_expr -keepdc; opt_mem_feedback; opt_lut; opt_mem_feedback; opt_mem_feedback; opt_expr -keepdc; opt_reduce -fine; opt_merge; opt_ffinv; opt_reduce; opt_ffinv; opt_reduce; opt_mem_feedback; opt_reduce -fine; memory; opt_reduce -fine; opt_demorgan; wreduce; opt_expr; opt_expr -keepdc; opt_expr -full; wreduce; opt_reduce -full; opt_merge -share_all; opt_ffinv; opt_mem_feedback; opt_lut; opt_expr -mux_undef; opt_expr -mux_bool; opt_dff; opt_ffinv; opt_expr -full; opt_lut; opt_clean -purge; opt_expr -mux_undef; opt_merge -share_all; opt_clean -purge; opt_expr; opt_reduce -full; opt_expr -keepdc; opt_dff; check; opt_expr -undriven; opt_expr -keepdc; opt_expr -full; opt_expr -full; opt_reduce -fine; opt_dff; opt_mem_feedback; opt_mem_feedback; opt_expr -mux_undef; opt_expr -mux_undef; opt_ffinv; opt_ffinv; opt_expr; opt_dff; opt_expr -mux_undef; opt_expr; opt_expr -fine; opt_demorgan; wreduce; opt_mem_widen; opt_ffinv; opt_mem_feedback; opt_dff -nosdff; opt_lut_ins; opt_lut; opt_mem_priority; opt_merge; opt_dff -sat; opt_share; opt_lut_ins; opt_expr -full; opt_reduce -full; opt_expr; opt_reduce; opt_merge -share_all; opt_mem; opt_expr -noclkinv; opt_expr -undriven; opt_expr -full; opt_expr -fine; opt_mem_widen; opt_lut; opt_reduce -full; opt_reduce -fine; opt_expr -mux_undef; opt_mem_widen; opt_expr -undriven; opt_mem_priority; opt_expr -undriven; opt_demorgan; opt_expr -keepdc; opt_clean -purge; opt_dff -nosdff; opt_ffinv; opt_lut; opt_expr -keepdc; opt_reduce -fine; opt_dff -nodffe; opt_mem_priority; opt_expr -noclkinv; opt_dff; opt_expr -keepdc; opt_expr -keepdc; opt_lut_ins; opt_ffinv; opt_reduce -full; opt_reduce -fine; opt_lut; opt_ffinv; opt_merge; opt_lut; opt_ffinv; opt_clean -purge; opt_mem_feedback; opt_expr; opt_expr -noclkinv; opt_expr -undriven; wreduce; opt_expr -mux_bool; opt_clean; opt_clean -purge; opt_mem_feedback; opt_mem_feedback; opt_dff -keepdc; opt_expr -noclkinv; wreduce; opt_expr -full; opt_expr -noclkinv; opt_expr -noclkinv; opt_lut; opt_lut_ins; wreduce; opt_lut; opt_reduce; opt_demorgan; wreduce; opt_expr -mux_undef; opt_expr -full; opt_mem_widen; opt_merge; opt_clean -purge; opt_mem_widen; opt_dff -nodffe; wreduce; opt_clean; opt_muxtree; opt_expr -undriven; opt_reduce -full; opt_reduce -fine; opt_merge; opt_expr -fine; opt_lut_ins; opt_reduce; opt_reduce -full; opt_clean -purge; opt_expr -mux_undef; opt_expr -keepdc; opt_expr -mux_undef; opt_ffinv; opt_expr -undriven; opt_expr -mux_bool; opt_mem_feedback; opt_mem_priority; wreduce; opt_expr; opt_reduce -fine; opt_expr -keepdc; opt_reduce -fine; opt_mem_widen; opt_reduce -full; opt_mem_feedback; opt_expr -keepdc; techmap; opt_merge; opt_expr -full; opt_expr; opt_demorgan; opt_ffinv; opt_expr -mux_undef; opt_clean -purge; opt_mem_feedback; opt_expr -keepdc; opt_mem_feedback; opt_expr; opt_mem; opt_reduce; opt_dff; opt_expr -undriven; opt_dff -nodffe; opt_reduce -fine; wreduce; opt_clean -purge; opt_mem_feedback; opt_ffinv; opt_clean -purge; opt_mem_widen; opt_mem_feedback; opt_dff; opt_expr -noclkinv; opt_ffinv; opt_expr -mux_undef; opt_lut; opt_expr -fine; opt_expr -mux_undef; opt_lut; opt_expr; opt_expr -keepdc; opt_clean -purge; opt_ffinv; opt_mem_priority; opt_expr -mux_bool; wreduce; opt_reduce -full; opt_demorgan; opt_merge -share_all; opt_expr -keepdc; opt_lut; opt_mem_feedback; opt_expr -undriven; opt_expr -mux_undef; opt_expr -noclkinv; opt_demorgan; opt_expr -mux_undef; opt_share; opt_lut_ins; opt_reduce -full; opt_expr -noclkinv; opt_reduce -fine; opt_clean -purge; opt_merge; opt_mem_feedback; opt_lut_ins; wreduce; opt_dff; opt_lut_ins; opt_clean -purge; opt_expr -undriven; opt_expr; opt_expr -full; opt_merge; opt_ffinv; opt_expr -mux_undef; wreduce; check; opt_reduce -full; opt_clean; opt_lut; opt_lut; opt_ffinv; opt_mem_priority; opt_dff; opt_expr -noclkinv; opt_reduce -full; opt_merge -share_all; opt_expr -keepdc; opt_expr -full; opt_mem_widen; opt_dff; opt_expr -full; opt_expr -keepdc; opt_ffinv; opt_muxtree; opt_mem_feedback; opt_expr -fine; opt_expr -full; opt_expr -mux_bool; opt_expr; opt_reduce -full; opt_expr -mux_undef; opt_expr -full; wreduce; wreduce; opt_mem_widen; opt_reduce -full; opt_ffinv; opt_reduce -fine; opt_lut_ins; opt_expr; opt_reduce -full; opt_expr -full; opt_dff -sat; opt_reduce -fine; opt_reduce -full; opt_expr -keepdc; opt_reduce; opt_expr; opt_expr -mux_undef; opt_expr -keepdc; opt_reduce -fine; opt_expr -keepdc; wreduce; opt_dff -nosdff; opt_clean -purge; opt_expr -undriven; opt_expr -noclkinv; opt_mem_feedback; opt_reduce; opt_demorgan; opt_lut; opt_dff -nodffe; opt_reduce -fine; opt_clean; opt_expr -noclkinv; opt_expr -mux_bool; opt_mem_priority; opt_expr -keepdc; opt_lut; opt_reduce -fine; opt_lut; opt_mem_widen; opt_ffinv; opt_expr -fine; opt_dff -keepdc; opt_ffinv; opt_expr -full; wreduce; opt_mem_widen; opt_expr -undriven; opt_expr -undriven; opt_mem_priority; opt_reduce -fine; opt_mem_feedback; opt_expr -keepdc; opt_merge; opt_expr -mux_undef; opt_lut; opt_lut_ins; opt_expr -undriven; opt_mem_widen; wreduce; opt_dff -nosdff; opt_merge -share_all; abc; opt_expr -undriven; opt_ffinv; opt_dff; opt_expr -full; opt_reduce -full; opt_lut; opt_expr -mux_undef; opt_mem_feedback; opt_lut; opt_merge; opt_merge; opt_expr -mux_undef; opt_dff -nosdff; opt_expr -keepdc; opt_dff; opt_expr -undriven; opt_share; opt_expr -full; opt_reduce -fine; opt_mem_widen; opt_expr -keepdc; opt_reduce -full; opt_merge -share_all; opt_ffinv; opt_dff; opt_mem_feedback; opt_lut; opt_expr -mux_undef; opt_mem_widen; opt_expr -mux_undef; opt_expr -undriven; opt_expr -noclkinv; opt_expr -full; opt_expr -undriven; opt_mem_feedback; opt_lut_ins; opt_dff -sat; wreduce; opt_lut; opt_mem_priority; opt_mem_feedback; opt_expr -noclkinv; opt_expr -full; opt_reduce -fine; wreduce; opt_expr; opt_reduce; opt_mem_widen; opt_expr -noclkinv; opt_mem_priority; wreduce; opt_expr; opt_clean -purge; opt_expr -mux_undef; opt_mem_widen; opt_demorgan; opt_mem_priority; opt_lut_ins; opt_reduce -full; opt_reduce -full; opt_demorgan; opt_ffinv; opt_reduce -full; opt_clean; opt_expr -full; opt_demorgan; opt_lut; opt_clean -purge; opt_expr -keepdc; opt_expr -mux_bool; opt_expr -fine; opt_dff; opt_lut; opt_expr -fine; opt_muxtree; opt_expr -mux_undef; wreduce; opt_reduce -fine; opt_expr; opt_reduce -full; wreduce; opt_expr -mux_undef; opt_expr; opt_mem_feedback; opt_lut; opt_mem_priority; opt_ffinv; opt_lut_ins; opt_lut_ins; check; opt_expr -keepdc; opt_dff -nodffe; opt_clean -purge; wreduce; opt_reduce -fine; opt_ffinv; opt_ffinv; opt_ffinv; opt_expr -keepdc; opt_reduce -full; opt_clean -purge; opt_mem_feedback; opt_merge; opt_reduce -full; opt_lut; opt_merge; opt_expr -full; opt_ffinv; opt_expr; opt_reduce -fine; opt_expr -keepdc; opt_merge -share_all; opt_clean; opt_ffinv; opt_expr; opt_expr -noclkinv; opt_mem_widen; opt_expr -undriven; opt_dff -keepdc; wreduce; opt_expr -noclkinv; opt_reduce -fine; opt_expr -full; opt_lut_ins; opt_lut; wreduce; opt_clean -purge; opt_expr -mux_undef; opt_ffinv; opt_clean -purge; opt_mem_widen; opt_mem_feedback; opt_dff -nodffe; opt_expr -mux_bool; opt_mem_feedback; opt_expr -keepdc; opt_expr -keepdc; opt_expr -keepdc; opt_expr -undriven; opt_mem_feedback; opt_mem; opt_expr -noclkinv; opt_merge -share_all; opt_expr -mux_bool; opt_clean -purge; opt_dff -nosdff; opt_expr -keepdc; opt_expr -full; opt_expr -undriven; opt_expr -fine; opt_expr -mux_undef; opt_expr; opt_reduce -fine; wreduce; opt_reduce; opt_reduce -fine; opt_reduce; opt_dff; opt_demorgan; 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