diff --git a/scripts/riscv_isa_formal/Makefile b/scripts/riscv_isa_formal/Makefile
new file mode 100755
index 000000000..f344b819b
--- /dev/null
+++ b/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)
+
diff --git a/scripts/riscv_isa_formal/README.md b/scripts/riscv_isa_formal/README.md
new file mode 100755
index 000000000..4ba93b08e
--- /dev/null
+++ b/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:
+ 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
diff --git a/scripts/riscv_isa_formal/common/constraints.sv b/scripts/riscv_isa_formal/common/constraints.sv
new file mode 100755
index 000000000..082432653
--- /dev/null
+++ b/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]0&&id_stage_i.gen_hwloop_regs.hwloop_regs_i.hwlp_end_q[1]0 && pc_id>=id_stage_i.gen_hwloop_regs.hwloop_regs_i.hwlp_start_q[0] && pc_id0 && pc_id>=id_stage_i.gen_hwloop_regs.hwloop_regs_i.hwlp_start_q[1] && pc_id0 && 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]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]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
diff --git a/scripts/riscv_isa_formal/common/core_checker.sv b/scripts/riscv_isa_formal/common/core_checker.sv
new file mode 100755
index 000000000..439347bc5
--- /dev/null
+++ b/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.
diff --git a/scripts/riscv_isa_formal/common/io.sv b/scripts/riscv_isa_formal/common/io.sv
new file mode 100755
index 000000000..ae97b2456
--- /dev/null
+++ b/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
diff --git a/scripts/riscv_isa_formal/common/other_bindings.sv b/scripts/riscv_isa_formal/common/other_bindings.sv
new file mode 100755
index 000000000..b026c1484
--- /dev/null
+++ b/scripts/riscv_isa_formal/common/other_bindings.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
+ .dmem_req_we (data_we_o),
+ .dmem_req_be (data_be_o),
+ .dmem_req_size (),
+ .dmem_req_sign (),
+
+ // Exceptions & Debug
+ .is_sstep (debug_single_step),
+ .xcpt_bp_if (),
+ .xcpt_bp_ld (),
+ .xcpt_bp_samo (),
+ .xcpt_dbg_bp_if (),
+ .xcpt_dbg_bp_ld (),
+ .xcpt_dbg_bp_samo (),
+ .xcpt_af_instr_1st (),
+ .xcpt_af_instr_2nd (),
+ .xcpt_af_ld_1st (),
+ .xcpt_af_ld_2nd (),
+ .xcpt_af_samo_1st (),
+ .xcpt_af_samo_2nd (),
+ .xcpt_pf_instr_1st (),
+ .xcpt_pf_instr_2nd (),
+ .xcpt_pf_ld_1st (),
+ .xcpt_pf_ld_2nd (),
+ .xcpt_pf_samo_1st (),
+ .xcpt_pf_samo_2nd (),
+ .xcpt_ma_ld (),
+ .xcpt_ma_samo (),
+
+ // Multiplication & Division
+ .mul_op_valid (),
+ .mul_op_a (ex_stage_i.mult_i.op_a_i),
+ .mul_op_b (ex_stage_i.mult_i.op_b_i),
+ .mul_op_c (ex_stage_i.mult_i.op_c_i),
+ .mul_result (ex_stage_i.mult_i.result_o),
+ .mul_result_valid (),
+ .div_op_valid (),
+ .div_op_a (ex_stage_i.alu_i.alu_div_i.OpA_DI),
+ .div_op_b (ex_stage_i.alu_i.alu_div_i.OpB_DI),
+ .div_op_b_shift (ex_stage_i.alu_i.alu_div_i.OpBShift_DI),
+ .div_result (ex_stage_i.alu_i.alu_div_i.Res_DO),
+ .div_result_valid (ex_stage_i.alu_i.div_ready),
+
+ // Floating point
+ .fpu_op_valid (ex_stage_i.apu_req),
+ .fpu_op_a (ex_stage_i.apu_operands_o[0]),
+ .fpu_op_b (ex_stage_i.apu_operands_o[1]),
+ .fpu_op_c (ex_stage_i.apu_operands_o[2]),
+ .fpu_rm (),
+ .fpu_flags (ex_stage_i.fpu_fflags_o),
+ .fpu_result (ex_stage_i.apu_result),
+ .fpu_result_valid (ex_stage_i.apu_valid),
+
+ // Design specific
+ .is_debug (id_stage_i.controller_i.ctrl_fsm_cs inside {DBG_TAKEN_ID,DBG_TAKEN_IF,DBG_FLUSH}),
+ .is_interrupt (id_stage_i.int_controller_i.irq_req_ctrl_o),
+ .boot_addr ({boot_addr_i[31:2],2'b00}),
+
+ .rf_we_lsu (ex_stage_i.regfile_we_lsu),
+ .rf_waddr_lsu (ex_stage_i.regfile_waddr_lsu),
+ .lsu_data_type (load_store_unit_i.data_type_q),
+ .lsu_data_sign (load_store_unit_i.data_sign_ext_q),
+ .lsu_data_offset (load_store_unit_i.rdata_offset_q),
+ .fpu_s_cycle (ex_stage_i.apu_singlecycle),
+ .fpu_m_cycle (ex_stage_i.apu_multicycle),
+ .fpu_waddr (ex_stage_i.apu_waddr),
+ .fpu_waddr_ex (apu_waddr_ex),
+ .fpu_lat_ex (apu_lat_ex),
+ .fpu_op_ex (apu_op_ex),
+ .dot_mul_op_a (ex_stage_i.mult_dot_op_a_i),
+ .dot_mul_op_b (ex_stage_i.mult_dot_op_b_i),
+ .dot_mul_op_c (ex_stage_i.mult_dot_op_c_i)
diff --git a/scripts/riscv_isa_formal/common/setup.tcl b/scripts/riscv_isa_formal/common/setup.tcl
new file mode 100755
index 000000000..8f68ea6b3
--- /dev/null
+++ b/scripts/riscv_isa_formal/common/setup.tcl
@@ -0,0 +1,588 @@
+# 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.
+
+proc duration {int_time} {
+ set timeList [list]
+ if {$int_time == 0} {
+ return "0 Sec"
+ } else {
+ foreach div {86400 3600 60 1} mod {0 24 60 60} name {Day Hour Min Sec} {
+ set n [expr {$int_time / $div}]
+ if {$mod > 0} {set n [expr {$n % $mod}]}
+ if {$n > 1} {
+ lappend timeList "$n ${name}s"
+ } elseif {$n == 1} {
+ lappend timeList "$n $name"
+ }
+ }
+ return [join $timeList]
+ }
+}
+
+proc quantify_run {{cmd_limit 0} {run 0} {no_cuts {}} {limit_scale 2.0} {effort 4} {skip_effort_level 0} {html_dir {}} {result_file {}} {checks {}} {prev_run_result {}} {skip_files {}}} {
+
+ puts "\n-INFO- Start of Quantify Run ($run)::\n\nChecks Included::\n\n$checks"
+
+ set_limit -command_real_time $cmd_limit
+ set run_start_t [clock seconds]
+ puts "\n-INFO- Launching Quantify Command::\n\nquantify -assume_hold -additional_args \[list $no_cuts -limit_scale $limit_scale -use_single_prover\] -effort $effort -skip_effort_level $skip_effort_level -html $html_dir -save $result_file -checks $checks -incremental $prev_run_result -skip_files $skip_files\n"
+ catch {quantify -assume_hold -additional_args [list $no_cuts -limit_scale $limit_scale -use_single_prover] -effort $effort -skip_effort_level $skip_effort_level -html $html_dir -save $result_file -checks $checks -incremental $prev_run_result -skip_files $skip_files}
+ set run_end_t [expr [clock seconds] - $run_start_t]
+ set_limit -default
+
+ puts "\n-INFO- End of Quantify Run ($run) | Time spent:: [duration $run_end_t]\n"
+}
+
+## 0. DESIGN SETUP ##
+
+### SETTING UP THE DESIRED CONFIGURATION, RUN & APP ###
+## source the setup.inc as the following: [onespin -i setup.inc ]
+## arg1: what configuration to set .
+## arg2: what processor verification mode to set .
+## arg3: what app to launch on top of the processor app.
+## ------------------------------------------------------------------------------------------------------------------
+
+set configs [dict create \
+ "DEF" [dict create \
+ description "RV32IMCZicsr_Zifencei" \
+ elab "-verilog_parameter {}" \
+ define "" \
+ json "" \
+ ] \
+ "F0" [dict create \
+ description "RV32IMFCZicsr_Zifencei with FPU latency params set to 0" \
+ elab "-verilog_parameter {FPU=1 FPU_ADDMUL_LAT=0 FPU_OTHERS_LAT=0}" \
+ define "CFG_F" \
+ json "" \
+ ] \
+ "ZF0" [dict create \
+ description "RV32IMCZicsr_Zifencei_Zfinx with FPU latency params set to 0" \
+ elab "-verilog_parameter {FPU=1 ZFINX=1 FPU_ADDMUL_LAT=0 FPU_OTHERS_LAT=0}" \
+ define "CFG_ZFINX" \
+ json "" \
+ ] \
+ "XP" [dict create \
+ description "RV32IMCZicsr_Zifencei_Xpulp" \
+ elab "-verilog_parameter {COREV_PULP=1}" \
+ define "CFG_XP" \
+ json "Xpulp.json Zfinx.json" \
+ ] \
+ "XPF0" [dict create \
+ description "RV32IMFCZicsr_Zifencei_Xpulp with FPU latency params set to 0" \
+ elab "-verilog_parameter {FPU=1 COREV_PULP=1 FPU_ADDMUL_LAT=0 FPU_OTHERS_LAT=0}" \
+ define "CFG_XP CFG_F" \
+ json "Xpulp.json" \
+ ] \
+ "XPF1" [dict create \
+ description "RV32IMFCZicsr_Zifencei_Xpulp with FPU latency params set to 1" \
+ elab "-verilog_parameter {FPU=1 COREV_PULP=1 FPU_ADDMUL_LAT=1 FPU_OTHERS_LAT=1}" \
+ define "CFG_XP CFG_F" \
+ json "Xpulp.json" \
+ ] \
+ "XPF2" [dict create \
+ description "RV32IMFCZicsr_Zifencei_Xpulp with FPU latency params set to 2" \
+ elab "-verilog_parameter {FPU=1 COREV_PULP=1 FPU_ADDMUL_LAT=2 FPU_OTHERS_LAT=2}" \
+ define "CFG_XP CFG_F" \
+ json "Xpulp.json" \
+ ] \
+ "XPZF0" [dict create \
+ description "RV32IMCZicsr_Zifencei_Zfinx_Xpulp with FPU latency params set to 0" \
+ elab "-verilog_parameter {FPU=1 ZFINX=1 COREV_PULP=1 FPU_ADDMUL_LAT=0 FPU_OTHERS_LAT=0}" \
+ define "CFG_XP CFG_ZFINX" \
+ json "Xpulp.json Zfinx.json" \
+ ] \
+ "XPZF1" [dict create \
+ description "RV32IMCZicsr_Zifencei_Zfinx_Xpulp with FPU latency params set to 1" \
+ elab "-verilog_parameter {FPU=1 ZFINX=1 COREV_PULP=1 FPU_ADDMUL_LAT=1 FPU_OTHERS_LAT=1}" \
+ define "CFG_XP CFG_ZFINX" \
+ json "Xpulp.json Zfinx.json" \
+ ] \
+ "XPZF2" [dict create \
+ description "RV32IMCZicsr_Zifencei_Zfinx_Xpulp with FPU latency params set to 2" \
+ elab "-verilog_parameter {FPU=1 ZFINX=1 COREV_PULP=1 FPU_ADDMUL_LAT=2 FPU_OTHERS_LAT=2}" \
+ define "CFG_XP CFG_ZFINX" \
+ json "Xpulp.json Zfinx.json" \
+ ] \
+ "XPXC" [dict create \
+ description "RV32IMCZicsr_Zifencei_Xpulp_Xcluster" \
+ elab "-verilog_parameter {COREV_PULP=1 COREV_CLUSTER=1}" \
+ define "CFG_XP CFG_XC" \
+ json "Xpulp.json Xcluster.json Zfinx.json" \
+ ] \
+ "XPXCZF2" [dict create \
+ description "RV32IMCZicsr_Zifencei_Zfinx_Xpulp_Xcluster with FPU latency params set to 2" \
+ elab "-verilog_parameter {FPU=1 ZFINX=1 COREV_PULP=1 COREV_CLUSTER=1 FPU_ADDMUL_LAT=2 FPU_OTHERS_LAT=2}" \
+ define "CFG_XP CFG_XC CFG_ZFINX" \
+ json "Xpulp.json Xcluster.json Zfinx.json" \
+ ] \
+]
+
+set pve_modes [dict create \
+ "DEF" [dict create \
+ description "DEF: Control path verification of all instructions and datapath verification of all instructions except multiplication, division or floating point ones" \
+ define "" \
+ ] \
+ "DPM" [dict create \
+ description "DPM: Data path verification of multiplication/ division instructions" \
+ define "PVE_M_SUPPORT RESTRICT_MUL_OPS_FREE_BITS=1" \
+ ] \
+ "DPF" [dict create \
+ description "DPF: Data path verification of floating-point instructions" \
+ define "PVE_FPU_SUPPORT RESTRICT_MUL_OPS_FREE_BITS=1" \
+ ] \
+]
+
+set apps [dict create \
+ "PRC" [dict create \
+ description "PRC: Property Checking" \
+ compile "-dontcare_handling any -signal_domain {{scan_cg_en_i} 0}" \
+ ] \
+ "QTF" [dict create \
+ description "QTF: Quantify" \
+ compile "-dontcare_handling any -signal_domain {{scan_cg_en_i} 0} -constant [list [list core_i.id_stage_i.register_file_i.rst_n 1] ]" \
+ ] \
+ "VCI" [dict create \
+ description "VCI: Verification Coverage Integration" \
+ compile "-dontcare_handling any -signal_domain {{scan_cg_en_i} 0}" \
+ ] \
+]
+
+if {$::argc>0} {
+ lassign $::argv cfg pve_mode app
+ if {$cfg ni [dict keys $configs]} {
+ onespin::message -error "Only configurations [join [dict keys $configs] ,] are supported!"
+ return -code error
+ }
+ if {$pve_mode ni [dict keys $pve_modes]} {
+ onespin::message -error "Only processor verification modes [join [dict keys $pve_modes] ,] are supported!"
+ return -code error
+ } elseif {$pve_mode eq "DPF" && $cfg in {"DEF" "XP" "XPXC"} } {
+ onespin::message -error "Floating-point configuration must be selected in order to perform data path verification!"
+ return -code error
+ }
+ if {$app ni [dict keys $apps]} {
+ onespin::message -error "Only apps [join [dict keys $apps] ,] are supported!"
+ return -code error
+ }
+} else {
+ if {[get_tool_info -gui]} {
+ set cfg [string index [onespin::ask_user -default 0 -alternatives [lmap {k d} $configs {string cat "$k - " [dict get $d description]}] "Select which RISC-V configuration to set up:"] 0]
+ set pve_mode [string index [onespin::ask_user -default "DEF" -alternatives [lmap {k d} $pve_modes {string cat "$k - " [dict get $d description]}] "Select which processor verification mode to set:"] 0]
+ set app [string index [onespin::ask_user -default "PRC" -alternatives [lmap {k d} $apps {string cat "$k - " [dict get $d description]}] "Select which app to launch:"] 0]
+ } else {
+ set cfg "DEF"
+ set pve_mode "DEF"
+ set app "PRC"
+ }
+}
+set target cv32e40p_top
+set core_inst core_i
+set prefix ${core_inst}.
+##
+
+### ADJUST TO READ-IN THE NEW DESIGN ###
+onespin::set_parameter disable_intermediate_arithmetic_signals 1
+set cwd [pwd]
+set_session_option -naming_style sv
+set_compile_option {*}[dict get $apps $app compile]
+set_elaborate_option {*}[dict get $configs $cfg elab] -top $target
+cd cv32e40p
+source $cwd/setup_mv.tcl
+set_reset_sequence -low rst_ni
+cd $cwd
+
+set cfg_dir $cwd/$cfg
+set pve_mode_dir $cwd/$cfg/$pve_mode
+set app_dir $cwd/$cfg/$pve_mode/$app
+file mkdir $cfg_dir
+file mkdir $pve_mode_dir
+file mkdir $app_dir
+##
+
+### PROCESSOR APP FLOW ###
+
+## ---------------------------------------------------------------------------------------------------------------------------------
+## 1 > 2 > 3 > 4 > 5 > 6 > 7
+## ---------------------------------------------------------------------------------------------------------------------------------
+## PRE-ANALYSIS | DESIGN | POST-ANALYSIS | ASSERTION | ASSERTION | PERFORMANCE | ASSERTION
+## CONFIGURATION | ANALYSIS | CONFIGURATION | GENERATION | READING & RETUNING | ENHANCEMENT | RUNNING & DEBUGGING
+## ---------------------------------------------------------------------------------------------------------------------------------
+
+## ---------------------------------------------------------------------------------------------------------------------------------
+## processor_integrity:: | DESCRIPTION
+## ---------------------------------------------------------------------------------------------------------------------------------
+## extract_ISA | Extract ISA from a RISC-V based processor core and store data in a processor database.
+## -core_instance <> | Specify instance name of the core in the DUV to instantiate the VIP on.
+## -csr_addr <> | Specify CSR address signal that might be used to assist extraction.
+## -csr_rdata <> | Specify CSR read data signal that might be used to assist extraction.
+## merge_data | Merge JSON data into the database.
+## -file <> | Specify JSON file to be merged.
+## -configuration <> | Specify predefined JSON configuration to be merged.
+## generate_assertions | Generate assertions for verifying the RISC-V core based on the database.
+## -create_individual_checks <> | Specify extensions for which assertions are generated per instruction.
+## -exclude_extensions <> | Specify extensions for which assertions generation is supressed.
+## -include_extensions <> | Specify extensions only for which assertions are generated.
+## generate_IVA | Perform initial value abstraction of architecture state.
+## -candidates <> | Specify architecture register fields to be abstracted.
+## analyze_trace | Perform detailed trace analysis of run assertions.
+## save_data | Write the processor database, or part of it, to a JSON file.
+## clear_data | Clear JSON data from the processor database.
+## ---------------------------------------------------------------------------------------------------------------------------------
+## For full app documentation run "help *processor_integrity::*" or refer to Chapter 14. of the User Manual.
+## ---------------------------------------------------------------------------------------------------------------------------------
+
+## 0. APP SETUP ##
+
+package require processor_integrity
+
+### APPEND THE FOLLOWING SET OF DEFINES (ONLY IF NECESSARY) ###
+## ---------------------------------------------------------------------------------------------------------------------------------
+## DEFINE | USE CASE IF SET
+## ---------------------------------------------------------------------------------------------------------------------------------
+## GRADUAL VERIFICATION ##
+## SKIP_PC_CHECK | Skip checking PC register updates.
+## SKIP_RF_CHECK | Skip checking register file updates.
+## SKIP_CSR_CHECK | Skip checking CSR updates and reads.
+## SKIP_DMEM_CHECK | Skip checking data memory requests.
+## LIMIT_TOTAL_INSTR_COUNT | Limit total # of instructions allowed in the pipeline.
+## PERFORMANCE ENHANCEMENT ##
+## RESTRICT_REGS | Restrict instruction decoding & register file verification to a subset of registers.
+## RESTRICT_REGISTER_INDEX | Restrict register file verification to one register only, instruction decoding is not affected.
+## RESTRICT_CHECK_DATA_SLICE | Restrict register file data and memory write data verification to a slice or even a bit.
+## RESTRICT_MUL_OPS_FREE_BITS | Restrict # of operand bits allowed to toggle checking multiplication/ division instruction datapath.
+## RESTRICT_DMEM_STALL_CYCLES | Restrict data memory stall cycles to specific number. Has an effect w/ protocol VIPs' usage.
+## TAILORED VERIFICATION ##
+## PVE_M_SUPPORT | Enable checking M extension data path. By default, only the control path is checked.
+## PVE_FPU_SUPPORT | Enable checking F extension data path. By default, only the control path is checked.
+## CHECK_ACCESS_FAULTS | Enable checking all access faults fully according to the privileged specification or Smepmp.
+## CUSTOM_MEM_INTERFACES | Constrain memory interfaces. Use only in case bus protocols implemented are not tool supported.
+## ---------------------------------------------------------------------------------------------------------------------------------
+lappend defines {*}[dict get $configs $cfg define] {*}[dict get $pve_modes $pve_mode define] RESTRICT_REGS RESTRICT_DMEM_STALL_CYCLES=2
+##
+
+### RE-SET THE FOLLOWING SET OF VARIABLES (ONLY IF NECESSARY) ###
+lappend pre_analysis_json_files_to_merge spec.json {*}[dict get $configs $cfg json]
+set csr_addr_to_assist_analysis {}
+set csr_rdata_to_assist_analysis {}
+set core_instance_to_instantiate_vip_on ${core_inst}
+lappend post_analysis_json_files_to_merge spec.json {*}[dict get $configs $cfg json] core.json
+lappend extensions_to_generate_individual_checks_for F Zfinx
+set extensions_to_exclude_assertion_generation_for {}
+if {"CV_LOOP" in $defines} {
+ lappend pre_analysis_json_files_to_merge Xpulp_hwlp.json
+ lappend post_analysis_json_files_to_merge Xpulp_hwlp.json
+}
+##
+
+### EXTEND THE FOLLOWING LISTS BY THE RESPECTIVE RTL SIGNALS (ONLY IF NECESSARY) ###
+lappend mul_signals_to_cut ${prefix}ex_stage_i.mult_i.result_o ${prefix}ex_stage_i.alu_i.alu_div_i.Res_DO ${prefix}ex_stage_i.alu_i.alu_div_i.Cnt_DP
+lappend fpu_signals_to_cut ${prefix}apu_result_i ${prefix}apu_flags_i
+lappend rtl_signals_to_cut
+lappend rtl_signals_to_disassemble ${prefix}instr_rdata_i ${prefix}instr_rdata_id ${prefix}if_stage_i.instr_aligned
+##
+
+if {![info exists reuse_files] || !$reuse_files} {
+
+## 1. PRE-ANALYSIS CONFIGURATION ##
+
+ foreach i ${pre_analysis_json_files_to_merge} {
+ processor_integrity::merge_data -file ${i}
+ }
+
+## 2. DESIGN ANALYSIS ##
+
+ processor_integrity::extract_ISA -csr_addr $csr_addr_to_assist_analysis -csr_rdata $csr_rdata_to_assist_analysis -core_instance $core_instance_to_instantiate_vip_on
+
+## 3. POST-ANALYSIS CONFIGURATION ##
+
+ foreach i ${post_analysis_json_files_to_merge} {
+ processor_integrity::merge_data -file ${i}
+ }
+
+ if {"CFG_ZFINX" in $defines} {
+ onespin::data::set ISA/Z/Zfinx true
+ }
+
+ if {$pve_mode ne "DEF"} {
+ onespin::data::set PVE/checker_instance "RV_chk_DP"
+ }
+
+## 4. ASSERTION GENERATION ##
+
+ cd $pve_mode_dir
+ processor_integrity::generate_assertions -create_individual_checks $extensions_to_generate_individual_checks_for -exclude_extensions $extensions_to_exclude_assertion_generation_for -force
+ cd $cwd
+} else {
+ puts "-W- Re-using previously generated files! Make sure to re-generate all files on adopting a new tool version or changing the JSON configuration!"
+ source $pve_mode_dir/RISCV_disass.tcl
+ source RISCV_disass.tcl
+}
+
+## 5. ASSERTION READING & RETUNING ##
+
+### USE TO CONSTRAIN MEMORY INTERFACES (ONLY IF BUS PROTOCOLS IMPLEMENTED ARE TOOL SUPPORTED) ###
+## Instantiate the respective bus protocol VIP for each of the fetch and data memory interfaces
+## The VIPs in this case are used to check and more importantly constrain memory interfaces
+## Read in the instantiated VIPs, my_{}.sv, using the read_sva command below
+#instantiate_vip -addr_sig instr_addr_o -generated_instance_name obi_imem_checker -filename obi_imem.sv obi
+#instantiate_vip -addr_sig data_addr_o -generated_instance_name obi_dmem_checker -filename obi_dmem.sv obi
+##
+
+read_sva -define $defines -include_path $pve_mode_dir {core_checker.sv $pve_mode_dir/bind.sv vips/obi_?mem.sv}
+
+## 7.1 ASSERTION RUNNING & DEBUGGING ##
+
+### USE TO RUN INITIAL SET OF ASSERTIONS ###
+set_check_option -prover_exec_order { { approver1 approver4 prover2:0 prover2:8 prover2:11 disprover1 disprover3 } } -disprover1_steps 40 -disprover3_steps 40
+check [get_checks -filter name=~"*invariant_a"||name=~"*legal_CSR_reset_state_a"||name=~"*RESET_a"]
+##
+
+## 6. PERFORMANCE ENHANCEMENT ##
+
+### USE TO COMPUTE INVARIANTS (IF NECESSARY) ###
+compute_invariants
+##
+
+if {$app eq "PRC"} {
+ ### USE TO PERFORM AUTOMATIC INITIAL VALUE ABSTRACTION (IVA) OF ARCHITECTURE STATE (IF NECESSARY) ###
+ lappend candidates X F frm
+ if {"CFG_XP" in $defines} {
+ lappend candidates lpstart0 lpstart1 lpend0 lpend1
+ }
+ processor_integrity::generate_IVA -candidates $candidates
+ ##
+}
+
+### USE TO CUT DESIGN COMPLEX SIGNALS (IF NECESSARY) ###
+if {$pve_mode ne "DPM"} {
+ lappend rtl_signals_to_cut {*}$mul_signals_to_cut
+}
+if {($pve_mode ne "DPF") && ("CFG_F" in $defines || "CFG_ZFINX" in $defines)} {
+ lappend rtl_signals_to_cut {*}$fpu_signals_to_cut
+}
+add_cut_signals $rtl_signals_to_cut
+cut_signals
+##
+
+## 7.2 ASSERTION RUNNING & DEBUGGING ##
+
+### USE TO EASE DEBUGGING BY DISASSEMBLING VALUES OF RTL SIGNALS HOLDING INSTRUCTION WORDS & RUN THE OTHER ASSERTIONS ###
+foreach i ${rtl_signals_to_disassemble} {
+ use_value_printer ${i} PVE_disass
+}
+##
+
+#set nb_processes 2
+#set nb_processes 3
+#set nb_processes 4
+#set nb_processes 5
+#set nb_processes 6
+#set nb_processes 8
+#set nb_processes 12
+set nb_processes 16
+#set nb_processes 24
+#set nb_processes 32
+
+set_check_option -verbose
+set_check_option -local_processes $nb_processes
+set_check_option -engine_licensing unlimited
+
+puts "\n-INFO- Launching $app app in $pve_mode mode with $nb_processes parallel processes.\n"
+
+#set_check_option -prover_exec_order { { approver1 approver4 prover2:0 prover2:8 prover2:11 disprover1 disprover3 } }
+set_check_option -prover_exec_order { { approver1 prover2:0 prover2:8 prover2:11 } }
+#set_check_option -disprover1_steps 40 -disprover3_steps 40
+
+check_consistency -category model_building -effort maximum
+exclude_check [get_checks -filter name=~"*hdl*"||name=~"*FSQRT_S_a*"||name=~"**FDIV_S_a*"]
+
+set DEF_checks [lsort -dictionary [get_checks -filter excluded==false&&(type==property||type==assertion)]]
+set DPM_checks [lsort -dictionary [get_checks -filter excluded==false&&(name=~"*RV32M.*"||name=~"*RV32X.CV_XDOT*"||name=~"*RV32X.CV_MUL*"||name=~"*RV32X.CV_MAC*"||name=~"*RV32X.CV_CPLXMUL*")]]
+set DPF_checks [lsort -dictionary [get_checks -filter excluded==false&&(name=~"*RV32F.*"||name=~"*RV32Zfinx.*")]]
+
+set group_1_checks [lsort -dictionary [concat core_i.RV_chk.ops.RESET_a [get_checks -filter excluded==false&&type==assertion]]]
+set group_2_checks [lsort -dictionary [list core_i.RV_chk.ops.XCPT_IF_ID_a core_i.RV_chk.RV32C.ARITH_a core_i.RV_chk.RV32C.BRANCH_Taken_a core_i.RV_chk.RV32C.BRANCH_a core_i.RV_chk.RV32C.JUMP_a core_i.RV_chk.RV32I.EBREAK_BreakPoint_a core_i.RV_chk.RV32I.MEM_MultiAccess_a core_i.RV_chk.RV32I.xRET_a core_i.RV_chk.RV32X.CV_ADD_X_a core_i.RV_chk.RV32X.CV_BITMAN_OTHER_a core_i.RV_chk.RV32X.CV_EXTRACTX_X_a core_i.RV_chk.RV32X.CV_INSERTX_a core_i.RV_chk.RV32X.CV_PACKXX_X_a core_i.RV_chk.RV32X.CV_SETUPX_a core_i.RV_chk.RV32X.CV_SHUFFLE2_X_a core_i.RV_chk.RV32Zicsr.CSRx_a]]
+set group_3_checks [lsort -dictionary [list core_i.RV_chk.ops.BUBBLE_a core_i.RV_chk.RV32I.ARITH_a core_i.RV_chk.RV32I.EBREAK_HaltReq_a core_i.RV_chk.RV32I.ECALL_a core_i.RV_chk.RV32I.FENCE_a core_i.RV_chk.RV32I.WFI_a core_i.RV_chk.RV32X.CV_ABS_X_a core_i.RV_chk.RV32X.CV_CLIPXX_a core_i.RV_chk.RV32X.CV_CMPEQ_X_a core_i.RV_chk.RV32X.CV_EXTRACTXX_a core_i.RV_chk.RV32X.CV_EXTXX_a core_i.RV_chk.RV32X.CV_INSERT_X_a core_i.RV_chk.RV32X.CV_SX_I_a core_i.RV_chk.RV32X.CV_SX_RI_a core_i.RV_chk.RV32X.CV_ADDXXNR_a core_i.RV_chk.RV32X.CV_SHUFFLEIX_SCI_B_a core_i.RV_chk.RV32X.CV_BSETX_a core_i.RV_chk.RV32X.CV_BXXIMM_Taken_a core_i.RV_chk.RV32X.CV_ENDX_a core_i.RV_chk.RV32X.CV_LXX_I_a core_i.RV_chk.RV32X.CV_LXX_RI_a core_i.RV_chk.RV32X.CV_SLL_X_a core_i.RV_chk.RV32X.CV_STARTX_a core_i.RV_chk.RV32X.CV_ADD_DIVX_a core_i.RV_chk.RV32X.CV_ADDXXN_a core_i.RV_chk.RV32X.CV_AVGU_X_a core_i.RV_chk.RV32X.CV_BCLRX_a core_i.RV_chk.RV32X.CV_SUB_DIVX_a core_i.RV_chk.RV32X.CV_SUBROTMJ_X_a core_i.RV_chk.RV32X.CV_SUBXXN_a core_i.RV_chk.RV32X.CV_SUBXXNR_a core_i.RV_chk.RV32X.CV_MAXU_X_a]]
+set group_4_checks [lsort -dictionary [concat [get_checks -filter excluded==false&&name=~"*RV32X.CV_ELW*"] core_i.RV_chk.RV32I.EBREAK_ForcedEntry_a core_i.RV_chk.RV32X.CV_COUNTX_a core_i.RV_chk.RV32X.CV_LXX_R_a core_i.RV_chk.RV32X.CV_MAXX_a core_i.RV_chk.RV32X.CV_SX_R_a core_i.RV_chk.RV32C.MEM_a core_i.RV_chk.RV32C.MEM_MultiAccess_a core_i.RV_chk.RV32I.BRANCH_a core_i.RV_chk.RV32I.BRANCH_Taken_a core_i.RV_chk.RV32I.JUMP_a core_i.RV_chk.RV32I.MEM_a core_i.RV_chk.RV32X.CV_ABS_a core_i.RV_chk.RV32X.CV_AND_X_a core_i.RV_chk.RV32X.CV_AVG_X_a core_i.RV_chk.RV32X.CV_BXXIMM_a core_i.RV_chk.RV32X.CV_CMPGE_X_a core_i.RV_chk.RV32X.CV_CMPGEU_X_a core_i.RV_chk.RV32X.CV_CMPGT_X_a core_i.RV_chk.RV32X.CV_CMPGTU_X_a core_i.RV_chk.RV32X.CV_CMPLE_X_a core_i.RV_chk.RV32X.CV_CMPLEU_X_a core_i.RV_chk.RV32X.CV_CMPLT_X_a core_i.RV_chk.RV32X.CV_CMPLTU_X_a core_i.RV_chk.RV32X.CV_CMPNE_X_a core_i.RV_chk.RV32X.CV_CPLXCONJ_a core_i.RV_chk.RV32X.CV_LXX_I_MultiAccess_a core_i.RV_chk.RV32X.CV_LXX_R_MultiAccess_a core_i.RV_chk.RV32X.CV_LXX_RI_MultiAccess_a core_i.RV_chk.RV32X.CV_MAX_X_a core_i.RV_chk.RV32X.CV_MIN_X_a core_i.RV_chk.RV32X.CV_MINU_X_a core_i.RV_chk.RV32X.CV_MINX_a core_i.RV_chk.RV32X.CV_OR_X_a core_i.RV_chk.RV32X.CV_SHUFFLE_X_a core_i.RV_chk.RV32X.CV_SLEX_a core_i.RV_chk.RV32X.CV_SRA_X_a core_i.RV_chk.RV32X.CV_SRL_X_a core_i.RV_chk.RV32X.CV_SUB_X_a core_i.RV_chk.RV32X.CV_SX_I_MultiAccess_a core_i.RV_chk.RV32X.CV_SX_R_MultiAccess_a core_i.RV_chk.RV32X.CV_SX_RI_MultiAccess_a core_i.RV_chk.RV32X.CV_XOR_X_a core_i.RV_chk.RV32Zifencei.FENCE_I_a]]
+set group_5_checks [lsort -dictionary [get_checks -filter excluded==false&&(name=~"*RV32M.DIV16_a*"||name=~"*RV32M.DIV32_a*"||name=~"*RV32M.MUL_a*"||name=~"*RV32X.CV_XDOT*"||name=~"*RV32X.CV_MUL*"||name=~"*RV32X.CV_MAC*"||name=~"*RV32X.CV_CPLXMUL*")]]
+set group_6_checks [lsort -dictionary [get_checks -filter excluded==false&&(name=~"*RV32F.*"||name=~"*RV32Zfinx.*")]]
+
+set skipped_files "*/fpnew_* {} */gated_clk_cell* {} */lzc* {} */pa_fdsu_* {} */pa_fpu_* {} */rr_arb_tree* {}"
+
+puts "\n-INFO- Compile options::\n\n\t[dict get $apps $app compile]\n"
+puts "\n-INFO- Elaborate options::\n\n\t[dict get $configs $cfg elab]\n"
+puts "\n-INFO- Defines::\n\n\t$defines\n"
+puts "\n-INFO- Cut signals::\n\n\t$rtl_signals_to_cut\n"
+
+if {$app eq "PRC"} {
+
+# set_check_option -prover_exec_order { { approver1 approver4 prover2:0 prover2:8 prover2:11 disprover1 disprover3 } }
+ set_check_option -prover_exec_order { { approver1 prover2:0 prover2:8 prover2:11 } }
+# set_check_option -prover_exec_order { { disprover1 disprover3 } } -disprover1_steps 20 -disprover3_steps 20
+
+ set all_checks [set ${pve_mode}_checks]
+ set checks_nb [llength $all_checks]
+ set nb_round [expr $checks_nb / $nb_processes]
+ set nb_remain [expr $checks_nb % $nb_processes]
+ puts "nb_round = $nb_round, nb_remain = $nb_remain"
+ for {set i 0} {$i < $nb_round} {incr i} {
+ set checks [lrange $all_checks [expr $i * $nb_processes] [expr ((($i + 1) * $nb_processes) - 1)]]
+ puts "[expr $i * $nb_processes] [expr ((($i + 1) * $nb_processes) - 1)]"
+ puts "\n-INFO- Launching Check Command::\n\ncheck $checks\n"
+ check $checks
+ cd $app_dir
+ start_message_log round_[expr $i + 1].log
+ report_result -details
+ stop_message_log
+ save_database -force round_[expr $i + 1]
+ cd $cwd
+ }
+ if {$nb_remain > 0} {
+ set checks [lrange $all_checks [expr $nb_round * $nb_processes] [expr (($nb_round * $nb_processes) + $nb_remain - 1)]]
+ puts "[expr $nb_round * $nb_processes] [expr (($nb_round * $nb_processes) + $nb_remain - 1)]"
+ puts "\n-INFO- Launching Check Command::\n\ncheck $checks\n"
+ check $checks
+ cd $app_dir
+ start_message_log round_[expr $i + 1].log
+ report_result -details
+ stop_message_log
+ save_database -force round_[expr $nb_round + 1]
+ cd $cwd
+ }
+
+ cd $app_dir
+ start_message_log report_signoff_${app}_${cfg}_${pve_mode}.log
+ report_result -signoff -details
+ stop_message_log
+ cd $cwd
+
+# set_check_option -prover_exec_order { { disprover1 disprover3 } }
+# puts "\n-INFO- Launching Check Command::\n\ncheck RV32M.DIV16_a\n"
+# check [get_checks -filter name=~"*RV32M.DIV16_a*"]
+# cd $app_dir
+# save_database -force
+# cd $cwd
+
+}
+
+if {$app eq "QTF"} {
+
+ source basics.tcl.obf
+
+ set_check_option -prover_exec_order { { disprover1 disprover3 } } -disprover1_steps 20 -disprover3_steps 20
+
+ set html "${app_dir}/html_results_${cfg}_${pve_mode}"
+ set results "${app_dir}/qtf_results_${cfg}_${pve_mode}_R"
+ set log "${app_dir}/${app}_${cfg}_${pve_mode}_R"
+
+ if {$pve_mode eq "DEF"} {
+
+ for {set i 1} {$i < 7} {incr i} {
+ puts "\nGroup (${i}) checks:\n\nTotal number of checks is: [llength [set group_${i}_checks]] \n"
+ foreach j [set group_${i}_checks] {
+ puts "$j"
+ }
+ }
+
+ for {set i 1} {$i < 7} {incr i} {
+ puts "Group (${i}) checks: Total number of checks is: [llength [set group_${i}_checks]]"
+ }
+
+# for {set i 1} {$i < 7} {incr i} {
+
+ set i 5
+
+ start_message_log ${log}${i}.log
+ if {$i == 1} {
+ quantify_run 0 $i {-no_cuts} 1.0 2 1 ${html}_L2_S1_R${i} ${results}${i} $group_1_checks {} {}
+ } elseif {$i == 2} {
+ quantify_run 0 $i {-no_cuts} 4.0 4 3 ${html}_L4_S4_R${i} ${results}${i} $group_2_checks ${results}[expr $i-1] $skipped_files
+ } elseif {$i == 3} {
+ quantify_run 0 $i {-no_cuts} 2.0 4 3 ${html}_L4_S2_R${i} ${results}${i} $group_3_checks ${results}[expr $i-1] $skipped_files
+ } elseif {$i == 4} {
+ quantify_run 0 $i {-no_cuts} 2.0 4 3 ${html}_L4_S2_R${i} ${results}${i} $group_4_checks ${results}[expr $i-1] $skipped_files
+ } elseif {$i == 5} {
+# quantify_run 0 $i {-no_cuts} 4.0 4 3 ${html}_L4_S4_R${i} ${results}${i} $group_5_checks ${results}[expr $i-1] $skipped_files
+ quantify_run 0 $i {} 6.0 4 3 ${html}_L4_S4_R${i} ${results}${i} $group_5_checks ${results}[expr $i-1] $skipped_files
+ } elseif {($i == 6) && ("CFG_F" in $defines || "CFG_ZFINX" in $defines)} {
+ quantify_run 0 $i {-no_cuts} 4.0 4 3 ${html}_L4_S4_R${i} ${results}${i} $group_6_checks ${results}[expr $i-1] {}
+ }
+ stop_message_log
+# }
+
+ } elseif {$pve_mode eq "DPM"} {
+
+ if {("CFG_F" in $defines || "CFG_ZFINX" in $defines)} {
+ set i 7
+ } else {
+ set i 6
+ }
+
+ start_message_log ${log}${i}.log
+# quantify_run 0 $i {-no_cuts} 4.0 4 3 ${html}_L4_S4_R${i} ${results}${i} $group_5_checks {} $skipped_files
+# file copy -force ${cfg_dir}/DEF/QTF/qtf_results_${cfg}_DEF_R[expr $i-1] ${cfg_dir}/DEF/QTF/qtf_results_${cfg}_DEF_R[expr $i-1]-Xr
+# fileutil::updateInPlace ${cfg_dir}/DEF/QTF/qtf_results_${cfg}_DEF_R[expr $i-1] [list string map [list " Xr" " U0"]]
+# quantify_run 0 $i {-no_cuts} 4.0 4 3 ${html}_L4_S4_R${i} ${results}${i} $group_5_checks ${cfg_dir}/DEF/QTF/qtf_results_${cfg}_DEF_R[expr $i-1] $skipped_files
+ quantify_run 0 $i {} 6.0 4 3 ${html}_L4_S4_R${i} ${results}${i} $group_5_checks ${cfg_dir}/DEF/QTF/qtf_results_${cfg}_DEF_R[expr $i-1] $skipped_files
+ stop_message_log
+
+ } elseif {$pve_mode eq "DPF"} {
+
+ set i 8
+
+ start_message_log ${log}${i}.log
+# quantify_run 0 $i -no_cuts 2.0 4 3 ${html}_L4_S4_R${i} ${results}${i} $group_6_checks {} {}
+# file copy -force ${cfg_dir}/DPM/QTF/qtf_results_${cfg}_DPM_R[expr $i-1] ${cfg_dir}/DPM/QTF/qtf_results_${cfg}_DPM_R[expr $i-1]-Xr
+# fileutil::updateInPlace ${cfg_dir}/DPM/QTF/qtf_results_${cfg}_DPM_R[expr $i-1] [list string map [list " Xr" " U0"]]
+ quantify_run 0 $i -no_cuts 2.0 4 3 ${html}_L4_S4_R${i} ${results}${i} $group_6_checks ${cfg_dir}/DPM/QTF/qtf_results_${cfg}_DPM_R[expr $i-1] {}
+ stop_message_log
+
+ }
+
+}
+
+if {$app eq "VCI"} {
+
+ set_check_option -prover_exec_order { { disprover1 disprover3 } } -disprover1_steps 20 -disprover3_steps 20
+
+ set output_dir "${app_dir}/qtf_coverage_${cfg}_${pve_mode}"
+ set checks "[set ${pve_mode}_checks]"
+ set results "${cfg_dir}/${pve_mode}/QTF/qtf_results_${cfg}_${pve_mode}_R"
+ set log "${app_dir}/${app}_${cfg}_${pve_mode}"
+
+ if {$pve_mode eq "DEF"} {
+ if {("CFG_F" in $defines || "CFG_ZFINX" in $defines)} {
+ set i 6
+ } else {
+ set i 5
+ }
+ } elseif {$pve_mode eq "DPM"} {
+ if {("CFG_F" in $defines || "CFG_ZFINX" in $defines)} {
+ set i 7
+ } else {
+ set i 6
+ }
+ } elseif {$pve_mode eq "DPF"} {
+ set i 8
+ }
+
+ start_message_log ${log}.log
+ puts "\n-INFO- Launching VCI Command::\nexport_quantify_coverage -call_script t.sh -generate_flist -output_dir $output_dir -checks $checks ${results}${i}\n"
+ export_quantify_coverage -call_script t.sh -generate_flist -output_dir $output_dir -checks $checks ${results}${i}
+ stop_message_log
+# report_quantify_result -quantify_result qtf_results_run_${run} -html html_results_run_${run}
+
+}
diff --git a/scripts/riscv_isa_formal/common/setup_mv.tcl b/scripts/riscv_isa_formal/common/setup_mv.tcl
new file mode 100755
index 000000000..021a6a430
--- /dev/null
+++ b/scripts/riscv_isa_formal/common/setup_mv.tcl
@@ -0,0 +1,24 @@
+# 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.
+
+if {![info exists ::env(DESIGN_RTL_DIR)]} {
+ set ::env(DESIGN_RTL_DIR) [pwd]/rtl
+}
+set_read_hdl_option -verilog_version sv2012 -pragma_ignore {translate_}
+vlog -sv -f cv32e40p_fpu_manifest.flist
+elaborate
+compile
+set_mode mv
diff --git a/scripts/riscv_isa_formal/common/t.sh b/scripts/riscv_isa_formal/common/t.sh
new file mode 100755
index 000000000..fe536fc63
--- /dev/null
+++ b/scripts/riscv_isa_formal/common/t.sh
@@ -0,0 +1,28 @@
+#!/bin/bash
+#
+# 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.
+
+# This script is a template representing a customization to integrate OneSpin 360 with VCS simulator
+#
+# onespin calls the script as follows:
+# template_vcs_flow.sh
+#
+# In this script you need to set up the environment for the simulator,
+#
+ARG1=$1
+
+vsim -64 -c -do "source ${ARG1}; quit -f"
diff --git a/scripts/riscv_isa_formal/common/vips/obi_dmem.sv b/scripts/riscv_isa_formal/common/vips/obi_dmem.sv
new file mode 100755
index 000000000..8f155c2b4
--- /dev/null
+++ b/scripts/riscv_isa_formal/common/vips/obi_dmem.sv
@@ -0,0 +1,76 @@
+// 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.
+
+///////////////////////////////////////////////////////////////////////////////////////////////////////////////
+// //
+// General remarks: //
+// //
+// Just replace below with the name of the module you want to connect the VIP to //
+// and add the appropriate parameter values and DUT signals in braces. //
+// //
+// Leave unused signals (and parameters that just have the default value) simply unconnected //
+// because optional signals are pulled up/down appropriately in the checker file. //
+// //
+// The VIP uses an active LOW reset. //
+// If your DUT reset signal, called "rst", is active high, use "!rst" in the instantiation //
+// //
+// For external interfaces (bus signals are primary inputs/outputs), set parameter ASSUME=1. //
+// In that case, make sure MASTER=1 in case the DUT is the bus master (driving the address signal output), //
+// or MASTER=0 in case the DUT is the bus slave (address signal is input). //
+// //
+// In case you instantiate the VIP several times for different interfaces in the DUT, //
+// make sure to pick individual instance names (line with comment "non-ambiguous instance name" below) //
+// //
+///////////////////////////////////////////////////////////////////////////////////////////////////////////////
+
+bind cv32e40p_core obi_checker #(
+ .ADDR_WIDTH (), // (default 32) number of bits in addr
+ .DATA_WIDTH (), // (default 32) number of bits in wdata, rdata
+ .ASSUME (1), // (default 0) switch to create assumes
+ .MASTER (1), // (default 0) switch to select master/slave side (when switched off, i.e., slave side, important in case of ASSUME)
+ .ASSERT_ON (), // (default 1) switch to generate assertions,
+ // useful to switch off (ASSERT_ON=0) together with ASSUME=1 just to constrain a block for Inspect
+ .COVER_ON (), // (default 1) switch to additionally generate cover statements
+ .X_CHECKING_ON(), // (default 0) switch to create no-X assertions (to be used in conjunction with x_checking_setup)
+ .LIVENESS_ON (), // (default 0) switch to create liveness assertions
+ .MAX_WAIT (`RESTRICT_DMEM_STALL_CYCLES), // (default $) number of cycles for waiting period checks (for creating liveness checks in case LIVENESS_ON=1)
+ .AUSER_WIDTH (), // (default 32) number of bits in auser (if used)
+ .WUSER_WIDTH (), // (default 32) number of bits in wuser (if used)
+ .RUSER_WIDTH (), // (default 32) number of bits in ruser (if used)
+ .ID_WIDTH (), // (default 32) number of bits in aid, rid (if used)
+ .MAX_OUTSTANDING_TRANSACTIONS(), // (default 2) maximum number of outstanding transactions in the system
+ .RESPONSE_PREDICTOR(1) // (default 0) switch to introduce a signal to predict the response at the beginning of the data phase
+) obi_dmem_checker ( // non-ambiguous instance name
+ .clk (clk_i), // required
+ .reset_n(rst_ni), // required
+// Address channel
+ .req (data_req_o), // required
+ .gnt (data_gnt_i), // required
+ .addr (data_addr_o), // required /*ADDRESS*/
+ .we (data_we_o), // optional, default is 1'b0
+ .be (data_be_o), // optional, default is '1
+ .wdata (data_wdata_o), // required /*DATA*/
+ .auser (), // optional, default is '0
+ .wuser (), // optional, default is '0
+ .aid (), // optional, default is '0
+// Response channel
+ .rvalid (data_rvalid_i), // required
+ .rready (), // optional, default is 1'b1
+ .rdata (data_rdata_i), // required /*DATA*/
+ .err (), // optional, default is 1'b0
+ .ruser (), // optional, default is '0
+ .rid () // optional, default is '0
+);
diff --git a/scripts/riscv_isa_formal/common/vips/obi_imem.sv b/scripts/riscv_isa_formal/common/vips/obi_imem.sv
new file mode 100755
index 000000000..38bc2f884
--- /dev/null
+++ b/scripts/riscv_isa_formal/common/vips/obi_imem.sv
@@ -0,0 +1,75 @@
+// 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.
+
+///////////////////////////////////////////////////////////////////////////////////////////////////////////////
+// //
+// General remarks: //
+// //
+// Just replace below with the name of the module you want to connect the VIP to //
+// and add the appropriate parameter values and DUT signals in braces. //
+// //
+// Leave unused signals (and parameters that just have the default value) simply unconnected //
+// because optional signals are pulled up/down appropriately in the checker file. //
+// //
+// The VIP uses an active LOW reset. //
+// If your DUT reset signal, called "rst", is active high, use "!rst" in the instantiation //
+// //
+// For external interfaces (bus signals are primary inputs/outputs), set parameter ASSUME=1. //
+// In that case, make sure MASTER=1 in case the DUT is the bus master (driving the address signal output), //
+// or MASTER=0 in case the DUT is the bus slave (address signal is input). //
+// //
+// In case you instantiate the VIP several times for different interfaces in the DUT, //
+// make sure to pick individual instance names (line with comment "non-ambiguous instance name" below) //
+// //
+///////////////////////////////////////////////////////////////////////////////////////////////////////////////
+
+bind cv32e40p_core obi_checker #(
+ .ADDR_WIDTH (), // (default 32) number of bits in addr
+ .DATA_WIDTH (), // (default 32) number of bits in wdata, rdata
+ .ASSUME (1), // (default 0) switch to create assumes
+ .MASTER (1), // (default 0) switch to select master/slave side (when switched off, i.e., slave side, important in case of ASSUME)
+ .ASSERT_ON (), // (default 1) switch to generate assertions,
+ // useful to switch off (ASSERT_ON=0) together with ASSUME=1 just to constrain a block for Inspect
+ .COVER_ON (), // (default 1) switch to additionally generate cover statements
+ .X_CHECKING_ON(), // (default 0) switch to create no-X assertions (to be used in conjunction with x_checking_setup)
+ .LIVENESS_ON (), // (default 0) switch to create liveness assertions
+ .MAX_WAIT (), // (default $) number of cycles for waiting period checks (for creating liveness checks in case LIVENESS_ON=1)
+ .AUSER_WIDTH (), // (default 32) number of bits in auser (if used)
+ .WUSER_WIDTH (), // (default 32) number of bits in wuser (if used)
+ .RUSER_WIDTH (), // (default 32) number of bits in ruser (if used)
+ .ID_WIDTH (), // (default 32) number of bits in aid, rid (if used)
+ .MAX_OUTSTANDING_TRANSACTIONS() // (default 2) maximum number of outstanding transactions in the system
+) obi_imem_checker ( // non-ambiguous instance name
+ .clk (clk_i), // required
+ .reset_n(rst_ni), // required
+// Address channel
+ .req (instr_req_o), // required
+ .gnt (instr_gnt_i), // required
+ .addr (instr_addr_o), // required /*ADDRESS*/
+ .we (), // optional, default is 1'b0
+ .be (), // optional, default is '1
+ .wdata ('0), // required /*DATA*/
+ .auser (), // optional, default is '0
+ .wuser (), // optional, default is '0
+ .aid (), // optional, default is '0
+// Response channel
+ .rvalid (instr_rvalid_i), // required
+ .rready (), // optional, default is 1'b1
+ .rdata (instr_rdata_i), // required /*DATA*/
+ .err (), // optional, default is 1'b0
+ .ruser (), // optional, default is '0
+ .rid () // optional, default is '0
+);
diff --git a/scripts/riscv_isa_formal/launch_command example b/scripts/riscv_isa_formal/launch_command example
new file mode 100755
index 000000000..6b7f3a0a3
--- /dev/null
+++ b/scripts/riscv_isa_formal/launch_command example
@@ -0,0 +1,58 @@
+# Setup tool and licenses
+#source SourceMe
+
+set instructions="v1_8_0"; set name_cmd="NAME=${instructions} ;
+
+set config=XP ; set config_cmd="CONF=${config}"
+set config=XPF0 ; set config_cmd="CONF=${config}"
+set config=XPF1 ; set config_cmd="CONF=${config}"
+set config=XPF2 ; set config_cmd="CONF=${config}"
+set config=XPZF0 ; set config_cmd="CONF=${config}"
+set config=XPZF1 ; set config_cmd="CONF=${config}"
+set config=XPZF2 ; set config_cmd="CONF=${config}"
+
+set app=PRC ; set app_cmd="APP=${app}"
+set app=QTF ; set app_cmd="APP=${app}"
+set app=VCI ; set app_cmd="APP=${app}"
+
+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)
+set prepare=""
+set prepare="PREPARE=1"
+
+set verbose=""
+set verbose="VERBOSE=1"
+
+set timeout=""
+set timeout="DBG=1800"
+
+# Interactive or batch run on local server
+set gui="gui" ; set gui_cmd="GUI=1"
+set gui="batch" ; set gui_cmd=""
+
+set my_time = `date '+%Y-%m-%d-%Hh%Mm%Ss'` ; set logname=run_${gui}-${app}-cfg_${config}-mode_${mode}-${instructions}-${my_time}.log ; echo "\n vi ${logname}\n" ; \
+echo "make ${gui_cmd} ${app_cmd} ${config_cmd} ${mode_cmd} ${name_cmd} ${verbose} ${prepare} ${timeout} all\n" > ${logname} && echo "" >>& ${logname} ; \
+/usr/bin/time make ${gui_cmd} ${app_cmd} ${config_cmd} ${mode_cmd} ${name_cmd} ${verbose} ${prepare} ${timeout} all >> & ! ${logname} &
+
+# Interactive or batch run on compute farm server using LSF
+set gui="lsf" ; set gui_cmd="" ; set queue="long"
+set gui="lsf_gui" ; set gui_cmd="GUI=1" ; set queue="gui -XF"
+set gui="lsf_gui" ; set gui_cmd="GUI=1" ; set queue="gui -XF -Is -tty"
+
+set nb_cpus="1"
+set nb_cpus="2"
+set nb_cpus="4"
+set nb_cpus="8"
+set nb_cpus="12"
+set nb_cpus="16"
+set nb_cpus="24"
+set nb_cpus="32"
+set nb_cpus="36"
+set nb_cpus="48"
+
+set my_time = `date '+%Y-%m-%d-%Hh%Mm%Ss'` ; set logname=run_${gui}-${app}-cfg_${config}-mode_${mode}-${instructions}-${my_time}.log ; echo "\n vi ${logname}\n" ; \
+echo "make ${gui_cmd} ${app_cmd} ${config_cmd} ${mode_cmd} ${name_cmd} ${verbose} ${prepare} ${timeout} all\n" > ${logname} && echo "" >>& ${logname} ; \
+bsub -J ${app}-cfg_${config}-mode_${mode}-${instructions} -P cv32e40p -q ${queue} -oo ${logname} -n ${nb_cpus} -R "select[cpuf>=15.0] span[hosts=1] rusage[mem=64G]" make ${gui_cmd} ${app_cmd} ${config_cmd} ${mode_cmd} ${name_cmd} ${verbose} ${prepare} ${timeout} all