jasper SLEC script changes

Updated jasper SLEC script for parameters usage. Added assumption files and bind file scripts/slec/cadence folder.

scripts/slec/cadence/README.rtf

@@ -0,0 +1,8 @@
+{\rtf1\ansi\ansicpg1252\cocoartf2761
+\cocoatextscaling0\cocoaplatform0{\fonttbl\f0\fswiss\fcharset0 Helvetica;}
+{\colortbl;\red255\green255\blue255;}
+{\*\expandedcolortbl;;}
+\margl1440\margr1440\vieww11520\viewh8400\viewkind0
+\pard\tx720\tx1440\tx2160\tx2880\tx3600\tx4320\tx5040\tx5760\tx6480\tx7200\tx7920\tx8640\pardirnatural\partightenfactor0
+
+\f0\fs24 \cf0 Add assume (data_assert2.sv and insn_assert2.sv) files and bind (cv32e40p_bind2.sv) files to flist file inside rtl directory. }

scripts/slec/cadence/cv32e40p_bind2.sv

@@ -0,0 +1,18 @@
+
+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/cadence/data_assert2.sv

@@ -0,0 +1,46 @@
+
+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/cadence/insn_assert2.sv

@@ -0,0 +1,45 @@
+
+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

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