Remove LEC (The-OpenROAD-Project#2126)

- Remove `LEC_ENABLE` and `logic_equiv_check`

configuration/general.tcl

@@ -19,7 +19,6 @@ set ::env(RSZ_MULTICORNER_LIB) 1
 set ::env(RSZ_DONT_TOUCH) ""
 
 # Flow Controls
-set ::env(LEC_ENABLE) 0
 set ::env(YOSYS_REWRITE_VERILOG) 0
 set ::env(RUN_FILL_INSERTION) 1
 set ::env(RUN_TAP_DECAP_INSERTION) 1

docs/source/reference/configuration.md

@@ -451,7 +451,6 @@ For more information on integrating macros and other relevant configuration vari
 
 |Variable|Description|
 |-|-|
-| `LEC_ENABLE` <a id="LEC_ENABLE"></a> | Enables logic verification using yosys, for comparing each netlist at each stage of the flow with the previous netlist and verifying that they are logically equivalent. Warning: this will increase the runtime significantly. 1 = Enabled, 0 = Disabled <br> (Default: `0`)|
 | `GENERATE_FINAL_SUMMARY_REPORT` <a id="GENERATE_FINAL_SUMMARY_REPORT"></a> | Specifies whether or not to generate a final summary report after the run is completed. Check command `generate_final_summary_report`. 1 = Enabled, 0 = Disabled. <br> (Default: `1`) |
 | `USE_GPIO_PADS` <a id="USE_GPIO_PADS"></a> | Decides whether or not to use the gpio pads in routing by merging their LEF file set in `::env(USE_GPIO_ROUTING_LEF)` and blackboxing their verilog modules set in `::env(GPIO_PADS_VERILOG)`. 1 = Enabled, 0 = Disabled. <br> (Default: `0`) |
 | `TAP_DECAP_INSERTION` <a id="TAP_DECAP_INSERTION"></a> | **Deprecated: Use `RUN_TAP_DECAP_INSERTION`**: Enables tap and decap cells insertion after floorplanning. 1 = Enabled, 0 = Disabled. |
@@ -469,3 +468,4 @@ For more information on integrating macros and other relevant configuration vari
 | `QUIT_ON_MISMATCHES` <a id="QUIT_ON_MISMATCHES"></a> | **Removed: See `./flow.tcl -ignore_mismatches`**: Whether to halt the flow execution or not if `TEST_MISMATCHES` is enabled and any mismatches are found. |
 | `KLAYOUT_XOR_GDS` <a id="KLAYOUT_XOR_GDS"></a> | **Removed: GDS always generated**: If `RUN_KLAYOUT_XOR` is enabled, this will enable producing a GDS output from the XOR along with it's PNG export. 1 = Enabled, 0 = Disabled.|
 | `KLAYOUT_XOR_XML` <a id="KLAYOUT_XOR_XML"></a> | **Removed: XML always generated**: If `RUN_KLAYOUT_XOR` is enabled, this will enable producing an XML output from the XOR. 1 = Enabled, 0 = Disabled. |
+| `LEC_ENABLE` <a id="LEC_ENABLE"></a> | **Removed: buggy** Enables logic verification using yosys, for comparing each netlist at each stage of the flow with the previous netlist and verifying that they are logically equivalent. Warning: this will increase the runtime significantly. 1 = Enabled, 0 = Disabled <br> (Default: `0`)|

docs/source/reference/openlane_commands.md

@@ -13,7 +13,6 @@ Most of the following commands' implementation exists in this [file][0]
 | Command      | Flags                   | Description                                           |
 |---------------|------------------------|-----------------------------------------|
 | `set_netlist <netlist>`   | | Sets the current netlist used by the flow to `<netlist>` |
-|    | `[-lec]` | Runs logic verification for the new netlist against the previous netlist, if `LEC_ENABLE` is set to 1. <br> Optional flag. |
 | `set_def <def>`   | | Sets the current def file used by the flow to `<def>` |
 | `prep_lefs`   | | prepares the used lef files by the flow. This process includes merging the techlef and cells lef, generating a merged.lef.|
 | `trim_lib`   | | prepares a liberty file (i.e. `LIB_SYNTH`) by trimming the `NO_SYNTH_CELL_LIST` and `DRC_EXCLUDE_CELL_LIST` from another input liberty file (i.e. `$::env(LIB_SYNTH_COMPLETE)`). |
@@ -108,15 +107,12 @@ Most of the following commands' implementation exists in this [file][9]
 
 | Command      | Flags                   | Description                                           |
 |---------------|------------------------|-----------------------------------------|
-| `run_yosys` | | Runs yosys synthesis on the design processed in the flow (the design is set by the `prep` command). if `LEC_ENABLE` is set to 1, a logic verification will be run after generating the new netlist vs the previous netlist if it exists. |
+| `run_yosys` | | Runs yosys synthesis on the design processed in the flow (the design is set by the `prep` command). |
 |    | `[-output <output_file>]` | Sets the outputfile from yosys synthesis. <br> Defaults to `/<run_path>/results/synthesis/<design_name>.synthesis.v`  <br> Optional flag.       |
 | `run_synthesis` | | Runs yosys synthesis on the current design as well as OpenSTA timing analysis on the generated netlist. The logs are produced under `/<run_path>/logs/synthesis/`, the timing reports are under `/<run_path>/reports/synthesis/`, and the synthesized netlist under `/<run_path>/results/synthesis/`. |
 | `run_synth_exploration` | | Runs synthesis exploration, which will try out the available synthesis strategies against the input design. The output will be the four possible gate level netlists under `<run_path>/results/synthesis` and a summary report under `<run_path>/reports` that compares the 4 outputs. |
 | `verilog_elaborate <optional args>` | | Runs on structural verilog (top-level netlists) and elaborates it. The `<optional args>` are used to control what is passed to `run_yosys` |
 | `yosys_rewrite_verilog <filename>` | | Runs yosys to rewrite the verilog given in `<filename>` into the already set environment variable `SAVE_NETLIST`.  Mainly used to generate explicit wire declarations |
-| `logic_equiv_check` | | Runs logic verification using yosys between the two given netlists. |
-|    | `-lhs <verilog_netlist_file>` | The first netlist (lefthand-side) in the logic verification comparison. |
-|    | `-rhs <verilog_netlist_file>` | The second netlist (righthand-side) in the logic verification comparison. |
 | `get_yosys_bin` | | **Removed: Read $::env(SYNTH_BIN)** Returns the used binary for yosys. |
 | `verilog_to_verilogPower` | | **Removed: Use `write_verilog -powered`** Adds the power pins and connections to a verilog file. |
 |    | `-input <verilog_netlist_file>` | The input verilog that doesn't contain the power pins and connections. |
@@ -132,6 +128,9 @@ Most of the following commands' implementation exists in this [file][9]
 |    | `[-power <power_pin>]` | The name of the power pin. <br> Defaults to `VDD_PIN` |
 |    | `[-ground <ground_pin>]` | The name of the ground pin. <br> Defaults to `GND_PIN` |
 |    | `[-powered_netlist <verilog_netlist_file>]` | The verilog netlist parsed from yosys that contains the internal power connections in case the design has internal macros file. <br> Defaults to `/<run_path>/tmp/synthesis/synthesis.pg_define.v` if `::env(SYNTH_USE_PG_PINS_DEFINES)` is defined, and to empty string otherwise. |
+| `logic_equiv_check` | | **Removed**: Runs logic verification using yosys between the two given netlists. |
+|    | `-lhs <verilog_netlist_file>` | The first netlist (lefthand-side) in the logic verification comparison. |
+|    | `-rhs <verilog_netlist_file>` | The second netlist (righthand-side) in the logic verification comparison. |
 
 ## Floorplan Commands
 

docs/source/usage/hardening_macros.md

@@ -208,8 +208,6 @@ You can run Antenna Checks using OpenROAD ARC or magic. This is controlled by `U
 
 You can control whether LVS should be run down to the device level or the cell level based on the type of the extraction. If you perform extraction on GDSII then it is going to be down to the device/transistor level, otherwise using the LEF/DEF views then it is going to be down to the cell/block level. This is controlled by `MAGIC_EXT_USE_GDS`.
 
-You can enable LEC on the different netlists by setting `LEC_ENABLE` to one, which should run logic verification after writing each intermediate netlist.
-
 A final summary report is produced by default as `<run-path>/reports/metrics.csv`, for more details about the contents of the report check [**Datapoint Definitions**](../reference/datapoint_definitions.md).
 
 A final manufacturability report is produced by default as `<run-path>/reports/manufacturability_report.csv`, this report contains the magic DRC, the LVS, and the antenna violations summaries.

scripts/tcl_commands/all.tcl

@@ -54,8 +54,8 @@ proc set_netlist {args} {
     try_exec sed -i.bak -e "s/\\(set ::env(CURRENT_NETLIST)\\).*/\\1 $replace/" "$::env(GLB_CFG_FILE)"
     exec rm -f "$::env(GLB_CFG_FILE).bak"
 
-    if { [info exists flags_map(-lec)] && $::env(LEC_ENABLE) && [file exists $previous_netlist] } {
-        logic_equiv_check -lhs $previous_netlist -rhs $netlist
+    if { [info exists flags_map(-lec)] } {
+        puts_warn "-lec is deprecated (LEC functionality has been removed)"
     }
 }
 

scripts/tcl_commands/synthesis.tcl

@@ -58,7 +58,7 @@ proc run_yosys {args} {
 
 
     if { ! [info exists flags_map(-no_set_netlist)] } {
-        set_netlist -lec $::env(SAVE_NETLIST)
+        set_netlist $::env(SAVE_NETLIST)
     }
 
     # The following is a naive workaround to OpenROAD not accepting defparams.
@@ -185,10 +185,6 @@ proc verilog_elaborate {args} {
 }
 
 proc yosys_rewrite_verilog {filename} {
-    if { !$::env(LEC_ENABLE) } {
-        puts_verbose "Skipping Verilog rewrite (logic equivalency checks are disabled)..."
-        return
-    }
     if { !$::env(YOSYS_REWRITE_VERILOG) } {
         puts_verbose "Skipping Verilog rewrite..."
         return
@@ -211,49 +207,6 @@ proc yosys_rewrite_verilog {filename} {
     exec echo "[TIMER::get_runtime]" | python3 $::env(SCRIPTS_DIR)/write_runtime.py "verilog rewrite - yosys"
 }
 
-
-proc logic_equiv_check {args} {
-    set options {
-        {-lhs required}
-        {-rhs required}
-    }
-
-    set flags {}
-
-    set args_copy $args
-    parse_key_args "logic_equiv_check" args arg_values $options flags_map $flags
-
-
-    if { [file exists $arg_values(-lhs).without_power_pins.v] } {
-        set ::env(LEC_LHS_NETLIST) $arg_values(-lhs).without_power_pins.v
-    } else {
-        set ::env(LEC_LHS_NETLIST) $arg_values(-lhs)
-    }
-
-    if { [file exists $arg_values(-rhs).without_power_pins.v] } {
-        set ::env(LEC_RHS_NETLIST) $arg_values(-rhs).without_power_pins.v
-    } else {
-        set ::env(LEC_RHS_NETLIST) $arg_values(-rhs)
-    }
-    increment_index
-    TIMER::timer_start
-    set log [index_file $::env(synthesis_logs).equiv.log]
-    set lhs_rel [relpath . $::env(LEC_LHS_NETLIST)]
-    set rhs_rel [relpath . $::env(LEC_RHS_NETLIST)]
-    puts_info "Running LEC: '$lhs_rel' vs. '$rhs_rel' (log: [relpath . $log])..."
-
-    if { [catch {run_yosys_script $::env(SCRIPTS_DIR)/yosys/logic_equiv_check.tcl -indexed_log $log}] } {
-        puts_err "$::env(LEC_LHS_NETLIST) is not logically equivalent to $::env(LEC_RHS_NETLIST)."
-        TIMER::timer_stop
-        exec echo "[TIMER::get_runtime]" | python3 $::env(SCRIPTS_DIR)/write_runtime.py "logic equivalence check - yosys"
-        throw_error
-    }
-
-    puts_info "$::env(LEC_LHS_NETLIST) and $::env(LEC_RHS_NETLIST) are proven equivalent"
-    TIMER::timer_stop
-    exec echo "[TIMER::get_runtime]" | python3 $::env(SCRIPTS_DIR)/write_runtime.py "logic equivalence check - yosys"
-}
-
 proc generate_blackbox_verilog {inputs output {defines ""}} {
     set defines_flag ""
     set ::env(YOSYS_IN) $inputs

scripts/utils/utils.tcl

@@ -769,7 +769,7 @@ proc run_tcl_script {args} {
             } elseif { $element == "sdc" } {
                 set_sdc $::env(SAVE_SDC)
             } elseif { $element == "netlist" } {
-                set_netlist -lec $::env(SAVE_NETLIST)
+                set_netlist $::env(SAVE_NETLIST)
             } elseif { $element == "guide" } {
                 set_guide $::env(SAVE_GUIDE)
             } else {