-
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 #1003 from mret55/dev
jasper SLEC script changes
- Loading branch information
Showing
8 changed files
with
223 additions
and
5 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
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,23 @@ | ||
| // Copyright 2024 Cirrus Logic | ||
| // SPDX-License-Identifier: Apache-2.0 WITH SHL-2.1 | ||
|
|
||
| set DESIGN_RTL_DIR ../../rtl | ||
|
|
||
| analyze -sv -f ../../cv32e40p_fpu_manifest.flist | ||
| analyze -sva -f cv32e40p_formal.flist | ||
|
|
||
| elaborate -top cv32e40p_formal_top | ||
|
|
||
| #Set up clocks and reset | ||
| clock clk_i | ||
| reset ~rst_ni | ||
|
|
||
| # Get design information to check general complexity | ||
| get_design_info | ||
|
|
||
| #Prove properties | ||
| prove -all | ||
|
|
||
| #Report proof results | ||
| report | ||
|
|
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
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,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 <[email protected]> // | ||
| // Pascal Gouedo, Dolphin Design <[email protected]> // | ||
| // // | ||
| // Description: CV32E40P binding for formal code analysis // | ||
| // // | ||
| //////////////////////////////////////////////////////////////////////////////////// | ||
|
|
||
| bind cv32e40p_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) | ||
| ); | ||
|
|
||
| bind cv32e40p_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) | ||
| ); |
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,5 @@ | ||
| // Copyright 2024 Cirrus Logic | ||
| // SPDX-License-Identifier: Apache-2.0 WITH SHL-2.1 | ||
| ${TB_SRC_DIR}/insn_assert2.sv | ||
| ${TB_SRC_DIR}/data_assert2.sv | ||
| ${TB_SRC_DIR}/cv32e40p_bind2.sv |
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,70 @@ | ||
| // 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]> // | ||
| // Pascal Gouedo, Dolphin Design <[email protected]> // | ||
| // // | ||
| // 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 | ||
| ); | ||
|
|
||
| /***************** | ||
| * 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 |
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,69 @@ | ||
| // 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]> // | ||
| // Pascal Gouedo, Dolphin Design <[email protected]> // | ||
| // // | ||
| // Description: OBI protocol emulation for CV32E40P data 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 | ||
| ); | ||
|
|
||
| /***************** | ||
| * 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 | ||
|
|
||
| /********** | ||
| * 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 | ||
|
|
||
| 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 |