From c3e86fc81a068ca48094d55b6567f42e9400d2ea Mon Sep 17 00:00:00 2001 From: Pascal Gouedo Date: Thu, 6 Jun 2024 17:27:08 +0200 Subject: [PATCH] RISC-V ISA Formal Verification files for SiemensEDA OneSpin tool. Signed-off-by: Pascal Gouedo --- scripts/riscv_isa_formal/Makefile | 59 ++ scripts/riscv_isa_formal/README.md | 50 ++ .../riscv_isa_formal/common/constraints.sv | 119 ++++ .../riscv_isa_formal/common/core_checker.sv | 21 + scripts/riscv_isa_formal/common/io.sv | 72 +++ .../riscv_isa_formal/common/other_bindings.sv | 72 +++ scripts/riscv_isa_formal/common/setup.tcl | 564 ++++++++++++++++++ scripts/riscv_isa_formal/common/setup_mv.tcl | 8 + scripts/riscv_isa_formal/common/t.sh | 12 + .../riscv_isa_formal/common/vips/obi_dmem.sv | 60 ++ .../riscv_isa_formal/common/vips/obi_imem.sv | 59 ++ .../riscv_isa_formal/launch_command example | 58 ++ 12 files changed, 1154 insertions(+) create mode 100755 scripts/riscv_isa_formal/Makefile create mode 100755 scripts/riscv_isa_formal/README.md create mode 100755 scripts/riscv_isa_formal/common/constraints.sv create mode 100755 scripts/riscv_isa_formal/common/core_checker.sv create mode 100755 scripts/riscv_isa_formal/common/io.sv create mode 100755 scripts/riscv_isa_formal/common/other_bindings.sv create mode 100755 scripts/riscv_isa_formal/common/setup.tcl create mode 100755 scripts/riscv_isa_formal/common/setup_mv.tcl create mode 100755 scripts/riscv_isa_formal/common/t.sh create mode 100755 scripts/riscv_isa_formal/common/vips/obi_dmem.sv create mode 100755 scripts/riscv_isa_formal/common/vips/obi_imem.sv create mode 100755 scripts/riscv_isa_formal/launch_command example 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..84ab2f05e --- /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 EDA Onespin 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 EDA OneSpin customers. +> Once OneSpin 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..02bf694d0 --- /dev/null +++ b/scripts/riscv_isa_formal/common/constraints.sv @@ -0,0 +1,119 @@ +/*********************/ +// 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..74755ca9f --- /dev/null +++ b/scripts/riscv_isa_formal/common/core_checker.sv @@ -0,0 +1,21 @@ +/////////////////////////////////////////////////////////////////////////////// +// // +// RISC-V Checker // +// // +// This material contains trade secrets or otherwise confidential // +// information owned by Siemens Industry Software Inc. or its affiliates // +// (collectively, "SISW"), or its licensors. Access to and use of this // +// information is strictly limited as set forth in the Customer's applicable // +// agreements with SISW. // +// // +// This material may not be copied, distributed, or otherwise disclosed // +// outside of the Customer's facilities without the express written // +// permission of SISW, and may not be used in any way not expressly // +// authorized by SISW. // +// // +/////////////////////////////////////////////////////////////////////////////// + + + + +This file is available only to Siemens EDA OneSpin 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..cb7c9c1e2 --- /dev/null +++ b/scripts/riscv_isa_formal/common/io.sv @@ -0,0 +1,72 @@ + // 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..41c929d20 --- /dev/null +++ b/scripts/riscv_isa_formal/common/other_bindings.sv @@ -0,0 +1,72 @@ + // 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..0bcce5472 --- /dev/null +++ b/scripts/riscv_isa_formal/common/setup.tcl @@ -0,0 +1,564 @@ +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 + report_result -details + cd $app_dir + 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 + report_result -details + cd $app_dir + save_database -force round_[expr $nb_round + 1] + cd $cwd + } + + report_result -signoff -details + +# 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..84eb4523c --- /dev/null +++ b/scripts/riscv_isa_formal/common/setup_mv.tcl @@ -0,0 +1,8 @@ +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..eca98e09f --- /dev/null +++ b/scripts/riscv_isa_formal/common/t.sh @@ -0,0 +1,12 @@ +#!/bin/bash +# +# 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..7ca5866e2 --- /dev/null +++ b/scripts/riscv_isa_formal/common/vips/obi_dmem.sv @@ -0,0 +1,60 @@ +/////////////////////////////////////////////////////////////////////////////////////////////////////////////// +// // +// 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..126152246 --- /dev/null +++ b/scripts/riscv_isa_formal/common/vips/obi_imem.sv @@ -0,0 +1,59 @@ +/////////////////////////////////////////////////////////////////////////////////////////////////////////////// +// // +// 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