Skip to content

global check #4224

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
nanocoh wants to merge 1 commit into
base: master
Choose a base branch
from
+21 −5
Open

global check #4224

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 3 additions & 1 deletion docs/user/FlowVariables.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -171,7 +171,7 @@ configuration file.
| <a name="LATCH_MAP_FILE"></a>LATCH_MAP_FILE| Optional mapping file supplied to Yosys to map latches| |
| <a name="LAYER_PARASITICS_FILE"></a>LAYER_PARASITICS_FILE| Path to per layer parasitics file. Defaults to $(PLATFORM_DIR)/setRC.tcl.| |
| <a name="LEC_AUX_VERILOG_FILES"></a>LEC_AUX_VERILOG_FILES| Additional Verilog files (e.g. blackbox stubs) to include in LEC equivalence checks. Appended to the generated Verilog netlist before running the formal equivalence check.| |
| <a name="LEC_CHECK"></a>LEC_CHECK| Perform a formal equivalence check between before and after netlists. If this fails, report an issue to OpenROAD.| 0|
| <a name="LEC_CHECK"></a>LEC_CHECK| Perform formal equivalence checks between before and after netlists. This checks CTS repair timing and the initial synthesis netlist against the final netlist. If this fails, report an issue to OpenROAD.| 0|
| <a name="LIB_FILES"></a>LIB_FILES| A Liberty file of the standard cell library with PVT characterization, input and output characteristics, timing and power definitions for each cell.| |
| <a name="MACRO_BLOCKAGE_HALO"></a>MACRO_BLOCKAGE_HALO| Distance beyond the edges of a macro that will also be covered by the blockage generated for that macro. Note that the default macro blockage halo comes from the largest of the specified MACRO_PLACE_HALO x or y values. This variable overrides that calculation.| |
| <a name="MACRO_EXTENSION"></a>MACRO_EXTENSION| Sets the number of GCells added to the blockages boundaries from macros.| |
Expand Down Expand Up @@ -342,6 +342,7 @@ configuration file.
- [DFF_LIB_FILE](#DFF_LIB_FILE)
- [DFF_MAP_FILE](#DFF_MAP_FILE)
- [LATCH_MAP_FILE](#LATCH_MAP_FILE)
- [LEC_CHECK](#LEC_CHECK)
- [MIN_BUF_CELL_AND_PORTS](#MIN_BUF_CELL_AND_PORTS)
- [POST_SYNTH_TCL](#POST_SYNTH_TCL)
- [PRE_SYNTH_TCL](#PRE_SYNTH_TCL)
Expand Down Expand Up @@ -588,6 +589,7 @@ configuration file.
- [CDL_FILE](#CDL_FILE)
- [GDS_ALLOW_EMPTY](#GDS_ALLOW_EMPTY)
- [GND_NETS_VOLTAGES](#GND_NETS_VOLTAGES)
- [LEC_CHECK](#LEC_CHECK)
- [MAX_ROUTING_LAYER](#MAX_ROUTING_LAYER)
- [MIN_ROUTING_LAYER](#MIN_ROUTING_LAYER)
- [POST_DENSITY_FILL_TCL](#POST_DENSITY_FILL_TCL)
Expand Down
5 changes: 5 additions & 0 deletions flow/scripts/final_report.tcl
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
utl::set_metrics_stage "finish__{}"
source $::env(SCRIPTS_DIR)/load.tcl
source $::env(SCRIPTS_DIR)/lec_check.tcl
erase_non_stage_variables final
load_design 6_1_fill.odb 6_1_fill.sdc
source_step_tcl PRE FINAL_REPORT
Expand All @@ -19,6 +20,10 @@ write_def $::env(RESULTS_DIR)/6_final.def
write_verilog $::env(RESULTS_DIR)/6_final.v \
-remove_cells [find_physical_only_masters]

if { $::env(LEC_CHECK) } {
run_lec_test 6_final 1_synth_lec.v 6_final.v
}
Comment on lines +23 to +25
Copy link
Copy Markdown

@gemini-code-assist gemini-code-assist Bot May 11, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

medium

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
}


# Run extraction and STA
if {
[env_var_exists_and_non_empty RCX_RULES]
Expand Down
4 changes: 4 additions & 0 deletions flow/scripts/synth_odb.tcl
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -31,3 +31,7 @@ orfs_write_db $::env(RESULTS_DIR)/1_synth.odb
# which are read in here and a canonicalized version is written
# out by OpenSTA that has no dependencies.
orfs_write_sdc $::env(RESULTS_DIR)/1_synth.sdc
if { $::env(LEC_CHECK) } {
write_verilog $::env(RESULTS_DIR)/1_synth_lec.v \
-remove_cells [find_physical_only_masters]
}
Comment on lines +34 to +37
Copy link
Copy Markdown

@gemini-code-assist gemini-code-assist Bot May 11, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

medium

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
}

6 changes: 4 additions & 2 deletions flow/scripts/variables.json
View file
Open in desktop

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

7 changes: 5 additions & 2 deletions flow/scripts/variables.yaml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1548,11 +1548,14 @@ WRITE_ODB_AND_SDC_EACH_STAGE:
default: 1
LEC_CHECK:
description: >
Perform a formal equivalence check between before and after netlists.
If this fails, report an issue to OpenROAD.
Perform formal equivalence checks between before and after netlists.
This checks CTS repair timing and the initial synthesis netlist against
the final netlist. If this fails, report an issue to OpenROAD.
default: 0
stages:
- synth
- cts
- final
LEC_AUX_VERILOG_FILES:
description: >
Additional Verilog files (e.g. blackbox stubs) to include in LEC
Expand Down