Logical Equivalence Checking with Yosys EQY (#287)

* [rtl] Changed the default number of performance counters from 0 to 10 (#214)

* Implementation of sequential equivalence checking option using Yosys EQY.

* [sec] Automatic removal of new IO when performing SEC against (current) golden design with Yosys EQY

Author: cairo-caplan

.gitignore

@@ -35,3 +35,9 @@ 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
+/scripts/sec/ref_design

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,20 @@ 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 $(($(nproc)/2)) -d ${report_dir} &> ${report_dir}/output.yosys.log
+    rm yosys/golden_io.txt
+
+    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 +120,3 @@ else
     echo "SEC: The DESIGN IS NOT SEQUENTIAL EQUIVALENT"
     exit 1
 fi
-

scripts/sec/yosys/sec.eqy

@@ -0,0 +1,42 @@
+# 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.
+
+# To be ran as part of `./sec.sh -t yosys` from `scripts/sec`
+
+[gold]
+plugin -i slang
+read_slang --ignore-assertions -DGOLD --top cve2_top -f ./golden.src
+
+# Save the list of IO signals, in case the new revised version is different
+select -write yosys/golden_io.txt  o:* i:* 
+
+[gate]
+plugin -i slang
+read_slang --ignore-assertions -DGATE --top cve2_top -f ./revised.src
+
+
+# Delete eventual new IO signals from the revised design from analysis
+select -set golden_io -read yosys/golden_io.txt
+select -set revised_io o:* i:*
+select -set excl_sigs @revised_io @golden_io %d
+delete @excl_sigs
+
+[script]
+prep -top cve2_top
+memory_map
+
+[strategy sat]
+use sat
+depth 5
+