Global LEC check#4223
Conversation
d4f25f6 to
9671320
Compare
There was a problem hiding this comment.
Code Review
This pull request expands the Logical Equivalence Check (LEC) functionality by integrating it into the synthesis and final stages of the flow, with corresponding updates to documentation and scripts. Feedback recommends using the write_lec_verilog helper function instead of direct write_verilog calls to ensure auxiliary files are correctly handled and to prevent LEC-specific stubs from polluting the main output netlists.
I am having trouble creating individual review comments. Click here to see my feedback.
flow/scripts/synth_odb.tcl (34-37)
Instead of calling write_verilog directly, use the write_lec_verilog helper from lec_check.tcl. This ensures that REMOVE_CELLS_FOR_LEC and LEC_AUX_VERILOG_FILES (e.g., blackbox stubs) are correctly handled for the synthesis netlist, which is necessary for a successful LEC when blackboxes are present. Note that you'll need to source lec_check.tcl within the block.
if { $::env(LEC_CHECK) } {
source $::env(SCRIPTS_DIR)/lec_check.tcl
write_lec_verilog 1_synth_lec.v
}
flow/scripts/final_report.tcl (23-25)
Use write_lec_verilog to generate a dedicated netlist for LEC. This ensures that any auxiliary Verilog files (stubs) or extra cell removals are included in the comparison. Additionally, using a separate file like 6_final_lec.v avoids polluting the main output netlist 6_final.v with LEC-specific stubs, which could otherwise interfere with downstream tools like STA if the file is reused.
if { $::env(LEC_CHECK) } {
write_lec_verilog 6_final_lec.v
run_lec_test 6_final 1_synth_lec.v 6_final_lec.v
}
No description provided.