Merge pull request openhwgroup#1014 from pascalgouedo/dev_dd_pgo_risc…

…v_formal

Up-to-date files for RISC-V ISA Formal Verification.

scripts/riscv_isa_formal/Makefile

@@ -1,4 +1,4 @@
-commonPath=../../common
+commonPath=../../verif
 PREPARE?=0
 RTL?=../../cv32e40p/
 GUI?=0

scripts/riscv_isa_formal/README.md

@@ -30,7 +30,7 @@ RISC-V ISA Formal Verification methodology has been used with Siemens Questa Pro
 - Makefile
 - launch_command_example
 
-### common
+### verif
 Contains all files to create assertions and to launch different tool apps on different configurations and using different modes.
 
 > [!CAUTION]
@@ -39,6 +39,9 @@ Contains all files to create assertions and to launch different tool apps on dif
 
 ## How to launch a run
 
+> [!CAUTION]
+> Siemens Questa Processor 2024.2 and above must be used.
+
 - Locally clone cv32e40p github repository or make a symbolic link to an existing repo.
 - launch following command:<br>
   make GUI=1 APP=PRC CONF=XP MODE=DEF NAME=v1_8_0 VERBOSE=1 PREPARE=1 all >&! run_gui-PRC-cfg_XP-mode_DEF-v1_8_0.log

scripts/riscv_isa_formal/launch_command example → scripts/riscv_isa_formal/launch_command_example

@@ -19,7 +19,7 @@ set mode=DEF ; set mode_cmd="MODE=${mode}"
 set mode=DPM ; set mode_cmd="MODE=${mode}"
 set mode=DPF ; set mode_cmd="MODE=${mode}"
 
-# Prepare the working directory (common files and design copy) or reuse existing one (no copy)
+# Prepare the working directory (verif files and design copy) or reuse existing one (no copy)
 set prepare=""
 set prepare="PREPARE=1"
 

scripts/riscv_isa_formal/common/constraints.sv → scripts/riscv_isa_formal/verif/constraints.sv

@@ -112,7 +112,7 @@ endfunction
 `ifdef RESTRICT_REGS
 	// Restrict instruction decoding & register file verification to a subset of registers
 	restrict_regs_c: assume property (disable iff (~rst_n)
-	restrict_regs(execute.dec)
+	restrict_regs(my_dec)
 	`ifndef COMPLETENESS
 		`ifndef RESTRICT_REGISTER_INDEX
 //			&& (reg_idx<4 || (MISA.C|Zca) && reg_idx inside {5'd8,5'd9})

scripts/riscv_isa_formal/verif/cv32e40p/info.txt

@@ -0,0 +1,17 @@
+# Copyright 2024 Siemens
+# SPDX-License-Identifier: Apache-2.0 WITH SHL-2.1
+# 
+# Licensed under the Solderpad Hardware License v 2.1 (the "License");
+# you may not use this file except in compliance with the License, or,
+# at your option, the Apache License version 2.0.
+# You may obtain a copy of the License at
+# 
+# https://solderpad.org/licenses/SHL-2.1/
+# 
+# Unless required by applicable law or agreed to in writing, any work
+# 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.
+
+github clone from https://github.com/openhwgroup/cv32e40p.git on the 24th of Jun 2024, tag cv32e40p_v1.8.0 is selected.