jasper SLEC script changes

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
+

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
+endmodule

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
 
 

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,22 +169,25 @@ 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/|')
 
 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
 

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 <[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)
+);

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

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 <[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

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 <[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