diff --git a/scripts/formal/fpv.tcl b/scripts/formal/fpv.tcl new file mode 100755 index 000000000..06c22cda7 --- /dev/null +++ b/scripts/formal/fpv.tcl @@ -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 + diff --git a/scripts/formal/src/cv32e40p_controller_assert.sv b/scripts/formal/src/cv32e40p_controller_assert.sv index 6eab1dd7a..2c61e3d58 100644 --- a/scripts/formal/src/cv32e40p_controller_assert.sv +++ b/scripts/formal/src/cv32e40p_controller_assert.sv @@ -67,8 +67,8 @@ 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_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 +endmodule diff --git a/scripts/slec/cadence/sec.tcl b/scripts/slec/cadence/sec.tcl old mode 100644 new mode 100755 index 7107eb9e3..d2c2b0d8e --- a/scripts/slec/cadence/sec.tcl +++ b/scripts/slec/cadence/sec.tcl @@ -13,10 +13,15 @@ # limitations under the License. set summary_log $::env(summary_log) set top_module $::env(top_module) +set report_dir $::env(report_dir) + +set_sec_disable_imp_assumption none check_sec -setup -spec_top $top_module -imp_top $top_module \ - -spec_analyze "-sv -f ./golden.src" \ + -spec_analyze "-sv -f ./golden.src"\ -imp_analyze "-sv -f ./revised.src"\ + -spec_elaborate_opts "-parameter COREV_PULP 1"\ + -imp_elaborate_opts "-parameter COREV_PULP 1"\ -auto_map_reset_x_values diff --git a/scripts/slec/run.sh b/scripts/slec/run.sh index 01bb1b126..99e3284c6 100755 --- a/scripts/slec/run.sh +++ b/scripts/slec/run.sh @@ -117,6 +117,7 @@ if [[ "${VERSION}" == "v1" ]]; then REF_BRANCH=cv32e40p_v1.0.0 TOP_MODULE=cv32e40p_core else + echo "version 2" REF_BRANCH=dev TOP_MODULE=cv32e40p_top fi @@ -168,9 +169,10 @@ fi REVISED_DIR=$RTL_FOLDER REVISED_FLIST=$(pwd)/revised.src - +TB_SRC_DIR=$(pwd)/tb_src GOLDEN_DIR=$(readlink -f ./${REF_FOLDER}/) GOLDEN_FLIST=$(pwd)/golden.src +TB_FLIST=cv32e40p_tb_src.flist 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/|') @@ -178,12 +180,14 @@ if [[ "${VERSION}" == "v1" ]]; then 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/|') else 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/|') + 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}"'|') fi print_log "Generating GOLDEN flist in path: ${GOLDEN_FLIST}" echo $var_golden_rtl > ${GOLDEN_FLIST} print_log "Generating REVISED flist in path: ${REVISED_FLIST}" echo $var_revised_rtl > ${REVISED_FLIST} +echo $var_tb >> ${REVISED_FLIST} export report_dir=$(readlink -f $(dirname "${BASH_SOURCE[0]}"))/reports/${target_tool}/$(date +%Y-%m-%d-%Hh%Mm%Ss) @@ -204,7 +208,7 @@ if [[ "${target_tool}" == "cadence" ]]; then lec -Dofile ${tcl_script} -TclMode -NoGUI -xl | tee ${output_log} regex_string="Hierarchical compare : Equivalent" elif [[ "${target_process}" == "sec" ]]; then - jg -sec -proj ${report_dir} -batch -tcl ${tcl_script} -define report_dir ${report_dir} | tee ${output_log} + jg -sec -proj ${report_dir} -tcl ${tcl_script} -define report_dir ${report_dir} | tee ${output_log} regex_string="Overall SEC status[ ]+- Complete" fi diff --git a/scripts/slec/tb_src/cv32e40p_bind2.sv b/scripts/slec/tb_src/cv32e40p_bind2.sv new file mode 100755 index 000000000..d328a24fa --- /dev/null +++ b/scripts/slec/tb_src/cv32e40p_bind2.sv @@ -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 // +// Pascal Gouedo, Dolphin Design // +// // +// 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) +); diff --git a/scripts/slec/tb_src/cv32e40p_tb_src.flist b/scripts/slec/tb_src/cv32e40p_tb_src.flist new file mode 100755 index 000000000..893ce99a1 --- /dev/null +++ b/scripts/slec/tb_src/cv32e40p_tb_src.flist @@ -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 diff --git a/scripts/slec/tb_src/data_assert2.sv b/scripts/slec/tb_src/data_assert2.sv new file mode 100755 index 000000000..762057cc8 --- /dev/null +++ b/scripts/slec/tb_src/data_assert2.sv @@ -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 // +// Pascal Gouedo, Dolphin Design // +// // +// 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 diff --git a/scripts/slec/tb_src/insn_assert2.sv b/scripts/slec/tb_src/insn_assert2.sv new file mode 100755 index 000000000..b04c01228 --- /dev/null +++ b/scripts/slec/tb_src/insn_assert2.sv @@ -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 // +// Pascal Gouedo, Dolphin Design // +// // +// 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