diff --git a/configuration/general.tcl b/configuration/general.tcl index adfaa0515..8132619b9 100755 --- a/configuration/general.tcl +++ b/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 diff --git a/docs/source/reference/configuration.md b/docs/source/reference/configuration.md index 85f4eea81..6fde4f5eb 100644 --- a/docs/source/reference/configuration.md +++ b/docs/source/reference/configuration.md @@ -451,7 +451,6 @@ For more information on integrating macros and other relevant configuration vari |Variable|Description| |-|-| -| `LEC_ENABLE` | 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
(Default: `0`)| | `GENERATE_FINAL_SUMMARY_REPORT` | 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.
(Default: `1`) | | `USE_GPIO_PADS` | 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.
(Default: `0`) | | `TAP_DECAP_INSERTION` | **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` | **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` | **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` | **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` | **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
(Default: `0`)| diff --git a/docs/source/reference/openlane_commands.md b/docs/source/reference/openlane_commands.md index 1b066e8eb..4b7610055 100644 --- a/docs/source/reference/openlane_commands.md +++ b/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 ` | | Sets the current netlist used by the flow to `` | -| | `[-lec]` | Runs logic verification for the new netlist against the previous netlist, if `LEC_ENABLE` is set to 1.
Optional flag. | | `set_def ` | | Sets the current def file used by the flow to `` | | `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 ]` | Sets the outputfile from yosys synthesis.
Defaults to `//results/synthesis/.synthesis.v`
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 `//logs/synthesis/`, the timing reports are under `//reports/synthesis/`, and the synthesized netlist under `//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 `/results/synthesis` and a summary report under `/reports` that compares the 4 outputs. | | `verilog_elaborate ` | | Runs on structural verilog (top-level netlists) and elaborates it. The `` are used to control what is passed to `run_yosys` | | `yosys_rewrite_verilog ` | | Runs yosys to rewrite the verilog given in `` 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 ` | The first netlist (lefthand-side) in the logic verification comparison. | -| | `-rhs ` | 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 ` | 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 ]` | The name of the power pin.
Defaults to `VDD_PIN` | | | `[-ground ]` | The name of the ground pin.
Defaults to `GND_PIN` | | | `[-powered_netlist ]` | The verilog netlist parsed from yosys that contains the internal power connections in case the design has internal macros file.
Defaults to `//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 ` | The first netlist (lefthand-side) in the logic verification comparison. | +| | `-rhs ` | The second netlist (righthand-side) in the logic verification comparison. | ## Floorplan Commands diff --git a/docs/source/usage/hardening_macros.md b/docs/source/usage/hardening_macros.md index 00638dd0e..3b32abf61 100644 --- a/docs/source/usage/hardening_macros.md +++ b/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 `/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 `/reports/manufacturability_report.csv`, this report contains the magic DRC, the LVS, and the antenna violations summaries. diff --git a/scripts/tcl_commands/all.tcl b/scripts/tcl_commands/all.tcl index d697ac5d0..28bdb587d 100755 --- a/scripts/tcl_commands/all.tcl +++ b/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)" } } diff --git a/scripts/tcl_commands/synthesis.tcl b/scripts/tcl_commands/synthesis.tcl index 8abccab87..44d42bf50 100755 --- a/scripts/tcl_commands/synthesis.tcl +++ b/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 diff --git a/scripts/utils/utils.tcl b/scripts/utils/utils.tcl index 66e1a631b..5269ff78e 100755 --- a/scripts/utils/utils.tcl +++ b/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 { diff --git a/scripts/yosys/logic_equiv_check.tcl b/scripts/yosys/logic_equiv_check.tcl deleted file mode 100755 index 52a4fbef0..000000000 --- a/scripts/yosys/logic_equiv_check.tcl +++ /dev/null @@ -1,76 +0,0 @@ -# Copyright 2020-2022 Efabless Corporation -# -# Licensed under the Apache License, Version 2.0 (the "License"); -# you may not use this file except in compliance with the License. -# You may obtain a copy of the License at -# -# http://www.apache.org/licenses/LICENSE-2.0 -# -# Unless required by applicable law or agreed to in writing, software -# distributed under the License is distributed on an "AS IS" BASIS, -# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. -# See the License for the specific language governing permissions and -# limitations under the License. -yosys -import - -proc exclude_fills {args} { - set fills "$::env(CELL_PAD_EXCLUDE)" - foreach fill_wildcard $fills { - hierarchy -generate $fill_wildcard - } -} - -proc initialize {args} { - if { [info exists ::env(SYNTH_DEFINES) ] } { - foreach define $::env(SYNTH_DEFINES) { - puts "Defining $define" - verilog_defines -D$define - } - } - if { [info exists ::env(VERILOG_FILES_BLACKBOX)] } { - foreach verilog_file $::env(VERILOG_FILES_BLACKBOX) { - read_verilog -lib $verilog_file - } - } - foreach lib $::env(LIB_TYPICAL) { - read_liberty -ignore_miss_func -ignore_miss_dir $lib - } -} - -proc read_nl {netlist name} { - initialize - read_verilog $netlist - - rmports - - exclude_fills - - splitnets -ports - hierarchy -top $::env(DESIGN_NAME) - - if { $::env(SYNTH_FLAT_TOP) } { - flatten - } - - stat - renames -top $name - design -stash $name -} - -# LHS -read_nl $::env(LEC_LHS_NETLIST) gold - -# RHS -read_nl $::env(LEC_RHS_NETLIST) gate - -# LEC -design -copy-from gold -as gold gold -design -copy-from gate -as gate gate - -initialize -exclude_fills - -equiv_make gold gate equiv -prep -flatten -top equiv -equiv_simple -seq 10 -v -equiv_status -assert