-
Notifications
You must be signed in to change notification settings - Fork 418
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge pull request #997 from YoannPruvost/dev_formal_2
Adding formal rule for coverage holes on controller
- Loading branch information
Showing
5 changed files
with
115 additions
and
24 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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 | ||
|
|
||
|
|
||
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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 |