Skip to content

LEC_CHECK: default 0 for out of tree designs #3908

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
oharboe wants to merge 1 commit into
base: master
Choose a base branch
from
+12 −3
Open

LEC_CHECK: default 0 for out of tree designs #3908

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
2 changes: 1 addition & 1 deletion docs/user/FlowVariables.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -161,7 +161,7 @@ configuration file.
| <a name="KLAYOUT_TECH_FILE"></a>KLAYOUT_TECH_FILE| A mapping from LEF/DEF to GDS using the KLayout tool.| |
| <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_CHECK"></a>LEC_CHECK| Perform a formal equivalence check between before and after netlists.| 1|
| <a name="LEC_CHECK"></a>LEC_CHECK| This is primarily an ORFS CI regression testing feature and is default 0 for DESIGN_CONFIG pointing designs outside of the ORFS tree. Requires `KEPLER_FORMAL_EXE` to point to a built Kepler executable.| |
| <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
7 changes: 7 additions & 0 deletions flow/scripts/variables.mk
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,13 @@

export DESIGN_NICKNAME?=$(DESIGN_NAME)

ifneq ($(findstring $(abspath $(FLOW_HOME)),$(abspath $(DESIGN_CONFIG))),)
export ORFS_TEST_SUITE_DESIGN := 1
else
export ORFS_TEST_SUITE_DESIGN := 0
endif
export LEC_CHECK ?= $(ORFS_TEST_SUITE_DESIGN)

#-------------------------------------------------------------------------------
# Setup variables to point to other location for the following sub directory
# - designs - default is under current directory
Expand Down
6 changes: 4 additions & 2 deletions flow/scripts/variables.yaml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1297,8 +1297,10 @@ WRITE_ODB_AND_SDC_EACH_STAGE:
default: 1
LEC_CHECK:
description: >
Perform a formal equivalence check between before and after netlists.
default: 1
This is primarily an ORFS CI regression testing feature and is default 0
Copy link
Member

@maliberty maliberty Feb 23, 2026

Choose a reason for hiding this comment

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

I don't agree with this description. Anyone doing production work will likely want LEC checking. I can see not wanting to spend the time while prototyping.

The in-tree / out-of-tree distinction is a bit odd. I think it works for your particular use case but isn't that general. Perhaps it would be better to have an option project setting file you could put it there.

Copy link
Collaborator Author

@oharboe oharboe Feb 23, 2026 •
edited
Loading

Choose a reason for hiding this comment

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

I think there are two use-cases, or concerns, that should be clearly separated: development of ORFS/OpenROAD and usage of OpenROAD/ORFS.

For the usage use-case(where I'm not an OpenROAD developer, but a user), I think LEC should be default off for out of tree designs: minimum dependencies, fast lean, optional(for architectural exploration I don't care about correctness of throwaway results). I trust OpenROAD and only need LEC as a last crossing of t's and dotting's of i's. I don't want to bog down day to day CI wasted compute or extra dependencies.

For the OpenROAD/ORFS development use-case, I have no strong opinions, I think OpenROAD/ORFS developers are the best to judge and I think that they should be free to do so without worrying about the user-experience.

For the user's use-case, how about a more explicit invocation like make lec-floorplan/place/cts/grt/drt/final that checks previous stage against current stage?

make lec-final should probably do a LEC against drt as well as synthesis netlist following POLA.

I think the user use-case can be kicked down the road until we have more milage on LEC and we know that it works and is scalable for production, so this PR is good to go from that perspective.

for DESIGN_CONFIG pointing designs outside of the ORFS tree.

Requires `KEPLER_FORMAL_EXE` to point to a built Kepler executable.
stages:
- cts
REMOVE_CELLS_FOR_LEC:
Expand Down