Skip to content

Commit b2eebc5

Browse files
MikeOpenHWGroupMikeOpenHWGroup
authored
Merge pull request #1003 from mret55/dev
jasper SLEC script changes
2 parents bdd5253 + f5ce76d commit b2eebc5

File tree

8 files changed

+223
-5
lines changed

8 files changed

+223
-5
lines changed

‎scripts/formal/fpv.tcl

Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,23 @@
1+
// Copyright 2024 Cirrus Logic
2+
// SPDX-License-Identifier: Apache-2.0 WITH SHL-2.1
3+
4+
set DESIGN_RTL_DIR ../../rtl
5+
6+
analyze -sv -f ../../cv32e40p_fpu_manifest.flist
7+
analyze -sva -f cv32e40p_formal.flist
8+
9+
elaborate -top cv32e40p_formal_top
10+
11+
#Set up clocks and reset
12+
clock clk_i
13+
reset ~rst_ni
14+
15+
# Get design information to check general complexity
16+
get_design_info
17+
18+
#Prove properties
19+
prove -all
20+
21+
#Report proof results
22+
report
23+

‎scripts/formal/src/cv32e40p_controller_assert.sv

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -67,8 +67,8 @@ module cv32e40p_controller_assert import cv32e40p_pkg::*;
6767
assert_all_true_ctrl_1187_1189_and_1191: assert property(all_true_ctrl_1187_1189_and_1191);
6868
assert_all_true_ctrl_1210_and_1212 : assert property(all_true_ctrl_1210_and_1212);
6969
//This one is inconclusive with questa formal. To avoid long run keep it disabled
70-
// assert_unreachable_ctrl_1241_row_4 : assert property(unreachable_ctrl_1241_row_4);
70+
assert_unreachable_ctrl_1241_row_4 : assert property(unreachable_ctrl_1241_row_4);
7171
assert_unreachable_ctrl_1241_row_5 : assert property(unreachable_ctrl_1241_row_5);
7272
assert_unreachable_ctrl_1241_row_10: assert property(unreachable_ctrl_1241_row_10);
7373

74-
endmodule
74+
endmodule

‎scripts/slec/cadence/sec.tcl

100644100755
Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -13,10 +13,15 @@
1313
# limitations under the License.
1414
set summary_log $::env(summary_log)
1515
set top_module $::env(top_module)
16+
set report_dir $::env(report_dir)
17+
18+
set_sec_disable_imp_assumption none
1619

1720
check_sec -setup -spec_top $top_module -imp_top $top_module \
18-
-spec_analyze "-sv -f ./golden.src" \
21+
-spec_analyze "-sv -f ./golden.src"\
1922
-imp_analyze "-sv -f ./revised.src"\
23+
-spec_elaborate_opts "-parameter COREV_PULP 1"\
24+
-imp_elaborate_opts "-parameter COREV_PULP 1"\
2025
-auto_map_reset_x_values
2126

2227

‎scripts/slec/run.sh

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -117,6 +117,7 @@ if [[ "${VERSION}" == "v1" ]]; then
117117
REF_BRANCH=cv32e40p_v1.0.0
118118
TOP_MODULE=cv32e40p_core
119119
else
120+
echo "version 2"
120121
REF_BRANCH=dev
121122
TOP_MODULE=cv32e40p_top
122123
fi
@@ -168,22 +169,25 @@ fi
168169

169170
REVISED_DIR=$RTL_FOLDER
170171
REVISED_FLIST=$(pwd)/revised.src
171-
172+
TB_SRC_DIR=$(pwd)/tb_src
172173
GOLDEN_DIR=$(readlink -f ./${REF_FOLDER}/)
173174
GOLDEN_FLIST=$(pwd)/golden.src
175+
TB_FLIST=cv32e40p_tb_src.flist
174176

175177
var_golden_rtl=$(awk '{ if ($0 ~ "{DESIGN_RTL_DIR}" && $0 !~ "#" && $0 !~ "tracer" && $0 !~ "tb_wrapper" && $0 !~ "cv32e40p_wrapper") print $0 }' ${GOLDEN_DIR}/$FLIST | sed 's|${DESIGN_RTL_DIR}|'"${GOLDEN_DIR}"'/rtl/|')
176178

177179
if [[ "${VERSION}" == "v1" ]]; then
178180
var_revised_rtl=$(awk '{ if ($0 ~ "{DESIGN_RTL_DIR}" && $0 !~ "#" && $0 !~ "tracer" && $0 !~ "tb_wrapper" && $0 !~ "cv32e40p_wrapper" && $0 !~ "top") print $0 }' ${REVISED_DIR}/$FLIST | sed 's|${DESIGN_RTL_DIR}|'"${REVISED_DIR}"'/rtl/|')
179181
else
180182
var_revised_rtl=$(awk '{ if ($0 ~ "{DESIGN_RTL_DIR}" && $0 !~ "#" && $0 !~ "tracer" && $0 !~ "tb_wrapper") print $0 }' ${REVISED_DIR}/$FLIST | sed 's|${DESIGN_RTL_DIR}|'"${REVISED_DIR}"'/rtl/|')
183+
var_tb=$(awk '{ if ($0 ~ "{TB_SRC_DIR}" && $0 !~ "#" && $0 !~ "tracer" && $0 !~ "tb_wrapper") print $0 }' ${TB_SRC_DIR}/$TB_FLIST | sed 's|${TB_SRC_DIR}|'"${TB_SRC_DIR}"'|')
181184
fi
182185

183186
print_log "Generating GOLDEN flist in path: ${GOLDEN_FLIST}"
184187
echo $var_golden_rtl > ${GOLDEN_FLIST}
185188
print_log "Generating REVISED flist in path: ${REVISED_FLIST}"
186189
echo $var_revised_rtl > ${REVISED_FLIST}
190+
echo $var_tb >> ${REVISED_FLIST}
187191

188192
export report_dir=$(readlink -f $(dirname "${BASH_SOURCE[0]}"))/reports/${target_tool}/$(date +%Y-%m-%d-%Hh%Mm%Ss)
189193

@@ -204,7 +208,7 @@ if [[ "${target_tool}" == "cadence" ]]; then
204208
lec -Dofile ${tcl_script} -TclMode -NoGUI -xl | tee ${output_log}
205209
regex_string="Hierarchical compare : Equivalent"
206210
elif [[ "${target_process}" == "sec" ]]; then
207-
jg -sec -proj ${report_dir} -batch -tcl ${tcl_script} -define report_dir ${report_dir} | tee ${output_log}
211+
jg -sec -proj ${report_dir} -tcl ${tcl_script} -define report_dir ${report_dir} | tee ${output_log}
208212
regex_string="Overall SEC status[ ]+- Complete"
209213
fi
210214

‎scripts/slec/tb_src/cv32e40p_bind2.sv

Lines changed: 42 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,42 @@
1+
// Copyright 2024 Dolphin Design
2+
// SPDX-License-Identifier: Apache-2.0 WITH SHL-2.1
3+
//
4+
// Licensed under the Solderpad Hardware License v 2.1 (the "License");
5+
// you may not use this file except in compliance with the License, or,
6+
// at your option, the Apache License version 2.0.
7+
// You may obtain a copy of the License at
8+
//
9+
// https://solderpad.org/licenses/SHL-2.1/
10+
//
11+
// Unless required by applicable law or agreed to in writing, any work
12+
// distributed under the License is distributed on an "AS IS" BASIS,
13+
// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
14+
// See the License for the specific language governing permissions and
15+
// limitations under the License.
16+
17+
////////////////////////////////////////////////////////////////////////////////////
18+
// //
19+
// Contributors: Yoann Pruvost, Dolphin Design <yoann.pruvost@dolphin.fr> //
20+
// Pascal Gouedo, Dolphin Design <pascal.gouedo@dolphin.fr> //
21+
// //
22+
// Description: CV32E40P binding for formal code analysis //
23+
// //
24+
////////////////////////////////////////////////////////////////////////////////////
25+
26+
bind cv32e40p_top insn_assert u_insn_assert (
27+
.clk_i(clk_i),
28+
.rst_ni(rst_ni),
29+
30+
.instr_req_o (instr_req_o),
31+
.instr_gnt_i (instr_gnt_i),
32+
.instr_rvalid_i(instr_rvalid_i)
33+
);
34+
35+
bind cv32e40p_top data_assert u_data_assert (
36+
.clk_i(clk_i),
37+
.rst_ni(rst_ni),
38+
39+
.data_req_o (data_req_o ),
40+
.data_gnt_i (data_gnt_i ),
41+
.data_rvalid_i(data_rvalid_i)
42+
);

‎scripts/slec/tb_src/cv32e40p_tb_src.flist

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
// Copyright 2024 Cirrus Logic
2+
// SPDX-License-Identifier: Apache-2.0 WITH SHL-2.1
3+
${TB_SRC_DIR}/insn_assert2.sv
4+
${TB_SRC_DIR}/data_assert2.sv
5+
${TB_SRC_DIR}/cv32e40p_bind2.sv

‎scripts/slec/tb_src/data_assert2.sv

Lines changed: 70 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,70 @@
1+
// Copyright 2024 Dolphin Design
2+
// SPDX-License-Identifier: Apache-2.0 WITH SHL-2.1
3+
//
4+
// Licensed under the Solderpad Hardware License v 2.1 (the "License");
5+
// you may not use this file except in compliance with the License, or,
6+
// at your option, the Apache License version 2.0.
7+
// You may obtain a copy of the License at
8+
//
9+
// https://solderpad.org/licenses/SHL-2.1/
10+
//
11+
// Unless required by applicable law or agreed to in writing, any work
12+
// distributed under the License is distributed on an "AS IS" BASIS,
13+
// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
14+
// See the License for the specific language governing permissions and
15+
// limitations under the License.
16+
17+
////////////////////////////////////////////////////////////////////////////////////
18+
// //
19+
// Contributors: Yoann Pruvost, Dolphin Design <yoann.pruvost@dolphin.fr> //
20+
// Pascal Gouedo, Dolphin Design <pascal.gouedo@dolphin.fr> //
21+
// //
22+
// Description: OBI protocol emulation for CV32E40P data interface //
23+
// //
24+
////////////////////////////////////////////////////////////////////////////////////
25+
26+
module data_assert (
27+
input logic clk_i,
28+
input logic rst_ni,
29+
30+
// Data memory interface
31+
input logic data_req_o,
32+
input logic data_gnt_i,
33+
input logic data_rvalid_i
34+
);
35+
36+
/*****************
37+
* Helpers logic *
38+
*****************/
39+
int s_outstanding_cnt;
40+
41+
always_ff @(posedge clk_i or negedge rst_ni) begin
42+
if(!rst_ni) begin
43+
s_outstanding_cnt <= 0;
44+
end else if (data_req_o & data_gnt_i & data_rvalid_i) begin
45+
s_outstanding_cnt <= s_outstanding_cnt;
46+
end else if (data_req_o & data_gnt_i) begin
47+
s_outstanding_cnt <= s_outstanding_cnt + 1;
48+
end else if (data_rvalid_i) begin
49+
s_outstanding_cnt <= s_outstanding_cnt - 1;
50+
end
51+
end
52+
53+
/**********
54+
* Assume *
55+
**********/
56+
// Concerning lint_grnt
57+
property no_grnt_when_no_req;
58+
@(posedge clk_i) disable iff(!rst_ni)
59+
!data_req_o |-> !data_gnt_i;
60+
endproperty
61+
62+
property no_rvalid_if_no_pending_req;
63+
@(posedge clk_i) disable iff(!rst_ni)
64+
s_outstanding_cnt < 1 |-> !data_rvalid_i;
65+
endproperty
66+
67+
assume_no_grnt_when_no_req: assume property(no_grnt_when_no_req);
68+
assume_no_rvalid_if_no_pending_req: assume property(no_rvalid_if_no_pending_req);
69+
70+
endmodule

‎scripts/slec/tb_src/insn_assert2.sv

Lines changed: 69 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,69 @@
1+
// Copyright 2024 Dolphin Design
2+
// SPDX-License-Identifier: Apache-2.0 WITH SHL-2.1
3+
//
4+
// Licensed under the Solderpad Hardware License v 2.1 (the "License");
5+
// you may not use this file except in compliance with the License, or,
6+
// at your option, the Apache License version 2.0.
7+
// You may obtain a copy of the License at
8+
//
9+
// https://solderpad.org/licenses/SHL-2.1/
10+
//
11+
// Unless required by applicable law or agreed to in writing, any work
12+
// distributed under the License is distributed on an "AS IS" BASIS,
13+
// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
14+
// See the License for the specific language governing permissions and
15+
// limitations under the License.
16+
17+
////////////////////////////////////////////////////////////////////////////////////
18+
// //
19+
// Contributors: Yoann Pruvost, Dolphin Design <yoann.pruvost@dolphin.fr> //
20+
// Pascal Gouedo, Dolphin Design <pascal.gouedo@dolphin.fr> //
21+
// //
22+
// Description: OBI protocol emulation for CV32E40P data interface //
23+
// //
24+
////////////////////////////////////////////////////////////////////////////////////
25+
26+
module insn_assert (
27+
input logic clk_i,
28+
input logic rst_ni,
29+
// Instruction memory interface
30+
input logic instr_req_o,
31+
input logic instr_gnt_i,
32+
input logic instr_rvalid_i
33+
);
34+
35+
/*****************
36+
* Helpers logic *
37+
*****************/
38+
int s_outstanding_cnt;
39+
40+
always_ff @(posedge clk_i or negedge rst_ni) begin
41+
if(!rst_ni) begin
42+
s_outstanding_cnt <= 0;
43+
end else if (instr_req_o & instr_gnt_i & instr_rvalid_i) begin
44+
s_outstanding_cnt <= s_outstanding_cnt;
45+
end else if (instr_req_o & instr_gnt_i) begin
46+
s_outstanding_cnt <= s_outstanding_cnt + 1;
47+
end else if (instr_rvalid_i) begin
48+
s_outstanding_cnt <= s_outstanding_cnt - 1;
49+
end
50+
end
51+
52+
/**********
53+
* Assume *
54+
**********/
55+
// Concerning lint_grnt
56+
property no_grnt_when_no_req;
57+
@(posedge clk_i) disable iff(!rst_ni)
58+
!instr_req_o |-> !instr_gnt_i;
59+
endproperty
60+
61+
property no_rvalid_if_no_pending_req;
62+
@(posedge clk_i) disable iff(!rst_ni)
63+
s_outstanding_cnt < 1 |-> !instr_rvalid_i;
64+
endproperty
65+
66+
assume_no_grnt_when_no_req: assume property(no_grnt_when_no_req);
67+
assume_no_rvalid_if_no_pending_req: assume property(no_rvalid_if_no_pending_req);
68+
69+
endmodule

0 commit comments

Comments
 (0)