diff --git a/.gitignore b/.gitignore index c3a370c9..eef630f2 100644 --- a/.gitignore +++ b/.gitignore @@ -34,3 +34,8 @@ modelsim.ini # This is generated by Xcelium when running DV simulations, even with WAVE=0 /dv/uvm/core_cve2/waves.shm + +# This is generated by the sequential equivalent checking +/scripts/sec/golden.src +/scripts/sec/revised.src +/scripts/sec/reports diff --git a/scripts/sec/sec.sh b/scripts/sec/sec.sh index 438189c8..b392a6e3 100755 --- a/scripts/sec/sec.sh +++ b/scripts/sec/sec.sh @@ -15,7 +15,7 @@ # limitations under the License. usage() { # Function: Print a help message. - echo "Usage: $0 [ -t {cadence,synopsys,mentor} ]" 1>&2 + echo "Usage: $0 [ -t {cadence,mentor,synopsys,yosys} ]" 1>&2 } exit_abnormal() { # Function: Exit with error. usage @@ -44,7 +44,8 @@ if [ ! -d ./reports/ ]; then mkdir -p ./reports/ fi -if [[ "${target_tool}" != "cadence" && "${target_tool}" != "synopsys" && "${target_tool}" != "mentor" ]]; then +if [[ "${target_tool}" != "cadence" && "${target_tool}" != "synopsys" + && "${target_tool}" != "mentor" && "${target_tool}" != "yosys" ]]; then exit_abnormal fi @@ -80,7 +81,7 @@ mkdir -p ${report_dir} if [[ "${target_tool}" == "cadence" ]]; then tcl_script=$(readlink -f $(dirname "${BASH_SOURCE[0]}"))/cadence/sec.tcl - jg -sec -proj ${report_dir} -batch -tcl ${tcl_script} -define report_dir ${report_dir} &> ${report_dir}/output.candence.log + jg -sec -proj ${report_dir} -batch -tcl ${tcl_script} -define report_dir ${report_dir} &> ${report_dir}/output.cadence.log if [ ! -f ${report_dir}/summary.cadence.log ]; then echo "Something went wrong during the process" @@ -96,6 +97,19 @@ elif [[ "${target_tool}" == "synopsys" ]]; then elif [[ "${target_tool}" == "mentor" ]]; then echo "Mentor tool is not implemented yet" exit 1 + +elif [[ "${target_tool}" == "yosys" ]]; then + echo "Using Yosys EQY" + eqy -f yosys/sec.eqy -j 4 -d ${report_dir} &> ${report_dir}/output.yosys.log + + if [ -f "${report_dir}/PASS" ]; then + RESULT=0 + elif [ -f "${report_dir}/FAIL" ]; then + RESULT=1 + else + echo "Failed to run Yosys EQY" + exit 1 + fi fi if [[ $RESULT == 0 ]]; then @@ -105,4 +119,3 @@ else echo "SEC: The DESIGN IS NOT SEQUENTIAL EQUIVALENT" exit 1 fi - diff --git a/scripts/sec/yosys/sec.eqy b/scripts/sec/yosys/sec.eqy new file mode 100644 index 00000000..fdcc483b --- /dev/null +++ b/scripts/sec/yosys/sec.eqy @@ -0,0 +1,31 @@ +# Copyright 2025 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. + +[gold] +plugin -i slang +read_slang --ignore-assertions -DGOLD --top cve2_top -f ./golden.src + +[gate] +plugin -i slang +read_slang --ignore-assertions -DGATE --top cve2_top -G Xinterface=0 -f ./revised.src +delete cve2_top/x_* + +[script] +prep -top cve2_top +memory_map + +[strategy sat] +use sat +depth 5 +