From 3e9a88551f33ad9de931289f64362f4f734def50 Mon Sep 17 00:00:00 2001 From: Mario Date: Tue, 2 Jan 2024 09:39:56 +0000 Subject: [PATCH] SEC/LEC scripts refactor --- scripts/lec/README.md | 51 ------ scripts/lec/clone_reference.sh | 22 --- scripts/lec/lec.sh | 98 ----------- scripts/lec/synopsys_formality/check_lec.tcl | 22 --- scripts/slec/README.md | 58 +++++++ .../check_lec.tcl => slec/cadence/lec.tcl} | 11 +- scripts/slec/run.sh | 154 ++++++++++++++++++ scripts/slec/siemens/Makefile | 41 +++++ scripts/slec/synopsys/lec.tcl | 23 +++ 9 files changed, 282 insertions(+), 198 deletions(-) delete mode 100644 scripts/lec/README.md delete mode 100755 scripts/lec/clone_reference.sh delete mode 100755 scripts/lec/lec.sh delete mode 100644 scripts/lec/synopsys_formality/check_lec.tcl create mode 100644 scripts/slec/README.md rename scripts/{lec/cadence_conformal/check_lec.tcl => slec/cadence/lec.tcl} (74%) create mode 100755 scripts/slec/run.sh create mode 100755 scripts/slec/siemens/Makefile create mode 100644 scripts/slec/synopsys/lec.tcl diff --git a/scripts/lec/README.md b/scripts/lec/README.md deleted file mode 100644 index 51befbc2f..000000000 --- a/scripts/lec/README.md +++ /dev/null @@ -1,51 +0,0 @@ -# Logic Equivalence Checking (LEC) - -This folder contains a LEC script that runs on both -Synopsys Formality and Cadence Design Systems Conformal. - -This script allows to catch non-logical equivalent changes on the RTL which are forbidden -on the verified paramter set. - -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. - -### Running the script - -From a bash shell, please execute: - -``` -./lec.sh synopsys -``` - or - -``` -./lec.sh cadence -``` - -to use one of the tools. synopsys is used by default if no tool is specified,. - -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. - -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 - -``` -setenv GOLDEN_RTL YOUR_GOLDEN_CORE_RTL_PATH -``` -If the script succeeds, it returns 0, otherwise -1. - -The `check_lec.tcl` scripts in the tool specific folders are executed on the tools to perform `RTL to RTL` logic equivalence checking. diff --git a/scripts/lec/clone_reference.sh b/scripts/lec/clone_reference.sh deleted file mode 100755 index 76a7510eb..000000000 --- a/scripts/lec/clone_reference.sh +++ /dev/null @@ -1,22 +0,0 @@ -#!/bin/bash - -# 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. - -if [ ! -d "./golden_reference_design" ]; then - mkdir -p ./golden_reference_design - cd ./golden_reference_design - git clone https://github.com/openhwgroup/cv32e40p.git --branch cv32e40p_v1.0.0 - cd ../ -fi diff --git a/scripts/lec/lec.sh b/scripts/lec/lec.sh deleted file mode 100755 index 5e9f7387f..000000000 --- a/scripts/lec/lec.sh +++ /dev/null @@ -1,98 +0,0 @@ -#!/bin/bash - -# 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. - -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" -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 - fi -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 -fi - -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" - 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" - fi - cd ../ -fi - -if [[ $NonLec == "0" ]]; then - echo "The DESIGN IS LOGICALLY EQUIVALENT" -else - NonLec="-1" - echo "The DESIGN IS NOT LOGICALLY EQUIVALENT" -fi - -echo "$0 returns $NonLec" - -exit $NonLec diff --git a/scripts/lec/synopsys_formality/check_lec.tcl b/scripts/lec/synopsys_formality/check_lec.tcl deleted file mode 100644 index 612aba257..000000000 --- a/scripts/lec/synopsys_formality/check_lec.tcl +++ /dev/null @@ -1,22 +0,0 @@ -set synopsys_auto_setup true - -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 -set_top i:/WORK/cv32e40p_core - -match > ./reports/match.rpt - -set_dont_verify_point -type port i:WORK/cv32e40p_core/apu_req_o -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 - -report_aborted_points > ./reports/aborted_points.rpt -report_failing_points > ./reports/failing_points.rpt -analyze_points -failing > ./reports/analyze.rpt - -exit diff --git a/scripts/slec/README.md b/scripts/slec/README.md new file mode 100644 index 000000000..42538458d --- /dev/null +++ b/scripts/slec/README.md @@ -0,0 +1,58 @@ +# 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 + ``` + + 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 + ``` + diff --git a/scripts/lec/cadence_conformal/check_lec.tcl b/scripts/slec/cadence/lec.tcl similarity index 74% rename from scripts/lec/cadence_conformal/check_lec.tcl rename to scripts/slec/cadence/lec.tcl index d8b918a36..7d527ac4b 100644 --- a/scripts/lec/cadence_conformal/check_lec.tcl +++ b/scripts/slec/cadence/lec.tcl @@ -11,12 +11,13 @@ // 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) -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 @@ -31,8 +32,8 @@ write_hier_compare_dofile hier_compare_r2r.do -constraint -replace run_hier_compare hier_compare_r2r.do -ROOT_module cv32e40p_core cv32e40p_core -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 > $sumary_log +report_verification -verbose -hier >> $sumary_log +report_hier_compare_result -NONEQuivalent -usage > $sumary_log.noneq.rpt exit 0 diff --git a/scripts/slec/run.sh b/scripts/slec/run.sh new file mode 100755 index 000000000..98bbda526 --- /dev/null +++ b/scripts/slec/run.sh @@ -0,0 +1,154 @@ +#!/bin/bash + +# 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. +# 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. + +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 + +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 "${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 + +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 + +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 + +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 [[ ! -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=$? + +[[ ${grep_exit_code} == ${expected_grep_exit_code} ]] && export EQ_STR="NOT" + +echo "${target_process^^}: The DESIGN IS ${EQ_STR} EQUIVALENT" +exit ${exit_code} + diff --git a/scripts/slec/siemens/Makefile b/scripts/slec/siemens/Makefile new file mode 100755 index 000000000..4e375340e --- /dev/null +++ b/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* + + diff --git a/scripts/slec/synopsys/lec.tcl b/scripts/slec/synopsys/lec.tcl new file mode 100644 index 000000000..0505138c1 --- /dev/null +++ b/scripts/slec/synopsys/lec.tcl @@ -0,0 +1,23 @@ +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 i -libname WORK -12 -f revised.src +set_top i:/WORK/cv32e40p_core + +match > ./reports/match.rpt + +set_dont_verify_point -type port i:WORK/cv32e40p_core/apu_req_o +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 > $summary_log + +report_aborted_points > $summary_log.aborted_points.rpt +report_failing_points > $summary_log.failing_points.rpt +analyze_points -failing >> $summary_log + +exit