RISC-V ISA Formal Verification setup and script files for Siemens Questa Processor tool

scripts/riscv_isa_formal/Makefile

@@ -0,0 +1,59 @@
+commonPath=../../common
+PREPARE?=0
+RTL?=../../cv32e40p/
+GUI?=0
+NAME?=noname
+
+ifeq ($(APP),)
+  $(error APP is empty)
+endif
+ifeq ($(CONF),)
+  $(error CONF is empty)
+endif
+ifeq ($(MODE),)
+  $(error MODE is empty)
+endif
+
+$(info APP=$(APP))
+$(info CONF=$(CONF))
+$(info MODE=$(MODE))
+
+ifeq ($(GUI), 1)
+  flag="-i"
+else
+  flag=
+endif
+
+dirname=$(NAME)
+
+ifeq ($(PREPARE), 1)
+  script_name=ones_prepare_run
+else
+  script_name=ones_run
+endif
+
+define ones_prepare_run
+	@echo "===================================================="
+	@echo "Preparing working area $(dirname)"
+	@echo "===================================================="
+	\mkdir -p cfgs/$(dirname)/logs
+	\cd cfgs/$(dirname) && \cp -pf $(commonPath)/{other_bindings.sv,core_checker.sv,io.sv,setup.tcl,setup_mv.tcl,*.json,constraints.sv,t.sh,basics.tcl.obf} . && \cp -prfL $(commonPath)/vips . && \cp -prfL $(RTL) .
+	@echo "===================================================="
+	@echo "Running mode $(MODE) on configuration $(CONF) in $(dirname)"
+	@echo "===================================================="
+	\cd cfgs/$(dirname) && onespin -Q -l logs/$(APP)-cfg_$(CONF)-mode_$(MODE).log $(flag) setup.tcl $(CONF) $(MODE) $(APP)
+endef
+
+define ones_run
+	@echo "===================================================="
+	@echo "Running mode $(MODE) on configuration $(CONF) in $(dirname)"
+	@echo "===================================================="
+	\cd cfgs/$(dirname) && onespin -Q -l logs/$(APP)-cfg_$(CONF)-mode_$(MODE).log $(flag) setup.tcl $(CONF) $(MODE) $(APP)
+endef
+
+all:
+	$(call $(script_name))
+
+clean: 
+	rm -rf cfgs/$(dirname)
+

scripts/riscv_isa_formal/README.md

@@ -0,0 +1,50 @@
+# RISC-V ISA Formal Verification
+
+RISC-V ISA Formal Verification methodology has been used with Siemens Questa Processor tool and its RISC-V ISA Processor Verification app.
+
+## Configurations
+
+  | Top Parameters     | XP     | XPF0     | XPF1     | XPF2     | XPZF0     | XPZF1     | XPZF2     |
+  | :----------------- | :----: |:-------: | :------: | :------: | :-------: | :-------: | :-------: |
+  | COREV_PULP         | 1      | 1        | 1        | 1        | 1         | 1         | 1         |
+  | COREV_CLUSTER      | 0      | 0        | 0        | 0        | 0         | 0         | 0         |
+  | FPU                | 0      | 1        | 1        | 1        | 1         | 1         | 1         |
+  | ZFINX              | 0      | 0        | 0        | 0        | 1         | 1         | 1         |
+  | FPU_ADDMUL_LAT     | 0      | 0        | 1        | 2        | 0         | 1         | 2         |
+  | FPU_OTHERS_LAT     | 0      | 0        | 1        | 2        | 0         | 1         | 2         |
+
+## Tool apps
+
+- PRC : Property Checking
+- QTF : Quantify
+- VCI : Verification Coverage Integration
+
+## Prove modes
+
+- DEF : Control path verification of all instructions and datapath verification of all instructions except multiplication, division or floating point ones
+- DPM : Data path verification of multiplication/ division instructions
+- DPF : Data path verification of floating-point instructions
+
+## Directory Structure of this Repo
+
+- Makefile
+- launch_command_example
+
+### common
+Contains all files to create assertions and to launch different tool apps on different configurations and using different modes.
+
+> [!CAUTION]
+> core_checker.sv contains proprietary information and is only available to Siemens Questa Processor customers.
+> Once Questa Processor licenses have been purchased, this file can be requested to Siemens support center.
+
+## How to launch a run
+
+- 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
+- or use launch_command_example to launch different runs in parallel.
+
+## Commands to launch assertion checks for each configuration
+
+- XP : PRC app with DEF and DPM modes
+- XPF[0,1,2] and XPZF[0,1,2] : PRC app with DEF, DPM and DPF modes

scripts/riscv_isa_formal/common/constraints.sv

@@ -0,0 +1,135 @@
+// 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.
+
+/*********************/
+// CONSTRAINTS
+/*********************/
+
+// MAIN CONSTRAINTS //
+
+const_addrs_c   : assume property (##1 $stable({boot_addr,`core.dm_halt_addr_i,`core.dm_exception_addr_i,`core.mtvec_addr_i,`core.hart_id_i}));
+const_dm_addr_c : assume property (`core.dm_halt_addr_i==32'h800 && `core.dm_exception_addr_i==32'h808); // **I** To meet app expectations
+
+`ifdef CFG_XP
+`ifdef CV_LOOP
+	// raising of hwloop illegal currently not modeled
+	no_hwloop_illegal_c      : assume property (!id_stage_i.controller_i.is_hwlp_illegal);
+
+    // hwloop must contain 3+ instructions
+	hwloop_min_size_c        : assume property (!(id_stage_i.gen_hwloop_regs.hwloop_regs_i.hwlp_counter_q[0]>0&&id_stage_i.gen_hwloop_regs.hwloop_regs_i.hwlp_end_q[0]-id_stage_i.gen_hwloop_regs.hwloop_regs_i.hwlp_start_q[0] inside {32'h0,32'h4,32'h8}) && !(id_stage_i.gen_hwloop_regs.hwloop_regs_i.hwlp_counter_q[1]>0&&id_stage_i.gen_hwloop_regs.hwloop_regs_i.hwlp_end_q[1]-id_stage_i.gen_hwloop_regs.hwloop_regs_i.hwlp_start_q[1] inside {32'h0,32'h4,32'h8}));
+
+	// hwloop must be word-aligned
+	hwloop_aligned_c         : assume property (id_stage_i.gen_hwloop_regs.hwloop_regs_i.hwlp_start_q[0][1:0]==0 && id_stage_i.gen_hwloop_regs.hwloop_regs_i.hwlp_end_q[0][1:0]==0 && id_stage_i.gen_hwloop_regs.hwloop_regs_i.hwlp_start_q[1][1:0]==0 && id_stage_i.gen_hwloop_regs.hwloop_regs_i.hwlp_end_q[1][1:0]==0);
+
+	// we must not create loop 0 in the middle of itself (setting count to non-zero at a PC location that would qualify as inside the loop). Also, setting up the registers and then jumping to a location inside loop 0 will likely not work
+	loop0_setup_c            : assume property (id_stage_i.gen_hwloop_regs.hwloop_regs_i.hwlp_counter_q[0]==0 ##1 id_stage_i.gen_hwloop_regs.hwloop_regs_i.hwlp_counter_q[0]!=0 |-> id_stage_i.gen_hwloop_regs.hwloop_regs_i.hwlp_start_q[0]==$past(pc_id)+32'd4);
+
+	// we must not create loop 1 in the middle of itself (setting count to non-zero at a PC location that would qualify as inside the loop). Also, setting up the registers and then jumping to a location inside loop 1 will likely not work
+	loop1_setup_c            : assume property (id_stage_i.gen_hwloop_regs.hwloop_regs_i.hwlp_counter_q[1]==0 ##1 id_stage_i.gen_hwloop_regs.hwloop_regs_i.hwlp_counter_q[1]!=0 |-> id_stage_i.gen_hwloop_regs.hwloop_regs_i.hwlp_start_q[1]==$past(pc_id)+32'd4);
+
+	// let's not wrap
+	lopp_no_wrap_c           : assume property (!(id_stage_i.gen_hwloop_regs.hwloop_regs_i.hwlp_counter_q[0]>0&&id_stage_i.gen_hwloop_regs.hwloop_regs_i.hwlp_end_q[0]<id_stage_i.gen_hwloop_regs.hwloop_regs_i.hwlp_start_q[0]) && !(id_stage_i.gen_hwloop_regs.hwloop_regs_i.hwlp_counter_q[1]>0&&id_stage_i.gen_hwloop_regs.hwloop_regs_i.hwlp_end_q[1]<id_stage_i.gen_hwloop_regs.hwloop_regs_i.hwlp_start_q[1]));
+
+	// do not modify loop 0 inside body 0
+	loop0_no_modify_c        : assume property (!(id_stage_i.gen_hwloop_regs.hwloop_regs_i.hwlp_counter_q[0]>0 && pc_id>=id_stage_i.gen_hwloop_regs.hwloop_regs_i.hwlp_start_q[0] && pc_id<id_stage_i.gen_hwloop_regs.hwloop_regs_i.hwlp_end_q[0] && (id_stage_i.controller_i.branch_in_id_dec || id_stage_i.controller_i.jump_in_dec || id_stage_i.hwlp_regid==0 && id_stage_i.hwlp_we)));
+
+	// do not modify loop 1 inside body 1
+	loop1_no_modify_c        : assume property (!(id_stage_i.gen_hwloop_regs.hwloop_regs_i.hwlp_counter_q[1]>0 && pc_id>=id_stage_i.gen_hwloop_regs.hwloop_regs_i.hwlp_start_q[1] && pc_id<id_stage_i.gen_hwloop_regs.hwloop_regs_i.hwlp_end_q[1] && (id_stage_i.controller_i.branch_in_id_dec || id_stage_i.controller_i.jump_in_dec || id_stage_i.hwlp_regid==1 && id_stage_i.hwlp_we)));
+
+	// do not setup a count of 1 (not always decrementing to 0 on reaching loop end)
+	loop_count_gt1_c         : assume property (!(id_stage_i.gen_hwloop_regs.hwloop_regs_i.hwlp_we_i[2] && id_stage_i.gen_hwloop_regs.hwloop_regs_i.hwlp_cnt_data_i==1));
+
+	// loop 1 is outer loop
+	loop1_ouuter_loop_c      : assume property (!(id_stage_i.gen_hwloop_regs.hwloop_regs_i.hwlp_counter_q[0]>0 && id_stage_i.hwlp_regid==1 && id_stage_i.hwlp_we));
+
+	// end addresses 8 apart
+	loop_end_min_sitance_c   : assume property (!(id_stage_i.gen_hwloop_regs.hwloop_regs_i.hwlp_counter_q[0]>0 && id_stage_i.gen_hwloop_regs.hwloop_regs_i.hwlp_counter_q[1]>0 && id_stage_i.gen_hwloop_regs.hwloop_regs_i.hwlp_end_q[1]<id_stage_i.gen_hwloop_regs.hwloop_regs_i.hwlp_end_q[0]+33'h8));
+
+	// do not setup illegal end address in inner loop
+	loop_inner_address_c     : assume property (!(id_stage_i.gen_hwloop_regs.hwloop_regs_i.hwlp_counter_q[1]>0 && id_stage_i.gen_hwloop_regs.hwloop_regs_i.hwlp_we_i[1] && !id_stage_i.gen_hwloop_regs.hwloop_regs_i.hwlp_regid_i &&id_stage_i.gen_hwloop_regs.hwloop_regs_i.hwlp_end_q[1]<id_stage_i.gen_hwloop_regs.hwloop_regs_i.hwlp_end_data_i+33'h8));
+
+	// memory stalls in hwloops seem problematic (ebreak retires before earlier dmem instruction)
+	no_mem_stall_in_hwloop_c : assume property (id_stage_i.controller_i.ctrl_fsm_cs==cv32e40p_pkg::DECODE_HWLOOP && load_store_unit_i.cnt_q>0|->`core.data_rvalid_i);
+`else
+	no_hwloop_c              : assume property (!id_stage_i.controller_i.is_hwlp_body);
+`endif
+`endif
+
+`ifdef CFG_XC
+	clk_en_c: assume property (`core.pulp_clock_en_i);
+`endif
+
+// MEMORY INTERFACE CONSTRAINTS //
+
+//
+// The following set of constraints could be used to constrain memory interfaces in case bus protocols implemented are not tool supported.
+// **W** Use only in case bus protocols implemented are not tool supported
+//
+
+`ifdef CUSTOM_MEM_INTERFACES
+	`include "mem_constraints.sv"
+	localparam MAX_WAIT=DMEM_MAX_WAIT;
+`else
+	localparam MAX_WAIT=obi_dmem_checker.MAX_WAIT;
+`endif
+
+// PERFORMANCE ENHANCEMENT CONSTRAINTS //
+
+//
+// The following set of constraints could be used to enhance properties' runtime.
+// **W** If ever used, these constraints have to be removed totally afterwards to achieve full verification.
+//
+
+//
+// "restrict_regs" restricts instruction source and destination indices to a subset of registers.
+// By default, the following register indices are chosen: 0 to 3, and 8 to 9 in presence of compressed extensions.
+//
+function automatic restrict_regs(input dec_t dec);
+	restrict_regs=1'b1;
+	foreach (dec.RS[i])
+		if (dec.RS[i].valid)
+//			restrict_regs&=dec.RS[i].idx<4 || (MISA.C|Zca) && dec.RS[i].idx inside {5'd8,5'd9};
+			restrict_regs&=dec.RS[i].idx inside {5'd0, 5'd1, 5'd2, 5'd4, 5'd8, 5'd12, 5'd16};
+	foreach (dec.RD[i])
+		if (dec.RD[i].valid)
+//			restrict_regs&=dec.RD[i].idx<4 || (MISA.C|Zca) && dec.RD[i].idx inside {5'd8,5'd9};
+			restrict_regs&=dec.RD[i].idx inside {5'd0, 5'd1, 5'd2, 5'd4, 5'd8, 5'd12, 5'd16};
+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)
+	`ifndef COMPLETENESS
+		`ifndef RESTRICT_REGISTER_INDEX
+//			&& (reg_idx<4 || (MISA.C|Zca) && reg_idx inside {5'd8,5'd9})
+			&& (reg_idx inside {5'd0, 5'd1, 5'd2, 5'd4, 5'd8, 5'd12, 5'd16})
+		`endif
+	`endif
+	);
+`endif
+
+// GRADUAL VERIFICATION CONSTRAINTS //
+
+//
+// The following set of constraints could be used for a gradual setup of a new core.
+// **W** If ever used, these constraints have to be removed totally afterwards to achieve full verification.
+//
+
+`ifdef LIMIT_TOTAL_INSTR_COUNT
+	// Limit total number of instructions allowed in the pipeline
+	limit_total_instr_count_c : assume property (disable iff (~rst_n) full[0] -> id_instr_cnt<`LIMIT_TOTAL_INSTR_COUNT);
+`endif

scripts/riscv_isa_formal/common/core_checker.sv

@@ -0,0 +1,26 @@
+// 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.
+
+///////////////////////////////////////////////////////////////////////////////
+//                                                                           //
+// RISC-V Checker                                                            //
+//                                                                           //
+///////////////////////////////////////////////////////////////////////////////
+
+
+
+
+This file is available only to Siemens Questa Processor customers and is available by submitting a request to Siemens support center to get it.

scripts/riscv_isa_formal/common/io.sv

@@ -0,0 +1,88 @@
+// 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.
+
+	// Data memory interface
+	input                 dmem_req_we         ='0, // Data memory request type
+	input[3:0]            dmem_req_be         ='0, // Data memory request byte enable
+	input[1:0]            dmem_req_size       ='0, // Data memory request size
+	input                 dmem_req_sign       ='0, // Data memory request sign
+
+	// Exceptions & Debug
+	input                 is_sstep            ='0, // Single stepping of debug mode
+	input                 xcpt_bp_if          ='0, // Instruction address breakpoint exception
+	input                 xcpt_bp_ld          ='0, // Load address breakpoint exception
+	input                 xcpt_bp_samo        ='0, // Store/ AMO address breakpoint exception
+	input                 xcpt_dbg_bp_if      ='0, // Debug instruction address breakpoint exception
+	input                 xcpt_dbg_bp_ld      ='0, // Debug load address breakpoint exception
+	input                 xcpt_dbg_bp_samo    ='0, // Debug Store/ AMO address breakpoint exception
+	input                 xcpt_af_instr_1st   ='0, // Instruction access fault exception
+	input                 xcpt_af_instr_2nd   ='0, // Instruction second access fault exception
+	input                 xcpt_af_ld_1st      ='0, // Load access fault exception
+	input                 xcpt_af_ld_2nd      ='0, // Load second access fault exception
+	input                 xcpt_af_samo_1st    ='0, // Store/ AMO access fault exception
+	input                 xcpt_af_samo_2nd    ='0, // Store/ AMO second access fault exception
+	input                 xcpt_pf_instr_1st   ='0, // Instruction page fault exception
+	input                 xcpt_pf_instr_2nd   ='0, // Instruction second access page fault exception
+	input                 xcpt_pf_ld_1st      ='0, // Load page fault exception
+	input                 xcpt_pf_ld_2nd      ='0, // Load second access page fault exception
+	input                 xcpt_pf_samo_1st    ='0, // Store/ AMO page fault exception
+	input                 xcpt_pf_samo_2nd    ='0, // Store/ AMO second access page fault exception
+	input                 xcpt_ma_ld          ='0, // Load address misaligned exception
+	input                 xcpt_ma_samo        ='0, // Store/AMO address misaligned exception
+
+	// Multiplication & Division
+	input                 mul_op_valid        ='0, // Multiplication operation validity
+	input[XLEN-1:0]       mul_op_a            ='0, // Multiplication first source operand
+	input[XLEN-1:0]       mul_op_b            ='0, // Multiplication second source operand
+	input[XLEN-1:0]       mul_op_c            ='0, // Multiplication third source operand
+	input[XLEN-1:0]       mul_result          ='0, // Multiplication operation result
+	input                 mul_result_valid    ='0, // Multiplication operation result validity
+	input                 div_op_valid        ='0, // Division operation validity
+	input[XLEN-1:0]       div_op_a            ='0, // Division first source operand
+	input[XLEN-1:0]       div_op_b            ='0, // Division second source operand
+	input[$clog2(XLEN):0] div_op_b_shift      ='0, // Division second source operand shift amount
+	input[XLEN-1:0]       div_result          ='0, // Division operation result
+	input                 div_result_valid    ='0, // Division operation result validity
+
+	// Floating point
+	input                 fpu_op_valid        ='0, // FPU operation validity
+	input[XLEN-1:0]       fpu_op_a            ='0, // FPU first source operand
+	input[XLEN-1:0]       fpu_op_b            ='0, // FPU second source operand
+	input[XLEN-1:0]       fpu_op_c            ='0, // FPU third source operand
+	input Frm             fpu_rm              ='0, // FPU rounding mode
+	input Fflags          fpu_flags           ='0, // FPU flags
+	input[XLEN-1:0]       fpu_result          ='0, // FPU operation result
+	input                 fpu_result_valid    ='0, // FPU operation result validity
+
+	// Design specific
+	input                 is_debug            ='0, // Core is about to enter debug mode
+	input                 is_interrupt        ='0, // Core is about to encounter an interrupt
+	input[XLEN-1:0]       boot_addr           ='0, // Boot address
+
+	input                 rf_we_lsu           ='0,
+	input[5:0]            rf_waddr_lsu        ='0,
+	input[1:0]            lsu_data_type       ='0,
+	input[1:0]            lsu_data_sign       ='0,
+	input[1:0]            lsu_data_offset     ='0,
+	input                 fpu_s_cycle         ='0,
+	input                 fpu_m_cycle         ='0,
+	input[5:0]            fpu_waddr           ='0,
+	input[5:0]            fpu_waddr_ex        ='0,
+	input[1:0]            fpu_lat_ex          ='0,
+	input[5:0]            fpu_op_ex           ='0,
+	input[XLEN-1:0]       dot_mul_op_a        ='0,
+	input[XLEN-1:0]       dot_mul_op_b        ='0,
+	input[XLEN-1:0]       dot_mul_op_c        ='0