SEC/LEC scripts refactor

scripts/slec/README.md

@@ -1,51 +1,58 @@
-# 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.
+ 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`
+ environmental variable to the new RTL before calling the `run.sh` script.
 
-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.
-
-```
-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/run.sh

@@ -1,6 +1,6 @@
 #!/bin/bash
 
-# Copyright 2021 OpenHW Group
+# Copyright 2023 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.
@@ -14,85 +14,145 @@
 # See the License for the specific language governing permissions and
 # limitations under the License.
 
-if [[ -z "${GOLDEN_RTL}" ]]; then
-  echo "The env variable GOLDEN_RTL is empty."
-  echo "Cloning Golden Design...."
-  sh clone_reference.sh
-  export GOLDEN_RTL=$(pwd)/golden_reference_design/cv32e40p/rtl
-else
-  echo "Using ${GOLDEN_RTL} as reference design"
+REF_REPO=https://github.com/openhwgroup/cv32e40p.git
+REF_FOLDER=ref_design
+REF_BRANCH=master
+
+RTL_FOLDER=$(readlink -f ../..)
+
+FLIST=cv32e40p_manifest.flist
+TOP_MODULE=cv32e40p_core
+
+usage() {                                 # Function: Print a help message.
+  echo "Usage: $0 [ -t {cadence,synopsys,siemens} -p {sec,lec} ]" 1>&2
+}
+exit_abnormal() {                         # Function: Exit with error.
+  usage
+  exit 1
+}
+
+not_implemented() {
+    echo "$1 does not have yet $2 implemented"
+    exit 1
+}
+
+while getopts "t:p:" flag
+do
+    case "${flag}" in
+        t)
+        target_tool=${OPTARG}
+        ;;
+        p)
+        target_process=${OPTARG}
+        ;;
+        :)
+        exit_abnormal
+        ;;
+        *)
+        exit_abnormal
+        ;;
+        ?)
+        exit_abnormal
+        ;;
+    esac
+done
+
+if [ ! -d ./reports/ ]; then
+    mkdir -p ./reports/
+fi
+
+if [[ "${target_tool}" != "cadence" && "${target_tool}" != "synopsys" && "${target_tool}" != "siemens" ]]; then
+    exit_abnormal
+fi
+
+if [[ "${target_process}" != "sec" && "${target_process}" != "lec" ]]; then
+    exit_abnormal
 fi
 
-REVISED_RTL=$(pwd)/../../rtl
-
-
-var_golden_rtl=$(awk '{ if ($0 ~ "sv" && $0 !~ "incdir" && $0 !~ "wrapper" && $0 !~ "tracer") print $0 }' $GOLDEN_RTL/../cv32e40p_manifest.flist | awk -v rtlpath=$GOLDEN_RTL -F "/" '{$1=rtlpath} OFS="/"')
-
-var_revised_rtl=$(awk '{ if ($0 ~ "sv" && $0 !~ "incdir" && $0 !~ "wrapper" && $0 !~ "_top" && $0 !~ "tracer") print $0 }' $REVISED_RTL/../cv32e40p_manifest.flist | awk -v rtlpath=$REVISED_RTL -F "/" '{$1=rtlpath} OFS="/"')
-
-echo $var_golden_rtl > golden.src
-echo $var_revised_rtl > revised.src
-
-if [[ $# -gt 0 ]]; then 
-    if [[ $1 == "cadence" ]]; then
-        echo "Using Cadence Conformal"
-        if [[  -d ./cadence_conformal/reports ]]; then
-            rm -rf ./cadence_conformal/reports
-            mkdir ./cadence_conformal/reports
-        else
-            mkdir ./cadence_conformal/reports
-        fi
-    else
-        echo "Using Synopsys Formality"
-        if [[  -d ./synopsys_formality/reports ]]; then
-            rm -rf ./synopsys_formality/reports
-            mkdir ./synopsys_formality/reports
-        else
-            mkdir ./synopsys_formality/reports
-        fi
+if [[ -z "${GOLDEN_RTL}" ]]; then
+    echo "The env variable GOLDEN_RTL is empty."
+    if [ ! -d "./${REF_FOLDER}" ]; then
+        echo "Cloning Golden Design...."
+        git clone $REF_REPO --single-branch -b $REF_BRANCH $REF_FOLDER;
+        git -C ${REF_FOLDER} checkout $REF_COMMIT
     fi
+    export GOLDEN_RTL=$(pwd)/${REF_FOLDER}/rtl
 else
-    echo "No tool specified...."
-    echo "Using Synopsys Formality"
-    if [[  -d ./synopsys_formality/reports ]]; then
-        rm -rf ./synopsys_formality/reports
-        mkdir ./synopsys_formality/reports
-    else
-        mkdir ./synopsys_formality/reports
-    fi
+    echo "${target_process^^}: Using ${GOLDEN_RTL} as reference design"
+fi
+
+REVISED_DIR=$RTL_FOLDER
+REVISED_FLIST=$(pwd)/revised.src
+
+GOLDEN_DIR=$(readlink -f ./${REF_FOLDER}/)
+GOLDEN_FLIST=$(pwd)/golden.src
+
+var_golden_rtl=$(awk '{ if ($0 ~ "{DESIGN_RTL_DIR}" && $0 !~ "#" && $0 !~ "tracer" && $0 !~ "wrapper") print $0 }' ${GOLDEN_DIR}/$FLIST | sed 's|${DESIGN_RTL_DIR}|'"${GOLDEN_DIR}"'/rtl/|')
+
+var_revised_rtl=$(awk '{ if ($0 ~ "{DESIGN_RTL_DIR}" && $0 !~ "#" && $0 !~ "tracer" && $0 !~ "wrapper") print $0 }' ${REVISED_DIR}/$FLIST | sed 's|${DESIGN_RTL_DIR}|'"${REVISED_DIR}"'/rtl/|')
+
+echo "Generating GOLDEN flist in path: ${GOLDEN_FLIST}"
+echo $var_golden_rtl > ${GOLDEN_FLIST}
+echo "Generating REVISED flist in path: ${REVISED_FLIST}"
+echo $var_revised_rtl > ${REVISED_FLIST}
+
+export report_dir=$(readlink -f $(dirname "${BASH_SOURCE[0]}"))/reports/$(date +%Y-%m-%d)/
+
+if [[ -d ${report_dir} ]]; then
+    rm -rf ${report_dir}
 fi
+mkdir -p ${report_dir}
+
+export tcl_script=$(readlink -f $(dirname "${BASH_SOURCE[0]}"))/${target_tool}/${target_process}.tcl
+export output_log=${report_dir}/output.${target_tool}.log
+export summary_log=${report_dir}/summary.${target_tool}.log
 
-if [[ $1 == "cadence" ]]; then
-    echo "Running Cadence Conformal"
-    cd ./cadence_conformal
-    lec -Dofile check_lec.tcl -TclMode -LOGfile cv32e40p_lec_log.log -NoGUI -xl
-    if [ -f "./reports/result.rpt" ]; then
-        NonLec=$(awk '{ if ($0 ~ "Hierarchical compare : Equivalent") print "0"}' ./reports/result.rpt)
-    else
-        echo "FATAL: could not find reports..."
-        NonLec="-1"
+export expected_grep_exit_code=1
+
+if [[ "${target_tool}" == "cadence" ]]; then
+
+    if [[ "${target_process}" == "lec" ]]; then
+        lec -Dofile ${tcl_script} -TclMode -NoGUI -xl | tee ${output_log}
+        regex_string="Hierarchical compare : Equivalent"
+    elif [[ "${target_process}" == "sec" ]]; then
+        jg -sec -proj ${report_dir} -batch -tcl ${tcl_script} -define report_dir ${report_dir} | tee ${output_log}
+        regex_string="Overall SEC status[ ]+- Complete"
     fi
-    cd ../
-else
-    echo "Running Synopsys Formality"
-    cd ./synopsys_formality
-    fm_shell -f check_lec.tcl |& tee cv32e40p_lec_log.log
-    if [ -f "./reports/verify.rpt" ]; then
-        NonLec=$(awk '{ if ($0 ~ "Verification SUCCEEDED") print "0"}' ./reports/verify.rpt)
-    else
-        echo "FATAL: could not find reports..."
-        NonLec="-1"
+
+elif [[ "${target_tool}" == "synopsys" ]]; then
+
+    if [[ "${target_process}" == "lec" ]]; then
+        fm_shell -work_path $report_dir/work/ -f ${tcl_script} | tee ${output_log}
+        regex_string="Verification SUCCEEDED"
+    elif [[ "${target_process}" == "sec" ]]; then
+        not_implemented ${target_tool} ${target_process}
     fi
-    cd ../
+
+elif [[ "${target_tool}" == "siemens" ]]; then
+
+    if [[ "${target_process}" == "lec" ]]; then
+        not_implemented ${target_tool} ${target_process}
+    elif [[ "${target_process}" == "sec" ]]; then
+        make -C siemens/ run_sec_vl SPEC_FLIST=${GOLDEN_FLIST} IMPL_FLIST=${REVISED_FLIST} TOP_MODULE=${TOP_MODULE} SUMMARY_LOG=${summary_log} | tee ${output_log}
+        regex_string="^Fired"
+        expected_grep_exit_code=0
+    fi
+
 fi
 
-if [[ $NonLec == "0" ]]; then
-    echo "The DESIGN IS LOGICALLY EQUIVALENT"
+if [[ ! -f ${output_log} || ! -f ${summary_log} ]]; then
+    echo "Something went wrong during the process"
+    exit 1
+fi
+
+grep -Eq "${regex_string}" ${summary_log}; grep_exit_code=$?
+
+if [[ ${grep_exit_code} != ${expected_grep_exit_code} ]]; then
+    echo "${target_process^^}: The DESIGN IS EQUIVALENT"
 else
-    NonLec="-1"
-    echo "The DESIGN IS NOT LOGICALLY EQUIVALENT"
+    echo "${target_process^^}: The DESIGN IS NOT EQUIVALENT"
 fi
 
-echo "$0 returns $NonLec"
 
-exit $NonLec
+exit ${exit_code}
+

scripts/slec/siemens/Makefile

@@ -0,0 +1,41 @@
+##############################################################################
+#             Copyright 2006-ntor Graphics Corporation
+#
+#             THIS SOFTWARE AND RELATED DOCUMENTATION
+#            ARE PROPRIETARY AND CONFIDENTIAL TO SIEMENS.
+#                        © 2023 Siemens
+
+INSTALL := $(shell qverify -install_path)
+VLIB = $(INSTALL)/modeltech/linux_x86_64/vlib
+VMAP = $(INSTALL)/modeltech/linux_x86_64/vmap
+VLOG = $(INSTALL)/modeltech/linux_x86_64/vlog
+VCOM = $(INSTALL)/modeltech/linux_x86_64/vcom
+
+run_sec_vl: clean run_sec
+
+run_sec:
+	$(VLIB) work_ip_orig
+	$(VLIB) work_ip_mod
+	$(VMAP) work_spec work_ip_orig
+	$(VMAP) work_impl work_ip_mod
+	$(VLOG) -sv -f $(SPEC_FLIST) -work work_spec
+	$(VLOG) -sv -f $(IMPL_FLIST) -work work_impl
+
+	qverify -c -od log -do " \
+	onerror { exit 1 }; \
+	slec configure -spec -d $(TOP_MODULE) -work work_spec; \
+	slec configure -impl -d $(TOP_MODULE) -work work_impl; \
+	slec compile; \
+	slec verify -timeout 10m; \
+	exit"
+	@cp log/slec_verify.log $(SUMMARY_LOG)
+
+
+debug:
+	qverify log/slec.db
+
+clean:
+	qverify_clean
+	rm -rf log* work* *.rpt modelsim.ini .visualizer visualizer*
+
+

scripts/slec/synopsys/lec.tcl

@@ -1,9 +1,10 @@
-set synopsys_auto_setup true 
+set synopsys_auto_setup true
+set summary_log $::env(summary_log)
 
-read_sverilog -container r -libname WORK -12 -f ../golden.src
-set_top r:/WORK/cv32e40p_core 
+read_sverilog -container r -libname WORK -12 -f golden.src
+set_top r:/WORK/cv32e40p_core
 
-read_sverilog -container i -libname WORK -12 -f ../revised.src
+read_sverilog -container i -libname WORK -12 -f revised.src
 set_top i:/WORK/cv32e40p_core
 
 match > ./reports/match.rpt
@@ -13,10 +14,10 @@ set_dont_verify_point -type port  i:WORK/cv32e40p_core/apu_operands_o*
 set_dont_verify_point -type port  i:WORK/cv32e40p_core/apu_op_o*
 set_dont_verify_point -type port  i:WORK/cv32e40p_core/apu_flags_o*
 
-verify > ./reports/verify.rpt
+verify > $summary_log
 
-report_aborted_points > ./reports/aborted_points.rpt
-report_failing_points > ./reports/failing_points.rpt
-analyze_points -failing > ./reports/analyze.rpt
+report_aborted_points > $summary_log.aborted_points.rpt
+report_failing_points > $summary_log.failing_points.rpt
+analyze_points -failing >> $summary_log
 
 exit