From f6bd677ca1523387e00762e02b26ec7589ec4135 Mon Sep 17 00:00:00 2001 From: Yoann Pruvost Date: Fri, 31 May 2024 16:41:28 +0800 Subject: [PATCH] Uploading formal work related to code coverage analysis --- scripts/formal/Makefile | 54 ++++++ scripts/formal/README.md | 24 +++ scripts/formal/cv32e40p_formal.flist | 33 ++++ scripts/formal/formal.do | 37 ++++ scripts/formal/src/cv32e40p_EX_assert.sv | 74 ++++++++ scripts/formal/src/cv32e40p_ID_assert.sv | 46 +++++ scripts/formal/src/cv32e40p_assert.sv | 124 +++++++++++++ scripts/formal/src/cv32e40p_bind.sv | 117 +++++++++++++ scripts/formal/src/cv32e40p_formal_top.sv | 93 ++++++++++ scripts/formal/src/data_assert.sv | 74 ++++++++ scripts/formal/src/debug_assert.sv | 46 +++++ .../formal/src/fpnew_divsqrt_th_32_assert.sv | 42 +++++ scripts/formal/src/insn_assert.sv | 165 ++++++++++++++++++ scripts/formal/src/interrupt_assert.sv | 46 +++++ 14 files changed, 975 insertions(+) create mode 100644 scripts/formal/Makefile create mode 100644 scripts/formal/README.md create mode 100644 scripts/formal/cv32e40p_formal.flist create mode 100644 scripts/formal/formal.do create mode 100644 scripts/formal/src/cv32e40p_EX_assert.sv create mode 100644 scripts/formal/src/cv32e40p_ID_assert.sv create mode 100644 scripts/formal/src/cv32e40p_assert.sv create mode 100644 scripts/formal/src/cv32e40p_bind.sv create mode 100644 scripts/formal/src/cv32e40p_formal_top.sv create mode 100644 scripts/formal/src/data_assert.sv create mode 100644 scripts/formal/src/debug_assert.sv create mode 100644 scripts/formal/src/fpnew_divsqrt_th_32_assert.sv create mode 100644 scripts/formal/src/insn_assert.sv create mode 100644 scripts/formal/src/interrupt_assert.sv diff --git a/scripts/formal/Makefile b/scripts/formal/Makefile new file mode 100644 index 000000000..bff46da6f --- /dev/null +++ b/scripts/formal/Makefile @@ -0,0 +1,54 @@ +# Copyright 2024 Dolphin Design +# 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. + +################################################################################## +# # +# Contributors: Yoann Pruvost, Dolphin Design # +# # +# Description: Makefile for CV32E40P Formal code analysis # +# # +################################################################################## + +export DESIGN_RTL_DIR = ../../rtl + +create_lib: + rm -rf work + vlib work + +compile_design: create_lib + vlog -sv -f ../../cv32e40p_fpu_manifest.flist + vlog -sv -mfcu -cuname cv32e40p_bind -f cv32e40p_formal.flist + +compile_design_pulp: create_lib + vlog -sv +define+PULP -f ../../cv32e40p_fpu_manifest.flist + vlog -sv +define+PULP -mfcu -cuname cv32e40p_bind -f cv32e40p_formal.flist + +compile_design_pulp_f0: create_lib + vlog -sv +define+PULP_F0 -f ../../cv32e40p_fpu_manifest.flist + vlog -sv +define+PULP_F0 -mfcu -cuname cv32e40p_bind -f cv32e40p_formal.flist + +run: compile_design + qverify -c -do formal.do + +run_pulp: compile_design_pulp + qverify -c -do formal.do + +run_pulp_F0: compile_design_pulp_f0 + qverify -c -do formal.do + +clean: + qverify_clean + rm -rf work \ No newline at end of file diff --git a/scripts/formal/README.md b/scripts/formal/README.md new file mode 100644 index 000000000..aa91fab6a --- /dev/null +++ b/scripts/formal/README.md @@ -0,0 +1,24 @@ +## CV32E40P Formal + + This folder contains the source and scripts used in the effort to justify waived code coverage holes using formal tools. + + Disclaimer: This has been developped and tested with Siemens Questa formal and the Makefile only support this tool. Porting to other tools should be straightforward as all source files are standard sva. + +### Introduction + To assist code coverage analysis we formally proved that some code was in our case unreachable. Each assertion correspond to one coverage holes. We tried to keep the constraints as minimal as possible. The only constraints we are using are: + - OBI protocol constraints on both instructions and data interfaces + - Disabling scan + + +### How to use + +Inside this folder, with ```vlog``` and ```qverify``` available in your PATH, run one of the following command. + +| Command | Description | +|-----------------|-----------------------------------------------| +|make run | Run default config (no corev_pulp, no FPU) | +|make run_pulp | Run config corev_pulp withou FPU | +|make run_pulp_F0 | Run config corev_pulp with FPU with latency 0 | +|make clean | Remove all temporary file | + +All runs are in batch. At the end of the run, use ```qverify ``` to open the results in GUI. \ No newline at end of file diff --git a/scripts/formal/cv32e40p_formal.flist b/scripts/formal/cv32e40p_formal.flist new file mode 100644 index 000000000..e3c5f1f2a --- /dev/null +++ b/scripts/formal/cv32e40p_formal.flist @@ -0,0 +1,33 @@ +// Copyright 2024 Dolphin Design +// 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. + +//////////////////////////////////////////////////////////////////////////////////// +// // +// Contributors: Yoann Pruvost, Dolphin Design // +// // +// Description: Filelist for CV32E40P formal code analysis // +// // +//////////////////////////////////////////////////////////////////////////////////// + ++incdir+./src +src/insn_assert.sv +src/data_assert.sv +src/cv32e40p_assert.sv +src/cv32e40p_ID_assert.sv +src/cv32e40p_EX_assert.sv +src/fpnew_divsqrt_th_32_assert.sv +src/cv32e40p_formal_top.sv +src/cv32e40p_bind.sv \ No newline at end of file diff --git a/scripts/formal/formal.do b/scripts/formal/formal.do new file mode 100644 index 000000000..8e0be6031 --- /dev/null +++ b/scripts/formal/formal.do @@ -0,0 +1,37 @@ +// Copyright 2024 Dolphin Design +// 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. + +//////////////////////////////////////////////////////////////////////////////////// +// // +// Contributors: Yoann Pruvost, Dolphin Design // +// // +// Description: Formal script for CV32E40P // +// // +//////////////////////////////////////////////////////////////////////////////////// + +set top cv32e40p_formal_top + +#netlist clock clk_i -period 50 + +#netlist constraint rst_ni -value 1'b1 -after_init + +#netlist port domain i_lint_grnt -clock i_clk + +formal compile -d cv32e40p_formal_top -cuname cv32e40p_bind + +formal verify -timeout 100m -jobs 4 -sanity_waveforms + +#exit diff --git a/scripts/formal/src/cv32e40p_EX_assert.sv b/scripts/formal/src/cv32e40p_EX_assert.sv new file mode 100644 index 000000000..6a04b7629 --- /dev/null +++ b/scripts/formal/src/cv32e40p_EX_assert.sv @@ -0,0 +1,74 @@ +// Copyright 2024 Dolphin Design +// 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. + +//////////////////////////////////////////////////////////////////////////////////// +// // +// Contributors: Yoann Pruvost, Dolphin Design // +// // +// Description: Assertion for unreachable code in CV32E40P EX stage // +// // +//////////////////////////////////////////////////////////////////////////////////// + +module cv32e40p_EX_assert import cv32e40p_pkg::*; +( + input logic clk_i, + input logic rst_ni, + + input logic apu_valid , + input logic apu_singlecycle , + input logic apu_multicycle , + input logic regfile_alu_we_i, + input logic apu_en_i , + input logic regfile_we_lsu , + input logic apu_rvalid_i , + input logic apu_rvalid_q , + + input logic data_misaligned_i , + input logic data_misaligned_ex_i , + input logic data_req_i , + input logic data_rvalid_i , + input logic mulh_active , + input mul_opcode_e mult_operator_i , + input logic [ 1:0] ctrl_transfer_insn_in_dec_i, + input logic apu_read_dep_for_jalr_o +); + + property unreachable_ex_211; + @(posedge clk_i) disable iff(!rst_ni) + (apu_valid & (apu_singlecycle | apu_multicycle)) |-> !(apu_en_i & regfile_alu_we_i); + endproperty + + property unreachable_ex_237; + @(posedge clk_i) disable iff(!rst_ni) + regfile_we_lsu |-> !(~apu_valid & (!apu_singlecycle & !apu_multicycle)); + endproperty + + property unreachable_ex_387; + @(posedge clk_i) disable iff(!rst_ni) + ((apu_rvalid_i && apu_multicycle) && ~(((ctrl_transfer_insn_in_dec_i == 2) && regfile_alu_we_i) && ~apu_read_dep_for_jalr_o) && ~((data_misaligned_i || data_misaligned_ex_i) || ((data_req_i || data_rvalid_i) && regfile_alu_we_i)) && mulh_active)|-> mult_operator_i == MUL_H; + endproperty + + property unreachable_ex_396; + @(posedge clk_i) disable iff(!rst_ni) + (apu_rvalid_q && ~(( ~apu_read_dep_for_jalr_o && (ctrl_transfer_insn_in_dec_i==2)) && regfile_alu_we_i) && ~((data_misaligned_i || data_misaligned_ex_i) || ((data_req_i || data_rvalid_i) && regfile_alu_we_i)) && mulh_active) |-> mult_operator_i == MUL_H; + endproperty + + assert_unreachable_ex_211: assert property(unreachable_ex_211); + assert_unreachable_ex_237: assert property(unreachable_ex_237); + assert_unreachable_ex_387: assert property(unreachable_ex_387); + assert_unreachable_ex_396: assert property(unreachable_ex_396); + +endmodule \ No newline at end of file diff --git a/scripts/formal/src/cv32e40p_ID_assert.sv b/scripts/formal/src/cv32e40p_ID_assert.sv new file mode 100644 index 000000000..1a6b58cf3 --- /dev/null +++ b/scripts/formal/src/cv32e40p_ID_assert.sv @@ -0,0 +1,46 @@ +// Copyright 2024 Dolphin Design +// 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. + +//////////////////////////////////////////////////////////////////////////////////// +// // +// Contributors: Yoann Pruvost, Dolphin Design // +// // +// Description: Assertion for unreachable code in CV32E40P ID stage // +// // +//////////////////////////////////////////////////////////////////////////////////// + +module cv32e40p_ID_assert import cv32e40p_pkg::*; +( + input logic clk_i, + input logic rst_ni, + + input logic [31:0] instr_rdata_i, + input logic is_compressed_id_i, + + input logic [ 2:0] alu_op_a_mux_sel, + input logic [ 2:0] alu_op_b_mux_sel, + input logic [ 1:0] alu_op_c_mux_sel, + input logic alu_bmask_b_mux_sel, + input logic [ 1:0] ctrl_transfer_target_mux_sel +); + + property unreachable_id_872; + @(posedge clk_i) disable iff(!rst_ni) + (alu_op_c_mux_sel == OP_C_REGC_OR_FWD) && (~(alu_op_b_mux_sel == OP_B_BMASK) && ((alu_op_a_mux_sel != OP_A_REGC_OR_FWD) && (ctrl_transfer_target_mux_sel != JT_JALR)) && ~alu_bmask_b_mux_sel) |-> alu_op_b_mux_sel == OP_B_IMM; + endproperty + + assert_unreachable_id_872: assert property(unreachable_id_872); +endmodule \ No newline at end of file diff --git a/scripts/formal/src/cv32e40p_assert.sv b/scripts/formal/src/cv32e40p_assert.sv new file mode 100644 index 000000000..610ad3940 --- /dev/null +++ b/scripts/formal/src/cv32e40p_assert.sv @@ -0,0 +1,124 @@ +// Copyright 2024 Dolphin Design +// 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. + +//////////////////////////////////////////////////////////////////////////////////// +// // +// Contributors: Yoann Pruvost, Dolphin Design // +// Pascal Gouedo, Dolphin Design // +// // +// Description: GLobal assume and assert for CV32E40P formal code analysis // +// // +//////////////////////////////////////////////////////////////////////////////////// + + +module cv32e40p_assert import cv32e40p_pkg::*; +( + input logic clk_i, + input logic rst_ni, + input logic scan_cg_en_i, + + input logic [31:0] boot_addr_i, + input logic [31:0] mtvec_addr_i, + input logic [31:0] hart_id_i, + input logic [31:0] dm_halt_addr_i, + input logic [31:0] dm_exception_addr_i, + + input logic [1:0] data_type_ex_i, + + input logic [31:0] pc_id_i, + + // Taken from controller + input ctrl_state_e ctrl_fsm_cs, + input logic is_hwlp_body, + input logic hwlp_end0_eq_pc, + input logic hwlp_counter0_gt_1, + input logic hwlp_end1_eq_pc, + input logic hwlp_counter1_gt_1, + input logic jump_done_q +); + import cv32e40p_tracer_pkg::*; + + /********** + * Assume * + **********/ + property no_scan; + @(posedge clk_i) disable iff(!rst_ni) + scan_cg_en_i == '0; + endproperty + + property hart_id_0; + @(posedge clk_i) disable iff(!rst_ni) + hart_id_i == '0; + endproperty + + property aligned_boot_address; + @(posedge clk_i) disable iff(!rst_ni) + boot_addr_i == 32'h1000_0000; + endproperty + + property aligned_mtvec_address; + @(posedge clk_i) disable iff(!rst_ni) + mtvec_addr_i == 32'h2000_0000; + endproperty + + property aligned_halt_address; + @(posedge clk_i) disable iff(!rst_ni) + dm_halt_addr_i == 32'h3000_0000; + endproperty + + property aligned_exception_address; + @(posedge clk_i) disable iff(!rst_ni) + dm_exception_addr_i == 32'h4000_0000; + endproperty + + /********** + * Assert * + **********/ + property data_type_ex_never_11; + @(posedge clk_i) disable iff(!rst_ni) + data_type_ex_i != 2'b11; + endproperty + + property never_jump_done_q_when_hwlp_body_and_hwlp_end0_eq_pc_and_hwlp_counter0_gt_1; + @(posedge clk_i) disable iff(!rst_ni) + (ctrl_fsm_cs == DECODE) & is_hwlp_body & hwlp_end0_eq_pc & hwlp_counter0_gt_1 |-> ~jump_done_q; + endproperty + + property never_ret_from_int_ecall_ebreak_exceptions_on_HWLoop1_last_inst_with_HWLoop1_counter_not_gt1; + @(posedge clk_i) disable iff(!rst_ni) + (ctrl_fsm_cs == DECODE) & is_hwlp_body |-> ~(hwlp_end1_eq_pc & hwlp_counter1_gt_1); + endproperty + + property pc_id_aligned; + @(posedge clk_i) disable iff(!rst_ni) + pc_id_i[2:0] != 2'b00; + endproperty + + + + assume_no_scan: assume property(no_scan); + // assume_hart_id_0: assume property(hart_id_0); + // assume_aligned_boot_address: assume property(aligned_boot_address); + // asuume_aligned_mtvec_address: assume property(aligned_mtvec_address); + // assume_aligned_halt_address: assume property(aligned_halt_address); + // assume_aligned_exception_address: assume property(aligned_exception_address); + + assert_data_type_ex_never_11: assert property(data_type_ex_never_11); + // assert_never_jump_done_q_when_hwlp_body_and_hwlp_end0_eq_pc_and_hwlp_counter0_gt_1: assert property(never_jump_done_q_when_hwlp_body_and_hwlp_end0_eq_pc_and_hwlp_counter0_gt_1); + // assert_never_ret_from_int_ecall_ebreak_exceptions_on_HWLoop1_last_inst_with_HWLoop1_counter_not_gt1: assert property(never_ret_from_int_ecall_ebreak_exceptions_on_HWLoop1_last_inst_with_HWLoop1_counter_not_gt1); + // assert_pc_id_aligned: assert property(pc_id_aligned); + +endmodule \ No newline at end of file diff --git a/scripts/formal/src/cv32e40p_bind.sv b/scripts/formal/src/cv32e40p_bind.sv new file mode 100644 index 000000000..38d51941a --- /dev/null +++ b/scripts/formal/src/cv32e40p_bind.sv @@ -0,0 +1,117 @@ +// Copyright 2024 Dolphin Design +// 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. + +//////////////////////////////////////////////////////////////////////////////////// +// // +// Contributors: Yoann Pruvost, Dolphin Design // +// Pascal Gouedo, Dolphin Design // +// // +// Description: CV32E40P binding for formal code analysis // +// // +//////////////////////////////////////////////////////////////////////////////////// + +bind cv32e40p_formal_top insn_assert u_insn_assert ( + .clk_i(clk_i), + .rst_ni(rst_ni), + + .instr_req_o (instr_req_o), + .instr_gnt_i (instr_gnt_i), + .instr_rvalid_i(instr_rvalid_i), + .instr_addr_o (instr_addr_o), + .instr_rdata_i (instr_rdata_i) +); + +bind cv32e40p_formal_top data_assert u_data_assert ( + .clk_i(clk_i), + .rst_ni(rst_ni), + + .data_req_o (data_req_o ), + .data_gnt_i (data_gnt_i ), + .data_rvalid_i(data_rvalid_i), + .data_we_o (data_we_o ), + .data_be_o (data_be_o ), + .data_addr_o (data_addr_o ), + .data_wdata_o (data_wdata_o ), + .data_rdata_i (data_rdata_i ) +); + +bind cv32e40p_formal_top cv32e40p_assert u_cv32e40p_assert ( + .clk_i(clk_i), + .rst_ni(rst_ni), + .scan_cg_en_i(scan_cg_en_i), + + .boot_addr_i (boot_addr_i ), + .mtvec_addr_i (mtvec_addr_i ), + .hart_id_i (hart_id_i ), + .dm_halt_addr_i (dm_halt_addr_i ), + .dm_exception_addr_i(dm_exception_addr_i), + + .data_type_ex_i(u_cv32e40p_top.core_i.data_type_ex), + + .pc_id_i(u_cv32e40p_top.core_i.pc_id), + + //From controller + .ctrl_fsm_cs (u_cv32e40p_top.core_i.id_stage_i.controller_i.ctrl_fsm_cs ), + .is_hwlp_body (u_cv32e40p_top.core_i.id_stage_i.controller_i.is_hwlp_body ), + .hwlp_end0_eq_pc (u_cv32e40p_top.core_i.id_stage_i.controller_i.hwlp_end0_eq_pc ), + .hwlp_counter0_gt_1(u_cv32e40p_top.core_i.id_stage_i.controller_i.hwlp_counter0_gt_1), + .hwlp_end1_eq_pc (u_cv32e40p_top.core_i.id_stage_i.controller_i.hwlp_end1_eq_pc ), + .hwlp_counter1_gt_1(u_cv32e40p_top.core_i.id_stage_i.controller_i.hwlp_counter1_gt_1), + .jump_done_q (u_cv32e40p_top.core_i.id_stage_i.controller_i.jump_done_q ) +); + +bind cv32e40p_id_stage cv32e40p_ID_assert u_cv32e40p_ID_assert ( + .clk_i(clk), + .rst_ni(rst_n), + + .alu_op_a_mux_sel (alu_op_a_mux_sel ), + .alu_op_b_mux_sel (alu_op_b_mux_sel ), + .alu_op_c_mux_sel (alu_op_c_mux_sel ), + .alu_bmask_b_mux_sel (alu_bmask_b_mux_sel ), + .ctrl_transfer_target_mux_sel(ctrl_transfer_target_mux_sel) +); + +bind cv32e40p_ex_stage cv32e40p_EX_assert u_cv32e40p_EX_assert ( + .clk_i(clk), + .rst_ni(rst_n), + + .apu_valid (apu_valid ), + .apu_singlecycle (apu_singlecycle ), + .apu_multicycle (apu_multicycle ), + .regfile_alu_we_i(regfile_alu_we_i), + .apu_en_i (apu_en_i ), + .regfile_we_lsu (regfile_we_lsu ), + .apu_rvalid_i (apu_rvalid_i ), + .apu_rvalid_q (apu_rvalid_q ), + .data_misaligned_i (data_misaligned_i ), + .data_misaligned_ex_i (data_misaligned_ex_i ), + .data_req_i (data_req_i ), + .data_rvalid_i (data_rvalid_i ), + .mulh_active (mulh_active ), + .mult_operator_i (mult_operator_i ), + .ctrl_transfer_insn_in_dec_i(ctrl_transfer_insn_in_dec_i), + .apu_read_dep_for_jalr_o (apu_read_dep_for_jalr_o ) +); + +bind fpnew_divsqrt_th_32 fpnew_divsqrt_th_32_assert u_fpnew_divsqrt_th_32_assert ( + .clk_i (clk_i), + .rst_ni(rst_ni), + + .op_starting (op_starting ), + .unit_ready_q (unit_ready_q ), + .ex2_inst_wb (ex2_inst_wb ), + .ex2_inst_wb_vld_q(ex2_inst_wb_vld_q) +); diff --git a/scripts/formal/src/cv32e40p_formal_top.sv b/scripts/formal/src/cv32e40p_formal_top.sv new file mode 100644 index 000000000..5148cd76d --- /dev/null +++ b/scripts/formal/src/cv32e40p_formal_top.sv @@ -0,0 +1,93 @@ +// Copyright 2024 Dolphin Design +// 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. + +//////////////////////////////////////////////////////////////////////////////////// +// // +// Contributors: Yoann Pruvost, Dolphin Design // +// // +// Description: Formal testbench for CV32E40P // +// // +//////////////////////////////////////////////////////////////////////////////////// + +module cv32e40p_formal_top ( + // Clock and Reset + input logic clk_i, + input logic rst_ni, + + input logic pulp_clock_en_i, // PULP clock enable (only used if COREV_CLUSTER = 1) + input logic scan_cg_en_i, // Enable all clock gates for testing + + // Core ID, Cluster ID, debug mode halt address and boot address are considered more or less static + input logic [31:0] boot_addr_i, + input logic [31:0] mtvec_addr_i, + input logic [31:0] dm_halt_addr_i, + input logic [31:0] hart_id_i, + input logic [31:0] dm_exception_addr_i, + + // Instruction memory interface + output logic instr_req_o, + input logic instr_gnt_i, + input logic instr_rvalid_i, + output logic [31:0] instr_addr_o, + input logic [31:0] instr_rdata_i, + + // Data memory interface + output logic data_req_o, + input logic data_gnt_i, + input logic data_rvalid_i, + output logic data_we_o, + output logic [ 3:0] data_be_o, + output logic [31:0] data_addr_o, + output logic [31:0] data_wdata_o, + input logic [31:0] data_rdata_i, + + // Interrupt inputs + input logic [31:0] irq_i, // CLINT interrupts + CLINT extension interrupts + output logic irq_ack_o, + output logic [ 4:0] irq_id_o, + + // Debug Interface + input logic debug_req_i, + output logic debug_havereset_o, + output logic debug_running_o, + output logic debug_halted_o, + + // CPU Control Signals + input logic fetch_enable_i, + output logic core_sleep_o +); + + `ifdef PULP_F0 + parameter COREV_PULP = 1; + parameter FPU = 1; + `elsif PULP + parameter COREV_PULP = 1; + parameter FPU = 0; + `else + parameter COREV_PULP = 0; + parameter FPU = 0; + `endif + + cv32e40p_top #( + .COREV_PULP(COREV_PULP), + .FPU(FPU) + + ) u_cv32e40p_top ( + .* + ); + + +endmodule \ No newline at end of file diff --git a/scripts/formal/src/data_assert.sv b/scripts/formal/src/data_assert.sv new file mode 100644 index 000000000..1b70b660b --- /dev/null +++ b/scripts/formal/src/data_assert.sv @@ -0,0 +1,74 @@ +// Copyright 2024 Dolphin Design +// 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. + +//////////////////////////////////////////////////////////////////////////////////// +// // +// Contributors: Yoann Pruvost, Dolphin Design // +// Pascal Gouedo, Dolphin Design // +// // +// Description: OBI protocol emulation for CV32E40P data interface // +// // +//////////////////////////////////////////////////////////////////////////////////// + +module data_assert ( + input logic clk_i, + input logic rst_ni, + + // Data memory interface + input logic data_req_o, + input logic data_gnt_i, + input logic data_rvalid_i, + input logic data_we_o, + input logic [ 3:0] data_be_o, + input logic [31:0] data_addr_o, + input logic [31:0] data_wdata_o, + input logic [31:0] data_rdata_i +); + + /***************** + * Helpers logic * + *****************/ + int s_outstanding_cnt; + + always_ff @(posedge clk_i or negedge rst_ni) begin + if(!rst_ni) begin + s_outstanding_cnt <= 0; + end else if (data_req_o & data_gnt_i & data_rvalid_i) begin + s_outstanding_cnt <= s_outstanding_cnt; + end else if (data_req_o & data_gnt_i) begin + s_outstanding_cnt <= s_outstanding_cnt + 1; + end else if (data_rvalid_i) begin + s_outstanding_cnt <= s_outstanding_cnt - 1; + end + end + + /********** + * Assume * + **********/ + // Concerning lint_grnt + property no_grnt_when_no_req; + @(posedge clk_i) disable iff(!rst_ni) + !data_req_o |-> !data_gnt_i; + endproperty + + property no_rvalid_if_no_pending_req; + @(posedge clk_i) disable iff(!rst_ni) + s_outstanding_cnt < 1 |-> !data_rvalid_i; + endproperty + + assume_no_grnt_when_no_req: assume property(no_grnt_when_no_req); + assume_no_rvalid_if_no_pending_req: assume property(no_rvalid_if_no_pending_req); +endmodule diff --git a/scripts/formal/src/debug_assert.sv b/scripts/formal/src/debug_assert.sv new file mode 100644 index 000000000..0c6c6bd8c --- /dev/null +++ b/scripts/formal/src/debug_assert.sv @@ -0,0 +1,46 @@ +// Copyright 2024 Dolphin Design +// 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. + +//////////////////////////////////////////////////////////////////////////////////// +// // +// Contributors: Yoann Pruvost, Dolphin Design // +// // +// Description: Debug interface constraints // +// // +//////////////////////////////////////////////////////////////////////////////////// + +module debug_assert ( + input logic clk_i, + input logic rst_ni, + // Debug Interface + input logic debug_req_i, + input logic debug_havereset_o, + input logic debug_running_o, + input logic debug_halted_o +); + + /********** + * Assume * + **********/ + property no_debug; + @(posedge clk_i) disable iff(!rst_ni) + debug_req_i == '0; + endproperty + + // Uncomment this line to disable debug interface + // assume_no_debug: assume property(no_debug); + +endmodule \ No newline at end of file diff --git a/scripts/formal/src/fpnew_divsqrt_th_32_assert.sv b/scripts/formal/src/fpnew_divsqrt_th_32_assert.sv new file mode 100644 index 000000000..d66e15df6 --- /dev/null +++ b/scripts/formal/src/fpnew_divsqrt_th_32_assert.sv @@ -0,0 +1,42 @@ +// Copyright 2024 Dolphin Design +// 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. + +//////////////////////////////////////////////////////////////////////////////////// +// // +// Contributors: Yoann Pruvost, Dolphin Design // +// // +// Description: Assertion for unreachable code in CV32E40P div sqrt unit // +// // +//////////////////////////////////////////////////////////////////////////////////// + +module fpnew_divsqrt_th_32_assert ( + input logic clk_i, + input logic rst_ni, + + input logic op_starting , + input logic unit_ready_q , + input logic ex2_inst_wb , + input logic ex2_inst_wb_vld_q +); + + property unreachable_divsqrt_th_288; + @(posedge clk_i) disable iff(!rst_ni) + (op_starting && unit_ready_q) |-> !(ex2_inst_wb && ex2_inst_wb_vld_q); + endproperty + + assert_unreachable_divsqrt_th_288: assert property(unreachable_divsqrt_th_288); + +endmodule \ No newline at end of file diff --git a/scripts/formal/src/insn_assert.sv b/scripts/formal/src/insn_assert.sv new file mode 100644 index 000000000..ca3acdc5f --- /dev/null +++ b/scripts/formal/src/insn_assert.sv @@ -0,0 +1,165 @@ +// Copyright 2024 Dolphin Design +// 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. + +//////////////////////////////////////////////////////////////////////////////////// +// // +// Contributors: Yoann Pruvost, Dolphin Design // +// // +// Description: OBI protocol emulation for CV32E40P instruction interface // +// // +//////////////////////////////////////////////////////////////////////////////////// + +module insn_assert ( + input logic clk_i, + input logic rst_ni, + // Instruction memory interface + input logic instr_req_o, + input logic instr_gnt_i, + input logic instr_rvalid_i, + input logic [31:0] instr_addr_o, + input logic [31:0] instr_rdata_i +); + + import cv32e40p_pkg::*; + import cv32e40p_tracer_pkg::*; + + /***************** + * Helpers logic * + *****************/ + int s_outstanding_cnt; + + always_ff @(posedge clk_i or negedge rst_ni) begin + if(!rst_ni) begin + s_outstanding_cnt <= 0; + end else if (instr_req_o & instr_gnt_i & instr_rvalid_i) begin + s_outstanding_cnt <= s_outstanding_cnt; + end else if (instr_req_o & instr_gnt_i) begin + s_outstanding_cnt <= s_outstanding_cnt + 1; + end else if (instr_rvalid_i) begin + s_outstanding_cnt <= s_outstanding_cnt - 1; + end + end + + logic [31:0] s_prev_insn; + always_ff @(posedge clk_i or negedge rst_ni) begin + if(!rst_ni) begin + s_prev_insn <= '0; + end else if (instr_rvalid_i) begin + s_prev_insn <= instr_rdata_i; + end + end + + /********** + * Assume * + **********/ + // Concerning lint_grnt + property no_grnt_when_no_req; + @(posedge clk_i) disable iff(!rst_ni) + !instr_req_o |-> !instr_gnt_i; + endproperty + + property no_rvalid_if_no_pending_req; + @(posedge clk_i) disable iff(!rst_ni) + s_outstanding_cnt < 1 |-> !instr_rvalid_i; + endproperty + + property no_compressed; + @(posedge clk_i) disable iff(!rst_ni) + instr_rdata_i[1:0] == 2'b11; + endproperty + + property no_jump; + @(posedge clk_i) disable iff(!rst_ni) + (instr_rdata_i[6:0] != OPCODE_JAL) & (instr_rdata_i[6:0] != OPCODE_JALR); + endproperty + + property no_branch; + @(posedge clk_i) disable iff(!rst_ni) + instr_rdata_i[6:0] != OPCODE_BRANCH; + endproperty + + property no_custom0; + @(posedge clk_i) disable iff(!rst_ni) + instr_rdata_i[6:0] != OPCODE_CUSTOM_0; + endproperty + + property cvend0_only_after_cvstart0; + @(posedge clk_i) disable iff(!rst_ni) + (s_prev_insn != INSTR_CVSTARTI0) & (s_prev_insn != INSTR_CVSTARTI0) |-> (instr_rdata_i != INSTR_CVSENDI0) & (instr_rdata_i != INSTR_CVEND0); + endproperty + + property cvcount0_only_after_cvend0; + @(posedge clk_i) disable iff(!rst_ni) + (s_prev_insn != INSTR_CVSENDI0) & (s_prev_insn != INSTR_CVEND0) |-> (instr_rdata_i != INSTR_CVCOUNTI0) & (instr_rdata_i != INSTR_CVCOUNT0); + endproperty + + property no_cvsetup0; + @(posedge clk_i) disable iff(!rst_ni) + (instr_rdata_i != INSTR_CVSETUPI0) & (instr_rdata_i != INSTR_CVSETUP0); + endproperty + + property no_cvstart0; + @(posedge clk_i) disable iff(!rst_ni) + (instr_rdata_i != INSTR_CVSTARTI0) & (instr_rdata_i != INSTR_CVSTART0); + endproperty + + property cvend1_only_after_cvstart1; + @(posedge clk_i) disable iff(!rst_ni) + (s_prev_insn != INSTR_CVSTARTI1) & (s_prev_insn != INSTR_CVSTARTI1) |-> (instr_rdata_i != INSTR_CVSENDI1) & (instr_rdata_i != INSTR_CVEND1); + endproperty + + property cvcount1_only_after_cvend1; + @(posedge clk_i) disable iff(!rst_ni) + (s_prev_insn != INSTR_CVSENDI1) & (s_prev_insn != INSTR_CVEND1) |-> (instr_rdata_i != INSTR_CVCOUNTI1) & (instr_rdata_i != INSTR_CVCOUNT1); + endproperty + + property no_cvsetup1; + @(posedge clk_i) disable iff(!rst_ni) + (instr_rdata_i != INSTR_CVSETUPI1) & (instr_rdata_i != INSTR_CVSETUP1); + endproperty + + property no_cvstart1; + @(posedge clk_i) disable iff(!rst_ni) + (instr_rdata_i != INSTR_CVSTARTI1) & (instr_rdata_i != INSTR_CVSTART1); + endproperty + + property no_csr_write_to_hwloop; + @(posedge clk_i) disable iff(!rst_ni) + instr_rdata_i[6:0] == OPCODE_SYSTEM |-> (instr_rdata_i[31:20] != 12'hCC0) & (instr_rdata_i[31:20] != 12'hCC1) & (instr_rdata_i[31:20] != 12'hCC2) & (instr_rdata_i[31:20] != 12'hCC4) & (instr_rdata_i[31:20] != 12'hCC5) & (instr_rdata_i[31:20] != 12'hCC6); + endproperty + + assume_no_grnt_when_no_req: assume property(no_grnt_when_no_req); + assume_no_rvalid_if_no_pending_req: assume property(no_rvalid_if_no_pending_req); + // assume_no_compressed: assume property(no_compressed); + // assume_no_jump: assume property(no_jump); + // assume_no_branch: assume property(no_branch); + + // assume_no_custom0: assume property(no_custom0); + + //hwloop 0 constraints + // assume_cvend0_only_after_cvstart0: assume property(cvend0_only_after_cvstart0); + // assume_cvcount0_only_after_cvend0: assume property(cvcount0_only_after_cvend0); + // assume_no_cvsetup0: assume property(no_cvsetup0); + // assume_no_cvstart0: assume property(no_cvstart0); //This one disables all hwloop0 + //hwloop 1 constraints + // assume_cvend1_only_after_cvstart1: assume property(cvend1_only_after_cvstart1); + // assume_cvcount1_only_after_cvend1: assume property(cvcount1_only_after_cvend1); + // assume_no_cvsetup1: assume property(no_cvsetup1); + // assume_no_cvstart1: assume property(no_cvstart1); //This one disables all hwloop1 + + assume_no_csr_write_to_hwloop: assume property(no_csr_write_to_hwloop); + +endmodule \ No newline at end of file diff --git a/scripts/formal/src/interrupt_assert.sv b/scripts/formal/src/interrupt_assert.sv new file mode 100644 index 000000000..0f0e67492 --- /dev/null +++ b/scripts/formal/src/interrupt_assert.sv @@ -0,0 +1,46 @@ +// Copyright 2024 Dolphin Design +// 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. + +//////////////////////////////////////////////////////////////////////////////////// +// // +// Contributors: Yoann Pruvost, Dolphin Design // +// // +// Description: Debug interface constraints // +// // +//////////////////////////////////////////////////////////////////////////////////// + +module interrput_assert ( + input logic clk_i, + input logic rst_ni, + // Interrupt inputs + input logic [31:0] irq_i, + input logic irq_ack_o, + input logic [ 4:0] irq_id_o +); + + /********** + * Assume * + **********/ + property no_interrupt; + @(posedge clk_i) disable iff(!rst_ni) + irq_i == '0; + endproperty + + // Uncomment to disable interrupt interface + // assume_no_interrupt: assume property(no_interrupt); + + +endmodule \ No newline at end of file