Adding formal rule for coverage holes on controller

bhv/cv32e40p_instr_trace.svh

@@ -802,7 +802,7 @@ class instr_trace_t;
       else str_hb = ".h";
 
       // set mnemonic
-      case (instr)
+      casex (instr)
         INSTR_CVADDH   ,
         INSTR_CVADDSCH ,
         INSTR_CVADDSCIH,

scripts/formal/cv32e40p_formal.flist

@@ -28,6 +28,7 @@ src/data_assert.sv
 src/cv32e40p_assert.sv
 src/cv32e40p_ID_assert.sv
 src/cv32e40p_EX_assert.sv
+src/cv32e40p_controller_assert.sv
 src/fpnew_divsqrt_th_32_assert.sv
 src/cv32e40p_formal_top.sv
 src/cv32e40p_bind.sv

scripts/formal/formal.do

@@ -1,26 +1,26 @@
-// 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                                       //
-//                                                                                //
-////////////////////////////////////////////////////////////////////////////////////
+# 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
 

scripts/formal/src/cv32e40p_bind.sv

@@ -106,6 +106,22 @@ bind cv32e40p_ex_stage cv32e40p_EX_assert u_cv32e40p_EX_assert (
     .apu_read_dep_for_jalr_o    (apu_read_dep_for_jalr_o    )
 );
 
+bind cv32e40p_controller cv32e40p_controller_assert u_cv32e40p_controller_assert (
+    .clk_i (clk_i ),
+    .rst_ni(rst_ni),
+
+    .data_load_event_i    (data_load_event_i    ),
+    .trigger_match_i      (trigger_match_i      ),
+    .ebrk_insn_i          (ebrk_insn_i          ),
+    .debug_mode_q         (debug_mode_q         ),
+    .debug_req_entry_q    (debug_req_entry_q    ),
+    .ebrk_force_debug_mode(ebrk_force_debug_mode),
+    .debug_force_wakeup_q (debug_force_wakeup_q ),
+    .debug_single_step_i  (debug_single_step_i  ),
+    .data_err_i           (data_err_i           ),
+    .ctrl_fsm_cs          (ctrl_fsm_cs          )
+);
+
 bind fpnew_divsqrt_th_32 fpnew_divsqrt_th_32_assert u_fpnew_divsqrt_th_32_assert (
     .clk_i (clk_i),
     .rst_ni(rst_ni),

scripts/formal/src/cv32e40p_controller_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 controller            //
+//                                                                                //
+////////////////////////////////////////////////////////////////////////////////////
+
+module cv32e40p_controller_assert import cv32e40p_pkg::*;
+(
+    input logic clk_i,
+    input logic rst_ni,
+
+    input logic data_load_event_i,
+    input logic trigger_match_i,
+    input logic ebrk_insn_i,
+    input logic debug_mode_q,
+    input logic debug_req_entry_q,
+    input logic ebrk_force_debug_mode,
+    input logic debug_force_wakeup_q,
+    input logic debug_single_step_i,
+    input logic data_err_i,
+    input ctrl_state_e ctrl_fsm_cs
+);
+
+    property all_true_ctrl_1187_1189_and_1191;
+        @(posedge clk_i) disable iff(!rst_ni)
+            ((ctrl_fsm_cs == DBG_TAKEN_ID) && ~debug_mode_q) |-> (trigger_match_i | (ebrk_force_debug_mode & ebrk_insn_i) | debug_req_entry_q);
+    endproperty
+
+    property all_true_ctrl_1210_and_1212;
+        @(posedge clk_i) disable iff(!rst_ni)
+            (ctrl_fsm_cs == DBG_TAKEN_IF) |-> (debug_force_wakeup_q | debug_single_step_i);
+    endproperty
+
+    property unreachable_ctrl_1241_row_4;
+        @(posedge clk_i) disable iff(!rst_ni)
+            ((ctrl_fsm_cs == DBG_FLUSH) && !data_err_i) && (~debug_req_entry_q && ~data_load_event_i && ~(ebrk_force_debug_mode & ebrk_insn_i) && ~debug_mode_q) |-> ~trigger_match_i;
+    endproperty
+
+    property unreachable_ctrl_1241_row_5;
+        @(posedge clk_i) disable iff(!rst_ni)
+            ((ctrl_fsm_cs == DBG_FLUSH) && !data_err_i) && (~debug_req_entry_q && ~data_load_event_i && ~(debug_mode_q | trigger_match_i) && ebrk_insn_i) |-> ebrk_force_debug_mode;
+    endproperty
+
+    property unreachable_ctrl_1241_row_10;
+        @(posedge clk_i) disable iff(!rst_ni)
+            ((ctrl_fsm_cs == DBG_FLUSH) && !data_err_i) && (~debug_req_entry_q && ~((debug_mode_q | trigger_match_i) | (ebrk_force_debug_mode & ebrk_insn_i))) |-> !data_load_event_i;
+    endproperty
+
+    assert_all_true_ctrl_1187_1189_and_1191: assert property(all_true_ctrl_1187_1189_and_1191);
+    assert_all_true_ctrl_1210_and_1212 : assert property(all_true_ctrl_1210_and_1212);
+    //This one is inconclusive with questa formal. To avoid long run keep it disabled
+    // assert_unreachable_ctrl_1241_row_4 : assert property(unreachable_ctrl_1241_row_4);
+    assert_unreachable_ctrl_1241_row_5 : assert property(unreachable_ctrl_1241_row_5);
+    assert_unreachable_ctrl_1241_row_10: assert property(unreachable_ctrl_1241_row_10);
+
+endmodule