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