SEC/LEC scripts refactor

scripts/slec/README.md

@@ -1,51 +1,61 @@
-# Logic Equivalence Checking (LEC)
+# Sequential Logic Equivalence Checking (SLEC)
 
-This folder contains a LEC script that runs on both 
-Synopsys Formality and Cadence Design Systems Conformal.
+This folder contains a SLEC script that runs:
 
-This script allows to catch non-logical equivalent changes on the RTL which are forbidden
-on the verified paramter set.
+- LEC: Synopsys Formality and Cadence Design Systems Conformal.
+- SEC: Siemens SLEC App
 
 Please have a look at: https://cv32e40p.readthedocs.io/en/latest/core_versions/
 
-The `cv32e40p_v1.0.0` tag refers to the frozen RTL. The RTL has been verified and frozen on a given value of the input parameter of the design. Unless a bug is found, it is forbidden to change the RTL
-in a non-logical equivalent manner for PPA optimizations of any other change.
-Instead, it is possible to change the RTL on a different value of the parameter set, which has not been verified yet.
-For example, it is possible to change the RTL design when the `FPU` parameter is set to 1 as this configuration has not been verified yet. However, the design must be logically equivalent when the parameter is set back to 0.
-It is possible to change the `apu` interface and the `pulp_clock_en_i` signal on the frozen parameter set as these
-signals are not used when the parameter `FPU` and `PULP_CLUSTER` are set to 0, respectively.
-
-The current scripts have been tried on Synopsys Formality `2021.06-SP5` and Cadence Design Systems Conformal `20.20` on a 64 bit executable.
+The `cv32e40p_v1.0.0` tag refers to the frozen RTL. The RTL has been verified
+and frozen on a given value of the input parameter of the design. Unless a bug
+is found, it is forbidden to change the RTL in a non-logical equivalent manner
+for PPA optimizations of any other change.
+Instead, it is possible to change the RTL on a different value of the parameter
+set, which has not been verified yet.
+For example, it is possible to change the RTL design when the `FPU` parameter is
+set to 1 as this configuration has not been verified yet. However, the design
+must be logically equivalent when the parameter is set back to 0.
+It is possible to change the `apu` interface and the `pulp_clock_en_i` signal on
+the frozen parameter set as these signals are not used when the parameter `FPU`
+and `PULP_CLUSTER` are set to 0, respectively.
+
+The current scripts have been tried on Synopsys Formality `2021.06-SP5` ,
+Cadence Design Systems Conformal `20.20` and Siemens SLEC App `2023.4`.
 
 ### Running the script
 
-From a bash shell, please execute:
+From a bash shell using LEC, please execute:
 
 ```
-./lec.sh synopsys
+./run.sh -t synopsys -p lec
 ```
  or
 
-```
-./lec.sh cadence
-```
+ ```
+ ./run.sh -t cadence -p lec
+ ```
 
-to use one of the tools. synopsys is used by default if no tool is specified,.
+ From a bash  shell to use SEC, please execute:
+ ```
+ ./run.sh -t siemens -p sec
+ ```
 
-Use `sh ./les.sh {synopsys, cadence}` if you run it from a tcsh shell.
+ By default `cv32e40p_core` is used as a top module, if you want to use
+ another one set the `TOP_MODULE` environment variable.
 
-The script clones the `cv32e40p_v1.0.0` tag of the core as a golden reference, and uses the current repository's `rtl` as revised version.
+ The script clones the `cv32e40p_v1.0.0` tag of the core as a golden reference,
+ and uses the current repository's `rtl` as revised version.
 
-If you want to use another golden reference rtl, Set the `GOLDEN_RTL` enviromental variable to the new rtl before calling the `lec.sh` script.
+ If you want to use another golden reference RTL, set the `GOLDEN_RTL`
+ environmental variable to the new RTL before calling the `run.sh` script.
 
-```
-export GOLDEN_RTL=YOUR_GOLDEN_CORE_RTL_PATH
-```
-or 
+ ```
+ export GOLDEN_RTL=YOUR_GOLDEN_CORE_RTL_PATH
+ ```
+ or
 
-```
-setenv GOLDEN_RTL  YOUR_GOLDEN_CORE_RTL_PATH
-```
-If the script succeeds, it returns 0, otherwise -1.
+ ```
+ setenv GOLDEN_RTL  YOUR_GOLDEN_CORE_RTL_PATH
+ ```
 
-The `check_lec.tcl` scripts in the tool specific folders are executed on the tools to perform `RTL to RTL` logic equivalence checking.

scripts/slec/cadence/lec.tcl

@@ -12,6 +12,7 @@
 // See the License for the specific language governing permissions and
 // limitations under the License.
 set summary_log $::env(summary_log)
+set top_module  $::env(top_module)
 
 read_design -SV -replace -noelaborate -golden -File ./golden.src
 
@@ -21,7 +22,7 @@ read_design -SV -replace -noelaborate -revised -File ./revised.src
 
 elaborate_design -revised
 
-report_design_data > ./reports/report_design.log
+report_design_data
 
 add_ignored_outputs apu_req_o -Both
 add_ignored_outputs apu_operands_o* -Both
@@ -30,10 +31,10 @@ add_ignored_outputs apu_flags_o* -Both
 
 write_hier_compare_dofile hier_compare_r2r.do -constraint -replace
 
-run_hier_compare hier_compare_r2r.do -ROOT_module cv32e40p_core cv32e40p_core
+run_hier_compare hier_compare_r2r.do -ROOT_module $top_module $top_module
 
-report_hier_compare_result -all -usage > $sumary_log
-report_verification -verbose -hier >> $sumary_log
-report_hier_compare_result -NONEQuivalent -usage > $sumary_log.noneq.rpt
+report_hier_compare_result -all -usage > $summary_log
+report_verification -verbose -hier >> $summary_log
+report_hier_compare_result -NONEQuivalent -usage > $summary_log.noneq.rpt
 
 exit 0

scripts/slec/cadence/sec.tcl

@@ -0,0 +1,40 @@
+# Copyright 2021 OpenHW Group
+#
+# Licensed under the Solderpad Hardware Licence, 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
+#
+#     https://solderpad.org/licenses/
+#
+# 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.
+set summary_log $::env(summary_log)
+set top_module  $::env(top_module)
+
+check_sec -setup -spec_top $top_module -imp_top $top_module \
+        -spec_analyze  "-sv -f ./golden.src" \
+        -imp_analyze "-sv -f ./revised.src"\
+        -auto_map_reset_x_values
+
+
+clock clk_i
+reset ~rst_ni
+
+check_sec -map -auto
+
+if {"$top_module" == "cv32e40p_core"} {
+    check_sec -waive -waive_signals ex_stage_i.alu_i.ff_one_i.sel_nodes
+    check_sec -waive -waive_signals cv32e40p_core_imp.ex_stage_i.alu_i.ff_one_i.sel_nodes
+
+    check_sec -waive -waive_signals ex_stage_i.alu_i.ff_one_i.index_nodes
+    check_sec -waive -waive_signals cv32e40p_core_imp.ex_stage_i.alu_i.ff_one_i.index_nodes
+}
+
+check_sec -prove
+
+check_sec -signoff -get_valid_status -summary -file $summary_log
+
+exit 0