Inconsistent Synthesis Results with Custom Optimization Parameters 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 -ifx; hierarchy; flatten; proc -ifx; opt_dff -nodffe; opt_lut; opt_expr -noclkinv; memory_libmap; opt_lut; opt_dff -sat; opt_expr -undriven; memory_dff; opt_merge -share_all; memory_collect; opt_muxtree; fsm_map; opt_expr -mux_bool; opt_mem_priority; opt_dff -keepdc; memory_bmux2rom; opt_expr -noclkinv; opt_lut_ins; opt_expr -undriven; check; check; opt_muxtree; opt_expr -mux_undef; opt_merge; opt_mem; memory_bram; fsm_recode; opt_clean; opt_clean -purge; opt_reduce -full; opt_dff -nosdff; opt_expr -fine; opt_expr -full; fsm_extract; opt_dff -keepdc; fsm_recode; opt_expr -mux_bool; opt_mem; opt_merge -share_all; memory_collect; fsm_detect; opt_merge; opt_dff -nodffe; opt_reduce; opt_reduce -fine; opt_share; opt_clean -purge; memory_dff; wreduce; fsm_opt; opt_expr; memory_narrow; opt_expr -keepdc; opt_clean; opt_demorgan; opt_dff -nosdff; memory_bmux2rom; opt_expr -fine; techmap; check; fsm_detect; opt_dff -keepdc; opt_lut_ins; opt_clean -purge; check; opt_expr -full; opt_reduce -full; opt_expr; wreduce; opt_dff -nosdff; opt_reduce; opt_muxtree; opt_dff -nosdff; opt_expr -undriven; opt_mem; opt_reduce -fine; opt_clean; fsm_opt; memory_libmap; fsm_recode; fsm_recode; opt_expr -mux_bool; opt_merge; memory_collect; opt_expr -fine; opt_mem; opt_expr -mux_bool; opt_merge -share_all; memory_narrow; opt_expr -mux_undef; opt_dff -nodffe; memory_dff; memory_collect; fsm_extract; opt_dff -keepdc; memory_dff; opt_expr -fine; memory_bram; opt_lut; opt_muxtree; opt_share; memory_bmux2rom; opt_dff -sat; opt_expr -noclkinv; opt_expr -undriven; opt_merge -share_all; opt_dff -nodffe; memory_bmux2rom; opt_demorgan; opt_expr -noclkinv; opt_merge; opt_clean -purge; fsm_map; opt_clean; opt_expr -keepdc; opt_lut; opt_mem_priority; abc; opt_dff -nodffe; opt_expr; opt_muxtree; opt_expr -mux_bool; opt_merge; memory_collect; opt_share; memory_bram; opt_lut_ins; opt_reduce; opt_clean -purge; opt_dff -sat; opt_mem; memory_dff; opt_dff -nodffe; opt_expr -mux_bool; opt_expr -full; memory_libmap; opt_clean -purge; memory_bmux2rom; opt_mem; opt_mem_priority; memory_narrow; opt_dff -keepdc; wreduce; opt_expr -mux_undef; opt_clean; opt_expr -undriven; opt_dff -nosdff; fsm_recode; memory_dff; fsm_opt; opt_expr -noclkinv; opt_merge -share_all; opt_lut; opt_reduce -fine; opt_expr -undriven; opt_dff -keepdc; opt_reduce -full; opt_demorgan; opt_dff -nosdff; fsm_map; opt_expr -fine; opt_expr -noclkinv; check; memory_collect; opt_merge -share_all; opt_clean; opt_merge; fsm_detect; opt_expr -fine; check; memory_bmux2rom; fsm_recode; opt_muxtree; opt_lut; opt_expr -keepdc; fsm_extract; opt -fine; 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.
LSOracle_project.zip