Refactor of LEC/SEC scripts

scripts/slec/README.md

@@ -0,0 +1,61 @@
+# Sequential Logic Equivalence Checking (SLEC)
+
+This folder contains a SLEC script that runs:
+
+- 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` ,
+Cadence Design Systems Conformal `20.20` and Siemens SLEC App `2023.4`.
+
+### Running the script
+
+From a bash shell using LEC, please execute:
+
+```
+./run.sh -t synopsys -p lec
+```
+ or
+
+ ```
+ ./run.sh -t cadence -p lec
+ ```
+
+ From a bash  shell to use SEC, please execute:
+ ```
+ ./run.sh -t siemens -p sec
+ ```
+
+ 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.
+
+ 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
+
+ ```
+ setenv GOLDEN_RTL  YOUR_GOLDEN_CORE_RTL_PATH
+ ```
+

scripts/lec/cadence_conformal/check_lec.tcl → scripts/slec/cadence/lec.tcl

@@ -11,16 +11,18 @@
 // 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)
 
-read_design -SV -replace -noelaborate -golden -File ../golden.src
+read_design -SV -replace -noelaborate -golden -File ./golden.src
 
 elaborate_design -golden
 
-read_design -SV -replace -noelaborate -revised -File ../revised.src
+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
@@ -29,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 > ./reports/result.rpt
-report_hier_compare_result -NONEQuivalent -usage > ./reports/result_noneq.rpt
-report_verification -verbose -hier > ./reports/result_verfication.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