From 162574dbbcc8eb1a9ebc2d8690ba2f08289a1e5a Mon Sep 17 00:00:00 2001 From: mret55 Date: Wed, 12 Jun 2024 10:13:07 -0500 Subject: [PATCH] jasper SLEC script changes Updated jasper SLEC script for parameters usage. Added assumption files and bind file scripts/slec/cadence folder. --- .DS_Store | Bin 0 -> 6148 bytes scripts/.DS_Store | Bin 0 -> 6148 bytes scripts/slec/.DS_Store | Bin 0 -> 6148 bytes scripts/slec/cadence/README.rtf | 8 +++++ scripts/slec/cadence/cv32e40p_bind2.sv | 18 ++++++++++ scripts/slec/cadence/data_assert2.sv | 46 +++++++++++++++++++++++++ scripts/slec/cadence/insn_assert2.sv | 45 ++++++++++++++++++++++++ scripts/slec/cadence/sec.tcl | 7 +++- 8 files changed, 123 insertions(+), 1 deletion(-) create mode 100644 .DS_Store create mode 100644 scripts/.DS_Store create mode 100644 scripts/slec/.DS_Store create mode 100644 scripts/slec/cadence/README.rtf create mode 100755 scripts/slec/cadence/cv32e40p_bind2.sv create mode 100755 scripts/slec/cadence/data_assert2.sv create mode 100755 scripts/slec/cadence/insn_assert2.sv mode change 100644 => 100755 scripts/slec/cadence/sec.tcl diff --git a/.DS_Store b/.DS_Store new file mode 100644 index 0000000000000000000000000000000000000000..63bf7aa6876ce38bea71a860508bbfd474d0df7b GIT binary patch literal 6148 zcmeHK%}T>S5T3QwrWBzEg&r5Y7Hn-%ikA@U3mDOZN^NY>V9b^zwTDv3SzpK}@p+ut z-GJ2|Jc-yD*!^bbXE*af_6GojHyyPB>Hy$iBNU{p5HhcHZP;K!q34)D25B%$CqcAg zqQ7XOZ?8ZKcaT5`pT1uO=y?k!QJ7|}*1Om!l{dF4j^osv8~;Jg{A`#_Q*W4D(db;M zC@Az{a1oAYgZj>iinC!Dj}x5`j>Z^reHq3hHS^Ro9;G_hHx8#-tq$sq`MlljHD%|h zw`j_F@1WI`-Ok}+QFV6r_K(j7kI_@CUJR82S=X{{v4B@pzEt(>Cvl|Wd-N1pMKmKb zzzi@0%)ojvV9x=kwq9j(wafrB@B;>De~{P+U5mLvy>(zm*JtvV2}w|=w*;ZI=vvGT zq6bBoR78_1>=Q$nbhJww=UU7Snsg9)Wt_*ZTs&TcULEaHhl6kpa?cDf1IrAQ%&<=9 z|0(`5DZ;7$ga~7`68eR;f@*j1qMCzjaZ9B1e@=JR&9*OZ;3-l8ezy@OU$ zb~}fQg(G(N_K(kokI7T2UJRie_|~#*v4mGpKG*Z?PtruC_uwn@%REA2fEXYKh=KKG zz@7=BzP=RD%83DD;0Fe9e~{1+J&T1wy>&o`*Jq5^5K%zKw*;cJ=vgcbLIi}HQb1G6 z?GuBWa_~!==UFTansUbV%rK6fxqQ5EJv;cNPG{URNIfw?3@kHHHKvQ_|0(=3DS5Z<-brW7Fug&r5Y7Hn-%ikDF93mDOZN=;1AV9b^#HHT8jSzpK}@p+ut z-GJ2`Jc-yD*nG3|v%B*__J=XXNAsY^n9UfopdoTpDg@1yt_>56$kiALyJMlBr&B+! z80asWaP19PwZ{S$vQO)mK6u{zX&j|lxBJdFYW2;nhSjiI){Xlhb2sy{c{=iDSJ*q3 zGWJW|^Dm+>pV&JmGReFs31=!H3PK3EzKoJU<|8>zf>h=V=EQC<7QMl+Bl<_f zWk)QA2i=Ys^beQIrnS4be|$E1jGq$uqN(J-x{_^!CA@<2rK)Flmc%l-2Tz$*MiUYP z!~iis46GLe<{YqE>s2;YOAHVLKVSg&2LTPyF<59+TL*mb`i%ZMA`0mEmOvB+9fO5N z@PKfg3aC@Ld17##4t8PU9D{{MozA$L8OAX)myZ{&W(T`a;fy;P=}Qa{1FHJaA`EHvUMXjkcgbP-U5(1#fK1qMC !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/cadence/insn_assert2.sv b/scripts/slec/cadence/insn_assert2.sv new file mode 100755 index 000000000..eb4eae11d --- /dev/null +++ b/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 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