diff --git a/scripts/slec/README.md b/scripts/slec/README.md index 51befbc2f..ff5311322 100644 --- a/scripts/slec/README.md +++ b/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. diff --git a/scripts/slec/cadence/lec.tcl b/scripts/slec/cadence/lec.tcl index 7d527ac4b..3cc8bea7b 100644 --- a/scripts/slec/cadence/lec.tcl +++ b/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 diff --git a/scripts/slec/cadence/sec.tcl b/scripts/slec/cadence/sec.tcl new file mode 100644 index 000000000..7107eb9e3 --- /dev/null +++ b/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 diff --git a/scripts/slec/run.sh b/scripts/slec/run.sh index 5e9f7387f..5ecd62f88 100755 --- a/scripts/slec/run.sh +++ b/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,159 @@ # 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" +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 +} + +print_log() { + echo "[LOG] $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 [[ "${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 "${REF_REPO}" ]; then + print_log "Empty REF_REPO env variable" + REF_REPO=https://github.com/openhwgroup/cv32e40p.git + REF_FOLDER=ref_design + REF_BRANCH=master + print_log " * Setting REF_REPO ${REF_REPO}" + print_log " * Setting REF_FOLDER ${REF_FOLDER}" + print_log " * Setting REF_BRANCH ${REF_BRANCH}" 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 +RTL_FOLDER=$(readlink -f ../..) + +FLIST=cv32e40p_manifest.flist + +if [[ -z "${TOP_MODULE}" ]]; then + print_log "Empty TOP_MODULE env variable" + TOP_MODULE=cv32e40p_core + print_log " * Setting TOP_MODULE ${TOP_MODULE}" +fi + +if [ ! -d ./reports/ ]; then + mkdir -p ./reports/ +fi + +if [[ -z "${GOLDEN_RTL}" ]]; then + print_log "The env variable GOLDEN_RTL is empty." + if [ ! -d "./${REF_FOLDER}" ]; then + print_log " * 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 + print_log "${target_process^^}: Using ${GOLDEN_RTL} as reference design" 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" +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/|') + +print_log "Generating GOLDEN flist in path: ${GOLDEN_FLIST}" +echo $var_golden_rtl > ${GOLDEN_FLIST} +print_log "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}-${target_process}.log +export summary_log=${report_dir}/summary.${target_tool}-${target_process}.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 - 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 + +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 - cd ../ + fi -if [[ $NonLec == "0" ]]; then - echo "The DESIGN IS LOGICALLY EQUIVALENT" -else - NonLec="-1" - echo "The DESIGN IS NOT LOGICALLY EQUIVALENT" +if [[ ! -f ${output_log} || ! -f ${summary_log} ]]; then + print_log "Something went wrong during the process" + exit 1 fi -echo "$0 returns $NonLec" +grep -Eq "${regex_string}" ${summary_log}; grep_exit_code=$? + +if [[ ${grep_exit_code} != ${expected_grep_exit_code} ]]; then + print_log "${target_process^^}: THE DESIGN IS EQUIVALENT" +else + print_log "${target_process^^}: THE DESIGN IS NOT EQUIVALENT" +fi -exit $NonLec +exit ${exit_code} diff --git a/scripts/slec/siemens/Makefile b/scripts/slec/siemens/Makefile new file mode 100755 index 000000000..15e281f93 --- /dev/null +++ b/scripts/slec/siemens/Makefile @@ -0,0 +1,41 @@ +############################################################################## +# Copyright 2006-Mentor 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 index 612aba257..1f6b41936 100644 --- a/scripts/slec/synopsys/lec.tcl +++ b/scripts/slec/synopsys/lec.tcl @@ -1,22 +1,26 @@ -set synopsys_auto_setup true +set synopsys_auto_setup true +set summary_log $::env(summary_log) +set top_module $::env(top_module) -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/$top_module -read_sverilog -container i -libname WORK -12 -f ../revised.src -set_top i:/WORK/cv32e40p_core +read_sverilog -container i -libname WORK -12 -f revised.src +set_top i:/WORK/$top_module 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* +if {"$top_module" == "cv32e40p_core"} { + 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 +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