From 162574dbbcc8eb1a9ebc2d8690ba2f08289a1e5a Mon Sep 17 00:00:00 2001 From: mret55 Date: Wed, 12 Jun 2024 10:13:07 -0500 Subject: [PATCH 01/11] 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 From 62c8b5706c10495e1152f3c42928f61181a77a04 Mon Sep 17 00:00:00 2001 From: mret55 Date: Wed, 12 Jun 2024 10:31:13 -0500 Subject: [PATCH 02/11] Update README.rtf Added license headers --- scripts/slec/cadence/README.rtf | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/scripts/slec/cadence/README.rtf b/scripts/slec/cadence/README.rtf index d3149678c..e87d58f4c 100644 --- a/scripts/slec/cadence/README.rtf +++ b/scripts/slec/cadence/README.rtf @@ -5,4 +5,7 @@ \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. } \ No newline at end of file +\f0\fs24 \cf0 +// Copyright 2024 +// SPDX-License-Identifier: Apache-2.0 WITH SHL-2.1 +Add assume (data_assert2.sv and insn_assert2.sv) files and bind (cv32e40p_bind2.sv) files to flist file inside rtl directory. } From cc3fe8820019c732da8e4a28f86695dc4e60fef3 Mon Sep 17 00:00:00 2001 From: mret55 Date: Wed, 12 Jun 2024 11:13:25 -0500 Subject: [PATCH 03/11] Delete .DS_Store --- .DS_Store | Bin 6148 -> 0 bytes 1 file changed, 0 insertions(+), 0 deletions(-) delete mode 100644 .DS_Store diff --git a/.DS_Store b/.DS_Store deleted file mode 100644 index 63bf7aa6876ce38bea71a860508bbfd474d0df7b..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 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@*j1qMC Date: Wed, 12 Jun 2024 11:13:56 -0500 Subject: [PATCH 04/11] Delete scripts/.DS_Store --- scripts/.DS_Store | Bin 6148 -> 0 bytes 1 file changed, 0 insertions(+), 0 deletions(-) delete mode 100644 scripts/.DS_Store diff --git a/scripts/.DS_Store b/scripts/.DS_Store deleted file mode 100644 index 8c27bc4ef30fc668d0b973a03da2bd8c873401b5..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 6148 zcmeHK-AcnS6i&9ODMRRm!Y%{e4&2;OhBsx-7qFriDzkM(i?tbR=Pt&e*ZM*}iO=IX zNh%KKt%y4ZlJEQ`%?Hg7V~qEwqc&qMV@yCpzjaZ9B1e@=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(=3D Date: Wed, 12 Jun 2024 11:14:20 -0500 Subject: [PATCH 05/11] Delete scripts/slec/.DS_Store --- scripts/slec/.DS_Store | Bin 6148 -> 0 bytes 1 file changed, 0 insertions(+), 0 deletions(-) delete mode 100644 scripts/slec/.DS_Store diff --git a/scripts/slec/.DS_Store b/scripts/slec/.DS_Store deleted file mode 100644 index f2ae0c143dd6d53d55c93ef3c92e36c68b5b6133..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 6148 zcmeHK%}T>S5Z<-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 Date: Sun, 16 Jun 2024 16:41:47 -0500 Subject: [PATCH 06/11] Changes made to run.sh. Added a new folder for assume and bind files --- .DS_Store | Bin 6148 -> 6148 bytes scripts/.DS_Store | Bin 6148 -> 6148 bytes scripts/formal/fpv.tcl | 23 ++++++++++++++++++ scripts/slec/.DS_Store | Bin 6148 -> 6148 bytes scripts/slec/cadence/.DS_Store | Bin 0 -> 6148 bytes scripts/slec/cadence/README.rtf | 11 --------- scripts/slec/run.sh | 8 ++++-- .../{cadence => tb_src}/cv32e40p_bind2.sv | 3 ++- scripts/slec/tb_src/cv32e40p_tb_src.flist | 5 ++++ .../slec/{cadence => tb_src}/data_assert2.sv | 3 ++- .../slec/{cadence => tb_src}/insn_assert2.sv | 3 ++- 11 files changed, 40 insertions(+), 16 deletions(-) create mode 100755 scripts/formal/fpv.tcl create mode 100644 scripts/slec/cadence/.DS_Store delete mode 100644 scripts/slec/cadence/README.rtf rename scripts/slec/{cadence => tb_src}/cv32e40p_bind2.sv (82%) create mode 100755 scripts/slec/tb_src/cv32e40p_tb_src.flist rename scripts/slec/{cadence => tb_src}/data_assert2.sv (93%) rename scripts/slec/{cadence => tb_src}/insn_assert2.sv (93%) diff --git a/.DS_Store b/.DS_Store index 63bf7aa6876ce38bea71a860508bbfd474d0df7b..242e80be6ae7704ac4d84d8d134d6c20910f6cc3 100644 GIT binary patch delta 21 ccmZoMXffC@kCDU7)JR9c(9CG_GR8PD07o_k5C8xG delta 21 ccmZoMXffC@kCDUB#8OAW*xYjSGR8PD07rKQ8vpB)qu~2NHo}wrV0|Nsi1A_nqLn1>?Qh9MfQcix-W=5vvjDjF3Hik5Y ze1;;1T#)o+3C0EvGgBiS1w%8V$qN|mB~hfyf{XHU^7GO`CQjyI?13xYynwNsWivYm cKL^lWpxNJB`mu~2NHo}wrd0|Nsi1A_oVQh9MfQcivnkiTPM;qu7_A}o{tGj(zp xnpo;67@J#ep1@qrvWevb<7Rdaeh#1kn?EvtXP(S2V#xv20y2YXbAZSeW&pc(7&rg` 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/slec/.DS_Store b/scripts/slec/.DS_Store index f2ae0c143dd6d53d55c93ef3c92e36c68b5b6133..a11e29eb8e1248bcec41b77bd9b7f747c40ac091 100644 GIT binary patch delta 162 zcmZoMXfc=|#>B)qu~2NHo+2a5#DLw41(+BaStj!^>N9dowqcCs=j4nRkf^RUGd0pt zFf=ooyo@oHmyMx>A&DWLp_rkFA$hVKqbyFf_L3-S%YuvYa`N-i85kHCH#0JcvutMP d;O79k0Lb~yJegm_l7kT_1(ask93ZlV8321$B6B`mu~2NHo+2aD#DLwC4MbQb^E2r%vQO4yj^^j!j2Doot~NBW)KM@t zx12nK*?#gH1@V-^m;4Wg<&0T*E43hX&L&p$$qDprKhvt+--jT7}7np#A3 zem<@ulZcFPQ@L2!n>{z**++&mCkOWA81W14cNZlEfg7;MkzE(HCqgga^y>{tEnwC%0;vJ&^%eQ zLs35+`xjp>T0 -// SPDX-License-Identifier: Apache-2.0 WITH SHL-2.1 -Add assume (data_assert2.sv and insn_assert2.sv) files and bind (cv32e40p_bind2.sv) files to flist file inside rtl directory. } 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/cadence/cv32e40p_bind2.sv b/scripts/slec/tb_src/cv32e40p_bind2.sv similarity index 82% rename from scripts/slec/cadence/cv32e40p_bind2.sv rename to scripts/slec/tb_src/cv32e40p_bind2.sv index a680024a1..b12dc0af8 100755 --- a/scripts/slec/cadence/cv32e40p_bind2.sv +++ b/scripts/slec/tb_src/cv32e40p_bind2.sv @@ -1,4 +1,5 @@ - +// Copyright 2024 Cirrus Logic +// SPDX-License-Identifier: Apache-2.0 WITH SHL-2.1 bind cv32e40p_top insn_assert u_insn_assert ( .clk_i(clk_i), .rst_ni(rst_ni), 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/cadence/data_assert2.sv b/scripts/slec/tb_src/data_assert2.sv similarity index 93% rename from scripts/slec/cadence/data_assert2.sv rename to scripts/slec/tb_src/data_assert2.sv index a5c7cb58d..59ba22d7a 100755 --- a/scripts/slec/cadence/data_assert2.sv +++ b/scripts/slec/tb_src/data_assert2.sv @@ -1,4 +1,5 @@ - +// Copyright 2024 Cirrus Logic +// SPDX-License-Identifier: Apache-2.0 WITH SHL-2.1 module data_assert ( input logic clk_i, input logic rst_ni, diff --git a/scripts/slec/cadence/insn_assert2.sv b/scripts/slec/tb_src/insn_assert2.sv similarity index 93% rename from scripts/slec/cadence/insn_assert2.sv rename to scripts/slec/tb_src/insn_assert2.sv index eb4eae11d..19d081066 100755 --- a/scripts/slec/cadence/insn_assert2.sv +++ b/scripts/slec/tb_src/insn_assert2.sv @@ -1,4 +1,5 @@ - +// Copyright 2024 Cirrus Logic +// SPDX-License-Identifier: Apache-2.0 WITH SHL-2.1 module insn_assert ( input logic clk_i, input logic rst_ni, From 5f5dc4e888adfffdb93cc2d1a00c0f402501c497 Mon Sep 17 00:00:00 2001 From: mret55 Date: Sun, 16 Jun 2024 16:46:03 -0500 Subject: [PATCH 07/11] Delete scripts/slec/.DS_Store --- scripts/slec/.DS_Store | Bin 6148 -> 0 bytes 1 file changed, 0 insertions(+), 0 deletions(-) delete mode 100644 scripts/slec/.DS_Store diff --git a/scripts/slec/.DS_Store b/scripts/slec/.DS_Store deleted file mode 100644 index a11e29eb8e1248bcec41b77bd9b7f747c40ac091..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 6148 zcmeHK!AiqG5S^`66GZ4ip~nTU1#8uUcnP)sfDt{Y)T9X-jM>tp_D~8r>ks)QevdP| zTd}QPMP&wN-|Xy6!n_T;82}KSQM3n80{{n=u;SwIh0r?bl2ojxiYW9mGU!7bj`Km7 zE=9BBH!?tbw~o6OKm;*-+CLTI%4;}Cle}m)-$Z4ly1KURIL?N1$D$7j8V^f6P!_dSu73W3W_kPh$dCo7DJeH^h+D(Su72jbP%@r5cbW&b|^x> z9iK0CI0(-mkIVowFwek>nbzq3KmES{pHJc$Gr$b|D+WZh>vua?lD%7(ile($qTZsC pP+V#7BLxk86=N)2#dTCI=$B+5dKOEA=t1Eh0ZjuB%)pN_@DA?eiPHc8 From 84940f46156b794618fcd6178043ce35ba4e8559 Mon Sep 17 00:00:00 2001 From: mret55 Date: Sun, 16 Jun 2024 16:46:30 -0500 Subject: [PATCH 08/11] Delete scripts/.DS_Store --- scripts/.DS_Store | Bin 6148 -> 0 bytes 1 file changed, 0 insertions(+), 0 deletions(-) delete mode 100644 scripts/.DS_Store diff --git a/scripts/.DS_Store b/scripts/.DS_Store deleted file mode 100644 index ec8dc46ca3ac68a1c67bcfafa05e624472630239..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 6148 zcmeHK%}&BV5S|6pHpGO3CLA~MN+O_=7%vUt3s|EEHP{MjW9bqKav&r<>kIiLK94iI z3lY$(@nR8`wIIioqOXbO=aZs7T9NyEjp@{Nws&@qPTP-hFHz5iNP%Zg%cjK{yx?RZrzd}q#45Q*JH-?r zg&4YU`{Atq=3M9bEaf@lgOM3v2AF|m2JHRm6qh%6%?vOD|DFN5A0#TFXE8IVuMQk^ z3xG(!ky>z0y#&Qbi=M^IAnu?D6N+d;g>5l}2}irMexAk5pa}J From 06dc30f75d41bfe413e1e9d3dff155502ee2cbc6 Mon Sep 17 00:00:00 2001 From: mret55 Date: Sun, 16 Jun 2024 16:49:05 -0500 Subject: [PATCH 09/11] Delete scripts/slec/cadence/.DS_Store --- scripts/slec/cadence/.DS_Store | Bin 6148 -> 0 bytes 1 file changed, 0 insertions(+), 0 deletions(-) delete mode 100644 scripts/slec/cadence/.DS_Store diff --git a/scripts/slec/cadence/.DS_Store b/scripts/slec/cadence/.DS_Store deleted file mode 100644 index 5008ddfcf53c02e82d7eee2e57c38e5672ef89f6..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 6148 zcmeH~Jr2S!425mzP>H1@V-^m;4Wg<&0T*E43hX&L&p$$qDprKhvt+--jT7}7np#A3 zem<@ulZcFPQ@L2!n>{z**++&mCkOWA81W14cNZlEfg7;MkzE(HCqgga^y>{tEnwC%0;vJ&^%eQ zLs35+`xjp>T0 Date: Sun, 16 Jun 2024 16:50:10 -0500 Subject: [PATCH 10/11] Delete .DS_Store --- .DS_Store | Bin 6148 -> 0 bytes 1 file changed, 0 insertions(+), 0 deletions(-) delete mode 100644 .DS_Store diff --git a/.DS_Store b/.DS_Store deleted file mode 100644 index 242e80be6ae7704ac4d84d8d134d6c20910f6cc3..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 6148 zcmeHK%}T>S5T0$TO({YT3Oz1(E!b8qh?h|73mDOZN^NY>V9b^zHHT8jSzpK}@p+ut z-GJ2|Jc-yD*!^bbXE*af_6Gn&e>Uy_GyuTCMkq*GA!J_ZD%oH{q34)F3W=X3Q$JiW z(O)#tw^t#7JBT5GPv5V6^t}1gFi6sN`(2dEm5t4+<2ZHa#(PkimyXg|(jUcFG&)x* z^b39DUj&nE*w{W%Q925uNvsos@dQJzFN0{Tvc8%{<3#6r#^KazwPB+b6_*V86Fm)SR8&z2mdtWB3%Q7el2$*0pR|EZ`NDFI7EzaTKcP9z8`?5zWX9 zFayj0Gq7F^*mJ Date: Mon, 17 Jun 2024 08:15:32 -0500 Subject: [PATCH 11/11] Replaced headers in assume and bind files with the ones in formal dir. Uncommented the row4 trigger_match_i assertion from controller_assert file --- .../formal/src/cv32e40p_controller_assert.sv | 4 +-- scripts/slec/tb_src/cv32e40p_bind2.sv | 25 ++++++++++++++++++- scripts/slec/tb_src/data_assert2.sv | 25 ++++++++++++++++++- scripts/slec/tb_src/insn_assert2.sv | 25 ++++++++++++++++++- 4 files changed, 74 insertions(+), 5 deletions(-) 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/tb_src/cv32e40p_bind2.sv b/scripts/slec/tb_src/cv32e40p_bind2.sv index b12dc0af8..d328a24fa 100755 --- a/scripts/slec/tb_src/cv32e40p_bind2.sv +++ b/scripts/slec/tb_src/cv32e40p_bind2.sv @@ -1,5 +1,28 @@ -// Copyright 2024 Cirrus Logic +// 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), diff --git a/scripts/slec/tb_src/data_assert2.sv b/scripts/slec/tb_src/data_assert2.sv index 59ba22d7a..762057cc8 100755 --- a/scripts/slec/tb_src/data_assert2.sv +++ b/scripts/slec/tb_src/data_assert2.sv @@ -1,5 +1,28 @@ -// Copyright 2024 Cirrus Logic +// 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, diff --git a/scripts/slec/tb_src/insn_assert2.sv b/scripts/slec/tb_src/insn_assert2.sv index 19d081066..b04c01228 100755 --- a/scripts/slec/tb_src/insn_assert2.sv +++ b/scripts/slec/tb_src/insn_assert2.sv @@ -1,5 +1,28 @@ -// Copyright 2024 Cirrus Logic +// 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,