global check

[nanocoh]

No description provided.

[gemini-code-assist]

Code Review

This pull request expands the Logical Equivalence Check (LEC_CHECK) functionality to the synthesis and final stages of the flow, updating documentation and variable definitions accordingly. Feedback suggests using the specialized write_lec_verilog procedure instead of write_verilog in the Tcl scripts. This ensures that LEC-specific requirements, such as blackbox stubs and cell removals, are properly handled without modifying the final deliverable netlists.

[gemini-code-assist]

Instead of calling write_verilog directly, you should use the write_lec_verilog procedure defined in lec_check.tcl. This ensures that the generated netlist respects REMOVE_CELLS_FOR_LEC and includes any LEC_AUX_VERILOG_FILES (like blackbox stubs), which are critical for a successful formal equivalence check. You will also 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
}

[gemini-code-assist]

It is recommended to use write_lec_verilog to generate a specific netlist for the LEC test (e.g., 6_final_lec.v) rather than using the deliverable 6_final.v. This ensures the revised netlist contains the necessary stubs and removed cells for the formal check without polluting the final output file. Using the helper procedure also ensures consistency with how the golden netlist was generated.

if { $::env(LEC_CHECK) } {
  write_lec_verilog 6_final_lec.v
  run_lec_test 6_final 1_synth_lec.v 6_final_lec.v
}