From b7434ba1dbadfe59fe116f9003f46073c2404781 Mon Sep 17 00:00:00 2001 From: Yoann Pruvost Date: Tue, 4 Jun 2024 14:21:42 +0800 Subject: [PATCH 1/2] Adding formal rule for coverage holes on controller --- bhv/cv32e40p_instr_trace.svh | 2 +- scripts/formal/cv32e40p_formal.flist | 1 + scripts/formal/formal.do | 46 +++++++------- scripts/formal/src/cv32e40p_bind.sv | 16 +++++ .../formal/src/cv32e40p_controller_assert.sv | 61 +++++++++++++++++++ 5 files changed, 102 insertions(+), 24 deletions(-) create mode 100644 scripts/formal/src/cv32e40p_controller_assert.sv diff --git a/bhv/cv32e40p_instr_trace.svh b/bhv/cv32e40p_instr_trace.svh index 355bc7382..95d0f90fa 100644 --- a/bhv/cv32e40p_instr_trace.svh +++ b/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, diff --git a/scripts/formal/cv32e40p_formal.flist b/scripts/formal/cv32e40p_formal.flist index e3c5f1f2a..8fa39ad0f 100644 --- a/scripts/formal/cv32e40p_formal.flist +++ b/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 \ No newline at end of file diff --git a/scripts/formal/formal.do b/scripts/formal/formal.do index 8e0be6031..f2f037143 100644 --- a/scripts/formal/formal.do +++ b/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 // -// // -// 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 // +# // +# Description: Formal script for CV32E40P // +# // +#////////////////////////////////////////////////////////////////////////////////// set top cv32e40p_formal_top diff --git a/scripts/formal/src/cv32e40p_bind.sv b/scripts/formal/src/cv32e40p_bind.sv index 38d51941a..e3a1b7b62 100644 --- a/scripts/formal/src/cv32e40p_bind.sv +++ b/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), diff --git a/scripts/formal/src/cv32e40p_controller_assert.sv b/scripts/formal/src/cv32e40p_controller_assert.sv new file mode 100644 index 000000000..47a41d715 --- /dev/null +++ b/scripts/formal/src/cv32e40p_controller_assert.sv @@ -0,0 +1,61 @@ +// 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 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_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); + assert_unreachable_ctrl_1241_row_10: assert property(unreachable_ctrl_1241_row_10); + +endmodule \ No newline at end of file From c581a90ea5e280f14cf33ee71538aa70b2102a50 Mon Sep 17 00:00:00 2001 From: Yoann Pruvost Date: Thu, 6 Jun 2024 15:37:34 +0800 Subject: [PATCH 2/2] Adding more assertions for code coverage holes in controller --- scripts/formal/src/cv32e40p_controller_assert.sv | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/scripts/formal/src/cv32e40p_controller_assert.sv b/scripts/formal/src/cv32e40p_controller_assert.sv index 47a41d715..6eab1dd7a 100644 --- a/scripts/formal/src/cv32e40p_controller_assert.sv +++ b/scripts/formal/src/cv32e40p_controller_assert.sv @@ -49,6 +49,16 @@ module cv32e40p_controller_assert import cv32e40p_pkg::*; (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; @@ -56,6 +66,9 @@ module cv32e40p_controller_assert import cv32e40p_pkg::*; 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 \ No newline at end of file