Merge pull request #994 from YoannPruvost/dev_formal

Code coverage holes formal analysis

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 <[email protected]>         #
+#                                                                                #
+# 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

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 <PATH_TO_PROPCHECK_DB>``` to open the results in GUI.

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 <[email protected]>         //
+//                                                                                //
+// 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

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 <[email protected]>         //
+//                                                                                //
+// 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

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 <[email protected]>         //
+//                                                                                //
+// 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

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 <[email protected]>         //
+//                                                                                //
+// 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