From b7434ba1dbadfe59fe116f9003f46073c2404781 Mon Sep 17 00:00:00 2001 From: Yoann Pruvost Date: Tue, 4 Jun 2024 14:21:42 +0800 Subject: [PATCH 01/29] Adding formal rule for coverage holes on controller --- bhv/cv32e40p_instr_trace.svh | 2 +- scripts/formal/cv32e40p_formal.flist | 1 + scripts/formal/formal.do | 46 +++++++------- scripts/formal/src/cv32e40p_bind.sv | 16 +++++ .../formal/src/cv32e40p_controller_assert.sv | 61 +++++++++++++++++++ 5 files changed, 102 insertions(+), 24 deletions(-) create mode 100644 scripts/formal/src/cv32e40p_controller_assert.sv diff --git a/bhv/cv32e40p_instr_trace.svh b/bhv/cv32e40p_instr_trace.svh index 355bc7382..95d0f90fa 100644 --- a/bhv/cv32e40p_instr_trace.svh +++ b/bhv/cv32e40p_instr_trace.svh @@ -802,7 +802,7 @@ class instr_trace_t; else str_hb = ".h"; // set mnemonic - case (instr) + casex (instr) INSTR_CVADDH , INSTR_CVADDSCH , INSTR_CVADDSCIH, diff --git a/scripts/formal/cv32e40p_formal.flist b/scripts/formal/cv32e40p_formal.flist index e3c5f1f2a..8fa39ad0f 100644 --- a/scripts/formal/cv32e40p_formal.flist +++ b/scripts/formal/cv32e40p_formal.flist @@ -28,6 +28,7 @@ src/data_assert.sv src/cv32e40p_assert.sv src/cv32e40p_ID_assert.sv src/cv32e40p_EX_assert.sv +src/cv32e40p_controller_assert.sv src/fpnew_divsqrt_th_32_assert.sv src/cv32e40p_formal_top.sv src/cv32e40p_bind.sv \ No newline at end of file diff --git a/scripts/formal/formal.do b/scripts/formal/formal.do index 8e0be6031..f2f037143 100644 --- a/scripts/formal/formal.do +++ b/scripts/formal/formal.do @@ -1,26 +1,26 @@ -// 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 // -// // -// Description: Formal script for CV32E40P // -// // -//////////////////////////////////////////////////////////////////////////////////// +# 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 // +# // +# Description: Formal script for CV32E40P // +# // +#////////////////////////////////////////////////////////////////////////////////// set top cv32e40p_formal_top diff --git a/scripts/formal/src/cv32e40p_bind.sv b/scripts/formal/src/cv32e40p_bind.sv index 38d51941a..e3a1b7b62 100644 --- a/scripts/formal/src/cv32e40p_bind.sv +++ b/scripts/formal/src/cv32e40p_bind.sv @@ -106,6 +106,22 @@ bind cv32e40p_ex_stage cv32e40p_EX_assert u_cv32e40p_EX_assert ( .apu_read_dep_for_jalr_o (apu_read_dep_for_jalr_o ) ); +bind cv32e40p_controller cv32e40p_controller_assert u_cv32e40p_controller_assert ( + .clk_i (clk_i ), + .rst_ni(rst_ni), + + .data_load_event_i (data_load_event_i ), + .trigger_match_i (trigger_match_i ), + .ebrk_insn_i (ebrk_insn_i ), + .debug_mode_q (debug_mode_q ), + .debug_req_entry_q (debug_req_entry_q ), + .ebrk_force_debug_mode(ebrk_force_debug_mode), + .debug_force_wakeup_q (debug_force_wakeup_q ), + .debug_single_step_i (debug_single_step_i ), + .data_err_i (data_err_i ), + .ctrl_fsm_cs (ctrl_fsm_cs ) +); + bind fpnew_divsqrt_th_32 fpnew_divsqrt_th_32_assert u_fpnew_divsqrt_th_32_assert ( .clk_i (clk_i), .rst_ni(rst_ni), diff --git a/scripts/formal/src/cv32e40p_controller_assert.sv b/scripts/formal/src/cv32e40p_controller_assert.sv new file mode 100644 index 000000000..47a41d715 --- /dev/null +++ b/scripts/formal/src/cv32e40p_controller_assert.sv @@ -0,0 +1,61 @@ +// 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 // +// // +// Description: Assertion for unreachable code in CV32E40P controller // +// // +//////////////////////////////////////////////////////////////////////////////////// + +module cv32e40p_controller_assert import cv32e40p_pkg::*; +( + input logic clk_i, + input logic rst_ni, + + input logic data_load_event_i, + input logic trigger_match_i, + input logic ebrk_insn_i, + input logic debug_mode_q, + input logic debug_req_entry_q, + input logic ebrk_force_debug_mode, + input logic debug_force_wakeup_q, + input logic debug_single_step_i, + input logic data_err_i, + input ctrl_state_e ctrl_fsm_cs +); + + property all_true_ctrl_1187_1189_and_1191; + @(posedge clk_i) disable iff(!rst_ni) + ((ctrl_fsm_cs == DBG_TAKEN_ID) && ~debug_mode_q) |-> (trigger_match_i | (ebrk_force_debug_mode & ebrk_insn_i) | debug_req_entry_q); + endproperty + + property all_true_ctrl_1210_and_1212; + @(posedge clk_i) disable iff(!rst_ni) + (ctrl_fsm_cs == DBG_TAKEN_IF) |-> (debug_force_wakeup_q | debug_single_step_i); + endproperty + + property unreachable_ctrl_1241_row_10; + @(posedge clk_i) disable iff(!rst_ni) + ((ctrl_fsm_cs == DBG_FLUSH) && !data_err_i) && (~debug_req_entry_q && ~((debug_mode_q | trigger_match_i) | (ebrk_force_debug_mode & ebrk_insn_i))) |-> !data_load_event_i; + endproperty + + 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); + assert_unreachable_ctrl_1241_row_10: assert property(unreachable_ctrl_1241_row_10); + +endmodule \ No newline at end of file From c581a90ea5e280f14cf33ee71538aa70b2102a50 Mon Sep 17 00:00:00 2001 From: Yoann Pruvost Date: Thu, 6 Jun 2024 15:37:34 +0800 Subject: [PATCH 02/29] Adding more assertions for code coverage holes in controller --- scripts/formal/src/cv32e40p_controller_assert.sv | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/scripts/formal/src/cv32e40p_controller_assert.sv b/scripts/formal/src/cv32e40p_controller_assert.sv index 47a41d715..6eab1dd7a 100644 --- a/scripts/formal/src/cv32e40p_controller_assert.sv +++ b/scripts/formal/src/cv32e40p_controller_assert.sv @@ -49,6 +49,16 @@ module cv32e40p_controller_assert import cv32e40p_pkg::*; (ctrl_fsm_cs == DBG_TAKEN_IF) |-> (debug_force_wakeup_q | debug_single_step_i); endproperty + property unreachable_ctrl_1241_row_4; + @(posedge clk_i) disable iff(!rst_ni) + ((ctrl_fsm_cs == DBG_FLUSH) && !data_err_i) && (~debug_req_entry_q && ~data_load_event_i && ~(ebrk_force_debug_mode & ebrk_insn_i) && ~debug_mode_q) |-> ~trigger_match_i; + endproperty + + property unreachable_ctrl_1241_row_5; + @(posedge clk_i) disable iff(!rst_ni) + ((ctrl_fsm_cs == DBG_FLUSH) && !data_err_i) && (~debug_req_entry_q && ~data_load_event_i && ~(debug_mode_q | trigger_match_i) && ebrk_insn_i) |-> ebrk_force_debug_mode; + endproperty + property unreachable_ctrl_1241_row_10; @(posedge clk_i) disable iff(!rst_ni) ((ctrl_fsm_cs == DBG_FLUSH) && !data_err_i) && (~debug_req_entry_q && ~((debug_mode_q | trigger_match_i) | (ebrk_force_debug_mode & ebrk_insn_i))) |-> !data_load_event_i; @@ -56,6 +66,9 @@ 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_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 From 54558a8a23c000bbf99785e3e202a1703bec5270 Mon Sep 17 00:00:00 2001 From: Yoann Pruvost Date: Thu, 6 Jun 2024 15:40:32 +0800 Subject: [PATCH 03/29] RVFI - Correction corner case conflict on mstatus_fs upades when integer load followed by fpu instr --- bhv/cv32e40p_rvfi.sv | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/bhv/cv32e40p_rvfi.sv b/bhv/cv32e40p_rvfi.sv index 99429d90d..05e2a588b 100644 --- a/bhv/cv32e40p_rvfi.sv +++ b/bhv/cv32e40p_rvfi.sv @@ -1640,7 +1640,8 @@ insn_trace_t trace_if, trace_id, trace_ex, trace_ex_next, trace_wb; trace_wb.m_rd_wdata[0] = r_pipe_freeze_trace.rf_wdata_wb; end - if (r_pipe_freeze_trace.csr.fregs_we) begin + // if (r_pipe_freeze_trace.csr.fregs_we) begin + if(r_pipe_freeze_trace.csr.fregs_we && r_pipe_freeze_trace.rf_we_wb && r_pipe_freeze_trace.rf_addr_wb[5]) begin //Catching mstatus updates caused by flw `CSR_FROM_PIPE(wb, mstatus_fs) trace_wb.m_csr.mstatus_fs_we = 1'b1; trace_wb.m_csr.mstatus_fs_wmask = '1; From b281ced1c8fe9d2b6b33bae4ac7538ec9d06a5d7 Mon Sep 17 00:00:00 2001 From: Yoann Pruvost Date: Thu, 6 Jun 2024 15:43:40 +0800 Subject: [PATCH 04/29] Running verible --- bhv/cv32e40p_rvfi.sv | 1 - 1 file changed, 1 deletion(-) diff --git a/bhv/cv32e40p_rvfi.sv b/bhv/cv32e40p_rvfi.sv index 05e2a588b..0344319bb 100644 --- a/bhv/cv32e40p_rvfi.sv +++ b/bhv/cv32e40p_rvfi.sv @@ -1640,7 +1640,6 @@ insn_trace_t trace_if, trace_id, trace_ex, trace_ex_next, trace_wb; trace_wb.m_rd_wdata[0] = r_pipe_freeze_trace.rf_wdata_wb; end - // if (r_pipe_freeze_trace.csr.fregs_we) begin if(r_pipe_freeze_trace.csr.fregs_we && r_pipe_freeze_trace.rf_we_wb && r_pipe_freeze_trace.rf_addr_wb[5]) begin //Catching mstatus updates caused by flw `CSR_FROM_PIPE(wb, mstatus_fs) trace_wb.m_csr.mstatus_fs_we = 1'b1; From 162574dbbcc8eb1a9ebc2d8690ba2f08289a1e5a Mon Sep 17 00:00:00 2001 From: mret55 Date: Wed, 12 Jun 2024 10:13:07 -0500 Subject: [PATCH 05/29] 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 06/29] 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 07/29] 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 08/29] 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 09/29] 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 10/29] 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 11/29] 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 12/29] 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 13/29] 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 14/29] 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 15/29] 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, From 2ceb84fdf36a39a60fafbb60c436c6c0a289edad Mon Sep 17 00:00:00 2001 From: Pascal Gouedo Date: Thu, 6 Jun 2024 17:27:08 +0200 Subject: [PATCH 16/29] RISC-V ISA Formal Verification files for SiemensEDA OneSpin tool. Signed-off-by: Pascal Gouedo --- scripts/riscv_isa_formal/Makefile | 59 ++ scripts/riscv_isa_formal/README.md | 50 ++ .../riscv_isa_formal/common/constraints.sv | 119 ++++ .../riscv_isa_formal/common/core_checker.sv | 21 + scripts/riscv_isa_formal/common/io.sv | 72 +++ .../riscv_isa_formal/common/other_bindings.sv | 72 +++ scripts/riscv_isa_formal/common/setup.tcl | 564 ++++++++++++++++++ scripts/riscv_isa_formal/common/setup_mv.tcl | 8 + scripts/riscv_isa_formal/common/t.sh | 12 + .../riscv_isa_formal/common/vips/obi_dmem.sv | 60 ++ .../riscv_isa_formal/common/vips/obi_imem.sv | 59 ++ .../riscv_isa_formal/launch_command example | 58 ++ 12 files changed, 1154 insertions(+) create mode 100755 scripts/riscv_isa_formal/Makefile create mode 100755 scripts/riscv_isa_formal/README.md create mode 100755 scripts/riscv_isa_formal/common/constraints.sv create mode 100755 scripts/riscv_isa_formal/common/core_checker.sv create mode 100755 scripts/riscv_isa_formal/common/io.sv create mode 100755 scripts/riscv_isa_formal/common/other_bindings.sv create mode 100755 scripts/riscv_isa_formal/common/setup.tcl create mode 100755 scripts/riscv_isa_formal/common/setup_mv.tcl create mode 100755 scripts/riscv_isa_formal/common/t.sh create mode 100755 scripts/riscv_isa_formal/common/vips/obi_dmem.sv create mode 100755 scripts/riscv_isa_formal/common/vips/obi_imem.sv create mode 100755 scripts/riscv_isa_formal/launch_command example diff --git a/scripts/riscv_isa_formal/Makefile b/scripts/riscv_isa_formal/Makefile new file mode 100755 index 000000000..f344b819b --- /dev/null +++ b/scripts/riscv_isa_formal/Makefile @@ -0,0 +1,59 @@ +commonPath=../../common +PREPARE?=0 +RTL?=../../cv32e40p/ +GUI?=0 +NAME?=noname + +ifeq ($(APP),) + $(error APP is empty) +endif +ifeq ($(CONF),) + $(error CONF is empty) +endif +ifeq ($(MODE),) + $(error MODE is empty) +endif + +$(info APP=$(APP)) +$(info CONF=$(CONF)) +$(info MODE=$(MODE)) + +ifeq ($(GUI), 1) + flag="-i" +else + flag= +endif + +dirname=$(NAME) + +ifeq ($(PREPARE), 1) + script_name=ones_prepare_run +else + script_name=ones_run +endif + +define ones_prepare_run + @echo "====================================================" + @echo "Preparing working area $(dirname)" + @echo "====================================================" + \mkdir -p cfgs/$(dirname)/logs + \cd cfgs/$(dirname) && \cp -pf $(commonPath)/{other_bindings.sv,core_checker.sv,io.sv,setup.tcl,setup_mv.tcl,*.json,constraints.sv,t.sh,basics.tcl.obf} . && \cp -prfL $(commonPath)/vips . && \cp -prfL $(RTL) . + @echo "====================================================" + @echo "Running mode $(MODE) on configuration $(CONF) in $(dirname)" + @echo "====================================================" + \cd cfgs/$(dirname) && onespin -Q -l logs/$(APP)-cfg_$(CONF)-mode_$(MODE).log $(flag) setup.tcl $(CONF) $(MODE) $(APP) +endef + +define ones_run + @echo "====================================================" + @echo "Running mode $(MODE) on configuration $(CONF) in $(dirname)" + @echo "====================================================" + \cd cfgs/$(dirname) && onespin -Q -l logs/$(APP)-cfg_$(CONF)-mode_$(MODE).log $(flag) setup.tcl $(CONF) $(MODE) $(APP) +endef + +all: + $(call $(script_name)) + +clean: + rm -rf cfgs/$(dirname) + diff --git a/scripts/riscv_isa_formal/README.md b/scripts/riscv_isa_formal/README.md new file mode 100755 index 000000000..84ab2f05e --- /dev/null +++ b/scripts/riscv_isa_formal/README.md @@ -0,0 +1,50 @@ +# RISC-V ISA Formal Verification + +RISC-V ISA Formal Verification methodology has been used with Siemens EDA Onespin tool and its RISC-V ISA Processor Verification app. + +## Configurations + + | Top Parameters | XP | XPF0 | XPF1 | XPF2 | XPZF0 | XPZF1 | XPZF2 | + | :----------------- | :----: |:-------: | :------: | :------: | :-------: | :-------: | :-------: | + | COREV_PULP | 1 | 1 | 1 | 1 | 1 | 1 | 1 | + | COREV_CLUSTER | 0 | 0 | 0 | 0 | 0 | 0 | 0 | + | FPU | 0 | 1 | 1 | 1 | 1 | 1 | 1 | + | ZFINX | 0 | 0 | 0 | 0 | 1 | 1 | 1 | + | FPU_ADDMUL_LAT | 0 | 0 | 1 | 2 | 0 | 1 | 2 | + | FPU_OTHERS_LAT | 0 | 0 | 1 | 2 | 0 | 1 | 2 | + +## Tool apps + +- PRC : Property Checking +- QTF : Quantify +- VCI : Verification Coverage Integration + +## Prove modes + +- DEF : Control path verification of all instructions and datapath verification of all instructions except multiplication, division or floating point ones +- DPM : Data path verification of multiplication/ division instructions +- DPF : Data path verification of floating-point instructions + +## Directory Structure of this Repo + +- Makefile +- launch_command_example + +### common +Contains all files to create assertions and to launch different tool apps on different configurations and using different modes. + +> [!CAUTION] +> core_checker.sv contains proprietary information and is only available to Siemens EDA OneSpin customers. +> Once OneSpin licenses have been purchased, this file can be requested to Siemens support center. + +## How to launch a run + +- Locally clone cv32e40p github repository or make a symbolic link to an existing repo. +- launch following command:
+ make GUI=1 APP=PRC CONF=XP MODE=DEF NAME=v1_8_0 VERBOSE=1 PREPARE=1 all >&! run_gui-PRC-cfg_XP-mode_DEF-v1_8_0.log +- or use launch_command_example to launch different runs in parallel. + +## Commands to launch assertion checks for each configuration + +- XP : PRC app with DEF and DPM modes +- XPF[0,1,2] and XPZF[0,1,2] : PRC app with DEF, DPM and DPF modes diff --git a/scripts/riscv_isa_formal/common/constraints.sv b/scripts/riscv_isa_formal/common/constraints.sv new file mode 100755 index 000000000..02bf694d0 --- /dev/null +++ b/scripts/riscv_isa_formal/common/constraints.sv @@ -0,0 +1,119 @@ +/*********************/ +// CONSTRAINTS +/*********************/ + +// MAIN CONSTRAINTS // + +const_addrs_c : assume property (##1 $stable({boot_addr,`core.dm_halt_addr_i,`core.dm_exception_addr_i,`core.mtvec_addr_i,`core.hart_id_i})); +const_dm_addr_c : assume property (`core.dm_halt_addr_i==32'h800 && `core.dm_exception_addr_i==32'h808); // **I** To meet app expectations + +`ifdef CFG_XP +`ifdef CV_LOOP + // raising of hwloop illegal currently not modeled + no_hwloop_illegal_c : assume property (!id_stage_i.controller_i.is_hwlp_illegal); + + // hwloop must contain 3+ instructions + hwloop_min_size_c : assume property (!(id_stage_i.gen_hwloop_regs.hwloop_regs_i.hwlp_counter_q[0]>0&&id_stage_i.gen_hwloop_regs.hwloop_regs_i.hwlp_end_q[0]-id_stage_i.gen_hwloop_regs.hwloop_regs_i.hwlp_start_q[0] inside {32'h0,32'h4,32'h8}) && !(id_stage_i.gen_hwloop_regs.hwloop_regs_i.hwlp_counter_q[1]>0&&id_stage_i.gen_hwloop_regs.hwloop_regs_i.hwlp_end_q[1]-id_stage_i.gen_hwloop_regs.hwloop_regs_i.hwlp_start_q[1] inside {32'h0,32'h4,32'h8})); + + // hwloop must be word-aligned + hwloop_aligned_c : assume property (id_stage_i.gen_hwloop_regs.hwloop_regs_i.hwlp_start_q[0][1:0]==0 && id_stage_i.gen_hwloop_regs.hwloop_regs_i.hwlp_end_q[0][1:0]==0 && id_stage_i.gen_hwloop_regs.hwloop_regs_i.hwlp_start_q[1][1:0]==0 && id_stage_i.gen_hwloop_regs.hwloop_regs_i.hwlp_end_q[1][1:0]==0); + + // we must not create loop 0 in the middle of itself (setting count to non-zero at a PC location that would qualify as inside the loop). Also, setting up the registers and then jumping to a location inside loop 0 will likely not work + loop0_setup_c : assume property (id_stage_i.gen_hwloop_regs.hwloop_regs_i.hwlp_counter_q[0]==0 ##1 id_stage_i.gen_hwloop_regs.hwloop_regs_i.hwlp_counter_q[0]!=0 |-> id_stage_i.gen_hwloop_regs.hwloop_regs_i.hwlp_start_q[0]==$past(pc_id)+32'd4); + + // we must not create loop 1 in the middle of itself (setting count to non-zero at a PC location that would qualify as inside the loop). Also, setting up the registers and then jumping to a location inside loop 1 will likely not work + loop1_setup_c : assume property (id_stage_i.gen_hwloop_regs.hwloop_regs_i.hwlp_counter_q[1]==0 ##1 id_stage_i.gen_hwloop_regs.hwloop_regs_i.hwlp_counter_q[1]!=0 |-> id_stage_i.gen_hwloop_regs.hwloop_regs_i.hwlp_start_q[1]==$past(pc_id)+32'd4); + + // let's not wrap + lopp_no_wrap_c : assume property (!(id_stage_i.gen_hwloop_regs.hwloop_regs_i.hwlp_counter_q[0]>0&&id_stage_i.gen_hwloop_regs.hwloop_regs_i.hwlp_end_q[0]0&&id_stage_i.gen_hwloop_regs.hwloop_regs_i.hwlp_end_q[1]0 && pc_id>=id_stage_i.gen_hwloop_regs.hwloop_regs_i.hwlp_start_q[0] && pc_id0 && pc_id>=id_stage_i.gen_hwloop_regs.hwloop_regs_i.hwlp_start_q[1] && pc_id0 && id_stage_i.hwlp_regid==1 && id_stage_i.hwlp_we)); + + // end addresses 8 apart + loop_end_min_sitance_c : assume property (!(id_stage_i.gen_hwloop_regs.hwloop_regs_i.hwlp_counter_q[0]>0 && id_stage_i.gen_hwloop_regs.hwloop_regs_i.hwlp_counter_q[1]>0 && id_stage_i.gen_hwloop_regs.hwloop_regs_i.hwlp_end_q[1]0 && id_stage_i.gen_hwloop_regs.hwloop_regs_i.hwlp_we_i[1] && !id_stage_i.gen_hwloop_regs.hwloop_regs_i.hwlp_regid_i &&id_stage_i.gen_hwloop_regs.hwloop_regs_i.hwlp_end_q[1]0|->`core.data_rvalid_i); +`else + no_hwloop_c : assume property (!id_stage_i.controller_i.is_hwlp_body); +`endif +`endif + +`ifdef CFG_XC + clk_en_c: assume property (`core.pulp_clock_en_i); +`endif + +// MEMORY INTERFACE CONSTRAINTS // + +// +// The following set of constraints could be used to constrain memory interfaces in case bus protocols implemented are not tool supported. +// **W** Use only in case bus protocols implemented are not tool supported +// + +`ifdef CUSTOM_MEM_INTERFACES + `include "mem_constraints.sv" + localparam MAX_WAIT=DMEM_MAX_WAIT; +`else + localparam MAX_WAIT=obi_dmem_checker.MAX_WAIT; +`endif + +// PERFORMANCE ENHANCEMENT CONSTRAINTS // + +// +// The following set of constraints could be used to enhance properties' runtime. +// **W** If ever used, these constraints have to be removed totally afterwards to achieve full verification. +// + +// +// "restrict_regs" restricts instruction source and destination indices to a subset of registers. +// By default, the following register indices are chosen: 0 to 3, and 8 to 9 in presence of compressed extensions. +// +function automatic restrict_regs(input dec_t dec); + restrict_regs=1'b1; + foreach (dec.RS[i]) + if (dec.RS[i].valid) +// restrict_regs&=dec.RS[i].idx<4 || (MISA.C|Zca) && dec.RS[i].idx inside {5'd8,5'd9}; + restrict_regs&=dec.RS[i].idx inside {5'd0, 5'd1, 5'd2, 5'd4, 5'd8, 5'd12, 5'd16}; + foreach (dec.RD[i]) + if (dec.RD[i].valid) +// restrict_regs&=dec.RD[i].idx<4 || (MISA.C|Zca) && dec.RD[i].idx inside {5'd8,5'd9}; + restrict_regs&=dec.RD[i].idx inside {5'd0, 5'd1, 5'd2, 5'd4, 5'd8, 5'd12, 5'd16}; +endfunction + +`ifdef RESTRICT_REGS + // Restrict instruction decoding & register file verification to a subset of registers + restrict_regs_c: assume property (disable iff (~rst_n) + restrict_regs(execute.dec) + `ifndef COMPLETENESS + `ifndef RESTRICT_REGISTER_INDEX +// && (reg_idx<4 || (MISA.C|Zca) && reg_idx inside {5'd8,5'd9}) + && (reg_idx inside {5'd0, 5'd1, 5'd2, 5'd4, 5'd8, 5'd12, 5'd16}) + `endif + `endif + ); +`endif + +// GRADUAL VERIFICATION CONSTRAINTS // + +// +// The following set of constraints could be used for a gradual setup of a new core. +// **W** If ever used, these constraints have to be removed totally afterwards to achieve full verification. +// + +`ifdef LIMIT_TOTAL_INSTR_COUNT + // Limit total number of instructions allowed in the pipeline + limit_total_instr_count_c : assume property (disable iff (~rst_n) full[0] -> id_instr_cnt<`LIMIT_TOTAL_INSTR_COUNT); +`endif diff --git a/scripts/riscv_isa_formal/common/core_checker.sv b/scripts/riscv_isa_formal/common/core_checker.sv new file mode 100755 index 000000000..74755ca9f --- /dev/null +++ b/scripts/riscv_isa_formal/common/core_checker.sv @@ -0,0 +1,21 @@ +/////////////////////////////////////////////////////////////////////////////// +// // +// RISC-V Checker // +// // +// This material contains trade secrets or otherwise confidential // +// information owned by Siemens Industry Software Inc. or its affiliates // +// (collectively, "SISW"), or its licensors. Access to and use of this // +// information is strictly limited as set forth in the Customer's applicable // +// agreements with SISW. // +// // +// This material may not be copied, distributed, or otherwise disclosed // +// outside of the Customer's facilities without the express written // +// permission of SISW, and may not be used in any way not expressly // +// authorized by SISW. // +// // +/////////////////////////////////////////////////////////////////////////////// + + + + +This file is available only to Siemens EDA OneSpin customers and is available by submitting a request to Siemens support center to get it. diff --git a/scripts/riscv_isa_formal/common/io.sv b/scripts/riscv_isa_formal/common/io.sv new file mode 100755 index 000000000..cb7c9c1e2 --- /dev/null +++ b/scripts/riscv_isa_formal/common/io.sv @@ -0,0 +1,72 @@ + // Data memory interface + input dmem_req_we ='0, // Data memory request type + input[3:0] dmem_req_be ='0, // Data memory request byte enable + input[1:0] dmem_req_size ='0, // Data memory request size + input dmem_req_sign ='0, // Data memory request sign + + // Exceptions & Debug + input is_sstep ='0, // Single stepping of debug mode + input xcpt_bp_if ='0, // Instruction address breakpoint exception + input xcpt_bp_ld ='0, // Load address breakpoint exception + input xcpt_bp_samo ='0, // Store/ AMO address breakpoint exception + input xcpt_dbg_bp_if ='0, // Debug instruction address breakpoint exception + input xcpt_dbg_bp_ld ='0, // Debug load address breakpoint exception + input xcpt_dbg_bp_samo ='0, // Debug Store/ AMO address breakpoint exception + input xcpt_af_instr_1st ='0, // Instruction access fault exception + input xcpt_af_instr_2nd ='0, // Instruction second access fault exception + input xcpt_af_ld_1st ='0, // Load access fault exception + input xcpt_af_ld_2nd ='0, // Load second access fault exception + input xcpt_af_samo_1st ='0, // Store/ AMO access fault exception + input xcpt_af_samo_2nd ='0, // Store/ AMO second access fault exception + input xcpt_pf_instr_1st ='0, // Instruction page fault exception + input xcpt_pf_instr_2nd ='0, // Instruction second access page fault exception + input xcpt_pf_ld_1st ='0, // Load page fault exception + input xcpt_pf_ld_2nd ='0, // Load second access page fault exception + input xcpt_pf_samo_1st ='0, // Store/ AMO page fault exception + input xcpt_pf_samo_2nd ='0, // Store/ AMO second access page fault exception + input xcpt_ma_ld ='0, // Load address misaligned exception + input xcpt_ma_samo ='0, // Store/AMO address misaligned exception + + // Multiplication & Division + input mul_op_valid ='0, // Multiplication operation validity + input[XLEN-1:0] mul_op_a ='0, // Multiplication first source operand + input[XLEN-1:0] mul_op_b ='0, // Multiplication second source operand + input[XLEN-1:0] mul_op_c ='0, // Multiplication third source operand + input[XLEN-1:0] mul_result ='0, // Multiplication operation result + input mul_result_valid ='0, // Multiplication operation result validity + input div_op_valid ='0, // Division operation validity + input[XLEN-1:0] div_op_a ='0, // Division first source operand + input[XLEN-1:0] div_op_b ='0, // Division second source operand + input[$clog2(XLEN):0] div_op_b_shift ='0, // Division second source operand shift amount + input[XLEN-1:0] div_result ='0, // Division operation result + input div_result_valid ='0, // Division operation result validity + + // Floating point + input fpu_op_valid ='0, // FPU operation validity + input[XLEN-1:0] fpu_op_a ='0, // FPU first source operand + input[XLEN-1:0] fpu_op_b ='0, // FPU second source operand + input[XLEN-1:0] fpu_op_c ='0, // FPU third source operand + input Frm fpu_rm ='0, // FPU rounding mode + input Fflags fpu_flags ='0, // FPU flags + input[XLEN-1:0] fpu_result ='0, // FPU operation result + input fpu_result_valid ='0, // FPU operation result validity + + // Design specific + input is_debug ='0, // Core is about to enter debug mode + input is_interrupt ='0, // Core is about to encounter an interrupt + input[XLEN-1:0] boot_addr ='0, // Boot address + + input rf_we_lsu ='0, + input[5:0] rf_waddr_lsu ='0, + input[1:0] lsu_data_type ='0, + input[1:0] lsu_data_sign ='0, + input[1:0] lsu_data_offset ='0, + input fpu_s_cycle ='0, + input fpu_m_cycle ='0, + input[5:0] fpu_waddr ='0, + input[5:0] fpu_waddr_ex ='0, + input[1:0] fpu_lat_ex ='0, + input[5:0] fpu_op_ex ='0, + input[XLEN-1:0] dot_mul_op_a ='0, + input[XLEN-1:0] dot_mul_op_b ='0, + input[XLEN-1:0] dot_mul_op_c ='0 diff --git a/scripts/riscv_isa_formal/common/other_bindings.sv b/scripts/riscv_isa_formal/common/other_bindings.sv new file mode 100755 index 000000000..41c929d20 --- /dev/null +++ b/scripts/riscv_isa_formal/common/other_bindings.sv @@ -0,0 +1,72 @@ + // Data memory interface + .dmem_req_we (data_we_o), + .dmem_req_be (data_be_o), + .dmem_req_size (), + .dmem_req_sign (), + + // Exceptions & Debug + .is_sstep (debug_single_step), + .xcpt_bp_if (), + .xcpt_bp_ld (), + .xcpt_bp_samo (), + .xcpt_dbg_bp_if (), + .xcpt_dbg_bp_ld (), + .xcpt_dbg_bp_samo (), + .xcpt_af_instr_1st (), + .xcpt_af_instr_2nd (), + .xcpt_af_ld_1st (), + .xcpt_af_ld_2nd (), + .xcpt_af_samo_1st (), + .xcpt_af_samo_2nd (), + .xcpt_pf_instr_1st (), + .xcpt_pf_instr_2nd (), + .xcpt_pf_ld_1st (), + .xcpt_pf_ld_2nd (), + .xcpt_pf_samo_1st (), + .xcpt_pf_samo_2nd (), + .xcpt_ma_ld (), + .xcpt_ma_samo (), + + // Multiplication & Division + .mul_op_valid (), + .mul_op_a (ex_stage_i.mult_i.op_a_i), + .mul_op_b (ex_stage_i.mult_i.op_b_i), + .mul_op_c (ex_stage_i.mult_i.op_c_i), + .mul_result (ex_stage_i.mult_i.result_o), + .mul_result_valid (), + .div_op_valid (), + .div_op_a (ex_stage_i.alu_i.alu_div_i.OpA_DI), + .div_op_b (ex_stage_i.alu_i.alu_div_i.OpB_DI), + .div_op_b_shift (ex_stage_i.alu_i.alu_div_i.OpBShift_DI), + .div_result (ex_stage_i.alu_i.alu_div_i.Res_DO), + .div_result_valid (ex_stage_i.alu_i.div_ready), + + // Floating point + .fpu_op_valid (ex_stage_i.apu_req), + .fpu_op_a (ex_stage_i.apu_operands_o[0]), + .fpu_op_b (ex_stage_i.apu_operands_o[1]), + .fpu_op_c (ex_stage_i.apu_operands_o[2]), + .fpu_rm (), + .fpu_flags (ex_stage_i.fpu_fflags_o), + .fpu_result (ex_stage_i.apu_result), + .fpu_result_valid (ex_stage_i.apu_valid), + + // Design specific + .is_debug (id_stage_i.controller_i.ctrl_fsm_cs inside {DBG_TAKEN_ID,DBG_TAKEN_IF,DBG_FLUSH}), + .is_interrupt (id_stage_i.int_controller_i.irq_req_ctrl_o), + .boot_addr ({boot_addr_i[31:2],2'b00}), + + .rf_we_lsu (ex_stage_i.regfile_we_lsu), + .rf_waddr_lsu (ex_stage_i.regfile_waddr_lsu), + .lsu_data_type (load_store_unit_i.data_type_q), + .lsu_data_sign (load_store_unit_i.data_sign_ext_q), + .lsu_data_offset (load_store_unit_i.rdata_offset_q), + .fpu_s_cycle (ex_stage_i.apu_singlecycle), + .fpu_m_cycle (ex_stage_i.apu_multicycle), + .fpu_waddr (ex_stage_i.apu_waddr), + .fpu_waddr_ex (apu_waddr_ex), + .fpu_lat_ex (apu_lat_ex), + .fpu_op_ex (apu_op_ex), + .dot_mul_op_a (ex_stage_i.mult_dot_op_a_i), + .dot_mul_op_b (ex_stage_i.mult_dot_op_b_i), + .dot_mul_op_c (ex_stage_i.mult_dot_op_c_i) diff --git a/scripts/riscv_isa_formal/common/setup.tcl b/scripts/riscv_isa_formal/common/setup.tcl new file mode 100755 index 000000000..0bcce5472 --- /dev/null +++ b/scripts/riscv_isa_formal/common/setup.tcl @@ -0,0 +1,564 @@ +proc duration {int_time} { + set timeList [list] + if {$int_time == 0} { + return "0 Sec" + } else { + foreach div {86400 3600 60 1} mod {0 24 60 60} name {Day Hour Min Sec} { + set n [expr {$int_time / $div}] + if {$mod > 0} {set n [expr {$n % $mod}]} + if {$n > 1} { + lappend timeList "$n ${name}s" + } elseif {$n == 1} { + lappend timeList "$n $name" + } + } + return [join $timeList] + } +} + +proc quantify_run {{cmd_limit 0} {run 0} {no_cuts {}} {limit_scale 2.0} {effort 4} {skip_effort_level 0} {html_dir {}} {result_file {}} {checks {}} {prev_run_result {}} {skip_files {}}} { + + puts "\n-INFO- Start of Quantify Run ($run)::\n\nChecks Included::\n\n$checks" + + set_limit -command_real_time $cmd_limit + set run_start_t [clock seconds] + puts "\n-INFO- Launching Quantify Command::\n\nquantify -assume_hold -additional_args \[list $no_cuts -limit_scale $limit_scale -use_single_prover\] -effort $effort -skip_effort_level $skip_effort_level -html $html_dir -save $result_file -checks $checks -incremental $prev_run_result -skip_files $skip_files\n" + catch {quantify -assume_hold -additional_args [list $no_cuts -limit_scale $limit_scale -use_single_prover] -effort $effort -skip_effort_level $skip_effort_level -html $html_dir -save $result_file -checks $checks -incremental $prev_run_result -skip_files $skip_files} + set run_end_t [expr [clock seconds] - $run_start_t] + set_limit -default + + puts "\n-INFO- End of Quantify Run ($run) | Time spent:: [duration $run_end_t]\n" +} + +## 0. DESIGN SETUP ## + +### SETTING UP THE DESIRED CONFIGURATION, RUN & APP ### +## source the setup.inc as the following: [onespin -i setup.inc ] +## arg1: what configuration to set . +## arg2: what processor verification mode to set . +## arg3: what app to launch on top of the processor app. +## ------------------------------------------------------------------------------------------------------------------ + +set configs [dict create \ + "DEF" [dict create \ + description "RV32IMCZicsr_Zifencei" \ + elab "-verilog_parameter {}" \ + define "" \ + json "" \ + ] \ + "F0" [dict create \ + description "RV32IMFCZicsr_Zifencei with FPU latency params set to 0" \ + elab "-verilog_parameter {FPU=1 FPU_ADDMUL_LAT=0 FPU_OTHERS_LAT=0}" \ + define "CFG_F" \ + json "" \ + ] \ + "ZF0" [dict create \ + description "RV32IMCZicsr_Zifencei_Zfinx with FPU latency params set to 0" \ + elab "-verilog_parameter {FPU=1 ZFINX=1 FPU_ADDMUL_LAT=0 FPU_OTHERS_LAT=0}" \ + define "CFG_ZFINX" \ + json "" \ + ] \ + "XP" [dict create \ + description "RV32IMCZicsr_Zifencei_Xpulp" \ + elab "-verilog_parameter {COREV_PULP=1}" \ + define "CFG_XP" \ + json "Xpulp.json Zfinx.json" \ + ] \ + "XPF0" [dict create \ + description "RV32IMFCZicsr_Zifencei_Xpulp with FPU latency params set to 0" \ + elab "-verilog_parameter {FPU=1 COREV_PULP=1 FPU_ADDMUL_LAT=0 FPU_OTHERS_LAT=0}" \ + define "CFG_XP CFG_F" \ + json "Xpulp.json" \ + ] \ + "XPF1" [dict create \ + description "RV32IMFCZicsr_Zifencei_Xpulp with FPU latency params set to 1" \ + elab "-verilog_parameter {FPU=1 COREV_PULP=1 FPU_ADDMUL_LAT=1 FPU_OTHERS_LAT=1}" \ + define "CFG_XP CFG_F" \ + json "Xpulp.json" \ + ] \ + "XPF2" [dict create \ + description "RV32IMFCZicsr_Zifencei_Xpulp with FPU latency params set to 2" \ + elab "-verilog_parameter {FPU=1 COREV_PULP=1 FPU_ADDMUL_LAT=2 FPU_OTHERS_LAT=2}" \ + define "CFG_XP CFG_F" \ + json "Xpulp.json" \ + ] \ + "XPZF0" [dict create \ + description "RV32IMCZicsr_Zifencei_Zfinx_Xpulp with FPU latency params set to 0" \ + elab "-verilog_parameter {FPU=1 ZFINX=1 COREV_PULP=1 FPU_ADDMUL_LAT=0 FPU_OTHERS_LAT=0}" \ + define "CFG_XP CFG_ZFINX" \ + json "Xpulp.json Zfinx.json" \ + ] \ + "XPZF1" [dict create \ + description "RV32IMCZicsr_Zifencei_Zfinx_Xpulp with FPU latency params set to 1" \ + elab "-verilog_parameter {FPU=1 ZFINX=1 COREV_PULP=1 FPU_ADDMUL_LAT=1 FPU_OTHERS_LAT=1}" \ + define "CFG_XP CFG_ZFINX" \ + json "Xpulp.json Zfinx.json" \ + ] \ + "XPZF2" [dict create \ + description "RV32IMCZicsr_Zifencei_Zfinx_Xpulp with FPU latency params set to 2" \ + elab "-verilog_parameter {FPU=1 ZFINX=1 COREV_PULP=1 FPU_ADDMUL_LAT=2 FPU_OTHERS_LAT=2}" \ + define "CFG_XP CFG_ZFINX" \ + json "Xpulp.json Zfinx.json" \ + ] \ + "XPXC" [dict create \ + description "RV32IMCZicsr_Zifencei_Xpulp_Xcluster" \ + elab "-verilog_parameter {COREV_PULP=1 COREV_CLUSTER=1}" \ + define "CFG_XP CFG_XC" \ + json "Xpulp.json Xcluster.json Zfinx.json" \ + ] \ + "XPXCZF2" [dict create \ + description "RV32IMCZicsr_Zifencei_Zfinx_Xpulp_Xcluster with FPU latency params set to 2" \ + elab "-verilog_parameter {FPU=1 ZFINX=1 COREV_PULP=1 COREV_CLUSTER=1 FPU_ADDMUL_LAT=2 FPU_OTHERS_LAT=2}" \ + define "CFG_XP CFG_XC CFG_ZFINX" \ + json "Xpulp.json Xcluster.json Zfinx.json" \ + ] \ +] + +set pve_modes [dict create \ + "DEF" [dict create \ + description "DEF: Control path verification of all instructions and datapath verification of all instructions except multiplication, division or floating point ones" \ + define "" \ + ] \ + "DPM" [dict create \ + description "DPM: Data path verification of multiplication/ division instructions" \ + define "PVE_M_SUPPORT RESTRICT_MUL_OPS_FREE_BITS=1" \ + ] \ + "DPF" [dict create \ + description "DPF: Data path verification of floating-point instructions" \ + define "PVE_FPU_SUPPORT RESTRICT_MUL_OPS_FREE_BITS=1" \ + ] \ +] + +set apps [dict create \ + "PRC" [dict create \ + description "PRC: Property Checking" \ + compile "-dontcare_handling any -signal_domain {{scan_cg_en_i} 0}" \ + ] \ + "QTF" [dict create \ + description "QTF: Quantify" \ + compile "-dontcare_handling any -signal_domain {{scan_cg_en_i} 0} -constant [list [list core_i.id_stage_i.register_file_i.rst_n 1] ]" \ + ] \ + "VCI" [dict create \ + description "VCI: Verification Coverage Integration" \ + compile "-dontcare_handling any -signal_domain {{scan_cg_en_i} 0}" \ + ] \ +] + +if {$::argc>0} { + lassign $::argv cfg pve_mode app + if {$cfg ni [dict keys $configs]} { + onespin::message -error "Only configurations [join [dict keys $configs] ,] are supported!" + return -code error + } + if {$pve_mode ni [dict keys $pve_modes]} { + onespin::message -error "Only processor verification modes [join [dict keys $pve_modes] ,] are supported!" + return -code error + } elseif {$pve_mode eq "DPF" && $cfg in {"DEF" "XP" "XPXC"} } { + onespin::message -error "Floating-point configuration must be selected in order to perform data path verification!" + return -code error + } + if {$app ni [dict keys $apps]} { + onespin::message -error "Only apps [join [dict keys $apps] ,] are supported!" + return -code error + } +} else { + if {[get_tool_info -gui]} { + set cfg [string index [onespin::ask_user -default 0 -alternatives [lmap {k d} $configs {string cat "$k - " [dict get $d description]}] "Select which RISC-V configuration to set up:"] 0] + set pve_mode [string index [onespin::ask_user -default "DEF" -alternatives [lmap {k d} $pve_modes {string cat "$k - " [dict get $d description]}] "Select which processor verification mode to set:"] 0] + set app [string index [onespin::ask_user -default "PRC" -alternatives [lmap {k d} $apps {string cat "$k - " [dict get $d description]}] "Select which app to launch:"] 0] + } else { + set cfg "DEF" + set pve_mode "DEF" + set app "PRC" + } +} +set target cv32e40p_top +set core_inst core_i +set prefix ${core_inst}. +## + +### ADJUST TO READ-IN THE NEW DESIGN ### +onespin::set_parameter disable_intermediate_arithmetic_signals 1 +set cwd [pwd] +set_session_option -naming_style sv +set_compile_option {*}[dict get $apps $app compile] +set_elaborate_option {*}[dict get $configs $cfg elab] -top $target +cd cv32e40p +source $cwd/setup_mv.tcl +set_reset_sequence -low rst_ni +cd $cwd + +set cfg_dir $cwd/$cfg +set pve_mode_dir $cwd/$cfg/$pve_mode +set app_dir $cwd/$cfg/$pve_mode/$app +file mkdir $cfg_dir +file mkdir $pve_mode_dir +file mkdir $app_dir +## + +### PROCESSOR APP FLOW ### + +## --------------------------------------------------------------------------------------------------------------------------------- +## 1 > 2 > 3 > 4 > 5 > 6 > 7 +## --------------------------------------------------------------------------------------------------------------------------------- +## PRE-ANALYSIS | DESIGN | POST-ANALYSIS | ASSERTION | ASSERTION | PERFORMANCE | ASSERTION +## CONFIGURATION | ANALYSIS | CONFIGURATION | GENERATION | READING & RETUNING | ENHANCEMENT | RUNNING & DEBUGGING +## --------------------------------------------------------------------------------------------------------------------------------- + +## --------------------------------------------------------------------------------------------------------------------------------- +## processor_integrity:: | DESCRIPTION +## --------------------------------------------------------------------------------------------------------------------------------- +## extract_ISA | Extract ISA from a RISC-V based processor core and store data in a processor database. +## -core_instance <> | Specify instance name of the core in the DUV to instantiate the VIP on. +## -csr_addr <> | Specify CSR address signal that might be used to assist extraction. +## -csr_rdata <> | Specify CSR read data signal that might be used to assist extraction. +## merge_data | Merge JSON data into the database. +## -file <> | Specify JSON file to be merged. +## -configuration <> | Specify predefined JSON configuration to be merged. +## generate_assertions | Generate assertions for verifying the RISC-V core based on the database. +## -create_individual_checks <> | Specify extensions for which assertions are generated per instruction. +## -exclude_extensions <> | Specify extensions for which assertions generation is supressed. +## -include_extensions <> | Specify extensions only for which assertions are generated. +## generate_IVA | Perform initial value abstraction of architecture state. +## -candidates <> | Specify architecture register fields to be abstracted. +## analyze_trace | Perform detailed trace analysis of run assertions. +## save_data | Write the processor database, or part of it, to a JSON file. +## clear_data | Clear JSON data from the processor database. +## --------------------------------------------------------------------------------------------------------------------------------- +## For full app documentation run "help *processor_integrity::*" or refer to Chapter 14. of the User Manual. +## --------------------------------------------------------------------------------------------------------------------------------- + +## 0. APP SETUP ## + +package require processor_integrity + +### APPEND THE FOLLOWING SET OF DEFINES (ONLY IF NECESSARY) ### +## --------------------------------------------------------------------------------------------------------------------------------- +## DEFINE | USE CASE IF SET +## --------------------------------------------------------------------------------------------------------------------------------- +## GRADUAL VERIFICATION ## +## SKIP_PC_CHECK | Skip checking PC register updates. +## SKIP_RF_CHECK | Skip checking register file updates. +## SKIP_CSR_CHECK | Skip checking CSR updates and reads. +## SKIP_DMEM_CHECK | Skip checking data memory requests. +## LIMIT_TOTAL_INSTR_COUNT | Limit total # of instructions allowed in the pipeline. +## PERFORMANCE ENHANCEMENT ## +## RESTRICT_REGS | Restrict instruction decoding & register file verification to a subset of registers. +## RESTRICT_REGISTER_INDEX | Restrict register file verification to one register only, instruction decoding is not affected. +## RESTRICT_CHECK_DATA_SLICE | Restrict register file data and memory write data verification to a slice or even a bit. +## RESTRICT_MUL_OPS_FREE_BITS | Restrict # of operand bits allowed to toggle checking multiplication/ division instruction datapath. +## RESTRICT_DMEM_STALL_CYCLES | Restrict data memory stall cycles to specific number. Has an effect w/ protocol VIPs' usage. +## TAILORED VERIFICATION ## +## PVE_M_SUPPORT | Enable checking M extension data path. By default, only the control path is checked. +## PVE_FPU_SUPPORT | Enable checking F extension data path. By default, only the control path is checked. +## CHECK_ACCESS_FAULTS | Enable checking all access faults fully according to the privileged specification or Smepmp. +## CUSTOM_MEM_INTERFACES | Constrain memory interfaces. Use only in case bus protocols implemented are not tool supported. +## --------------------------------------------------------------------------------------------------------------------------------- +lappend defines {*}[dict get $configs $cfg define] {*}[dict get $pve_modes $pve_mode define] RESTRICT_REGS RESTRICT_DMEM_STALL_CYCLES=2 +## + +### RE-SET THE FOLLOWING SET OF VARIABLES (ONLY IF NECESSARY) ### +lappend pre_analysis_json_files_to_merge spec.json {*}[dict get $configs $cfg json] +set csr_addr_to_assist_analysis {} +set csr_rdata_to_assist_analysis {} +set core_instance_to_instantiate_vip_on ${core_inst} +lappend post_analysis_json_files_to_merge spec.json {*}[dict get $configs $cfg json] core.json +lappend extensions_to_generate_individual_checks_for F Zfinx +set extensions_to_exclude_assertion_generation_for {} +if {"CV_LOOP" in $defines} { + lappend pre_analysis_json_files_to_merge Xpulp_hwlp.json + lappend post_analysis_json_files_to_merge Xpulp_hwlp.json +} +## + +### EXTEND THE FOLLOWING LISTS BY THE RESPECTIVE RTL SIGNALS (ONLY IF NECESSARY) ### +lappend mul_signals_to_cut ${prefix}ex_stage_i.mult_i.result_o ${prefix}ex_stage_i.alu_i.alu_div_i.Res_DO ${prefix}ex_stage_i.alu_i.alu_div_i.Cnt_DP +lappend fpu_signals_to_cut ${prefix}apu_result_i ${prefix}apu_flags_i +lappend rtl_signals_to_cut +lappend rtl_signals_to_disassemble ${prefix}instr_rdata_i ${prefix}instr_rdata_id ${prefix}if_stage_i.instr_aligned +## + +if {![info exists reuse_files] || !$reuse_files} { + +## 1. PRE-ANALYSIS CONFIGURATION ## + + foreach i ${pre_analysis_json_files_to_merge} { + processor_integrity::merge_data -file ${i} + } + +## 2. DESIGN ANALYSIS ## + + processor_integrity::extract_ISA -csr_addr $csr_addr_to_assist_analysis -csr_rdata $csr_rdata_to_assist_analysis -core_instance $core_instance_to_instantiate_vip_on + +## 3. POST-ANALYSIS CONFIGURATION ## + + foreach i ${post_analysis_json_files_to_merge} { + processor_integrity::merge_data -file ${i} + } + + if {"CFG_ZFINX" in $defines} { + onespin::data::set ISA/Z/Zfinx true + } + + if {$pve_mode ne "DEF"} { + onespin::data::set PVE/checker_instance "RV_chk_DP" + } + +## 4. ASSERTION GENERATION ## + + cd $pve_mode_dir + processor_integrity::generate_assertions -create_individual_checks $extensions_to_generate_individual_checks_for -exclude_extensions $extensions_to_exclude_assertion_generation_for -force + cd $cwd +} else { + puts "-W- Re-using previously generated files! Make sure to re-generate all files on adopting a new tool version or changing the JSON configuration!" + source $pve_mode_dir/RISCV_disass.tcl + source RISCV_disass.tcl +} + +## 5. ASSERTION READING & RETUNING ## + +### USE TO CONSTRAIN MEMORY INTERFACES (ONLY IF BUS PROTOCOLS IMPLEMENTED ARE TOOL SUPPORTED) ### +## Instantiate the respective bus protocol VIP for each of the fetch and data memory interfaces +## The VIPs in this case are used to check and more importantly constrain memory interfaces +## Read in the instantiated VIPs, my_{}.sv, using the read_sva command below +#instantiate_vip -addr_sig instr_addr_o -generated_instance_name obi_imem_checker -filename obi_imem.sv obi +#instantiate_vip -addr_sig data_addr_o -generated_instance_name obi_dmem_checker -filename obi_dmem.sv obi +## + +read_sva -define $defines -include_path $pve_mode_dir {core_checker.sv $pve_mode_dir/bind.sv vips/obi_?mem.sv} + +## 7.1 ASSERTION RUNNING & DEBUGGING ## + +### USE TO RUN INITIAL SET OF ASSERTIONS ### +set_check_option -prover_exec_order { { approver1 approver4 prover2:0 prover2:8 prover2:11 disprover1 disprover3 } } -disprover1_steps 40 -disprover3_steps 40 +check [get_checks -filter name=~"*invariant_a"||name=~"*legal_CSR_reset_state_a"||name=~"*RESET_a"] +## + +## 6. PERFORMANCE ENHANCEMENT ## + +### USE TO COMPUTE INVARIANTS (IF NECESSARY) ### +compute_invariants +## + +if {$app eq "PRC"} { + ### USE TO PERFORM AUTOMATIC INITIAL VALUE ABSTRACTION (IVA) OF ARCHITECTURE STATE (IF NECESSARY) ### + lappend candidates X F frm + if {"CFG_XP" in $defines} { + lappend candidates lpstart0 lpstart1 lpend0 lpend1 + } + processor_integrity::generate_IVA -candidates $candidates + ## +} + +### USE TO CUT DESIGN COMPLEX SIGNALS (IF NECESSARY) ### +if {$pve_mode ne "DPM"} { + lappend rtl_signals_to_cut {*}$mul_signals_to_cut +} +if {($pve_mode ne "DPF") && ("CFG_F" in $defines || "CFG_ZFINX" in $defines)} { + lappend rtl_signals_to_cut {*}$fpu_signals_to_cut +} +add_cut_signals $rtl_signals_to_cut +cut_signals +## + +## 7.2 ASSERTION RUNNING & DEBUGGING ## + +### USE TO EASE DEBUGGING BY DISASSEMBLING VALUES OF RTL SIGNALS HOLDING INSTRUCTION WORDS & RUN THE OTHER ASSERTIONS ### +foreach i ${rtl_signals_to_disassemble} { + use_value_printer ${i} PVE_disass +} +## + +#set nb_processes 2 +#set nb_processes 3 +#set nb_processes 4 +#set nb_processes 5 +#set nb_processes 6 +#set nb_processes 8 +#set nb_processes 12 +set nb_processes 16 +#set nb_processes 24 +#set nb_processes 32 + +set_check_option -verbose +set_check_option -local_processes $nb_processes +set_check_option -engine_licensing unlimited + +puts "\n-INFO- Launching $app app in $pve_mode mode with $nb_processes parallel processes.\n" + +#set_check_option -prover_exec_order { { approver1 approver4 prover2:0 prover2:8 prover2:11 disprover1 disprover3 } } +set_check_option -prover_exec_order { { approver1 prover2:0 prover2:8 prover2:11 } } +#set_check_option -disprover1_steps 40 -disprover3_steps 40 + +check_consistency -category model_building -effort maximum +exclude_check [get_checks -filter name=~"*hdl*"||name=~"*FSQRT_S_a*"||name=~"**FDIV_S_a*"] + +set DEF_checks [lsort -dictionary [get_checks -filter excluded==false&&(type==property||type==assertion)]] +set DPM_checks [lsort -dictionary [get_checks -filter excluded==false&&(name=~"*RV32M.*"||name=~"*RV32X.CV_XDOT*"||name=~"*RV32X.CV_MUL*"||name=~"*RV32X.CV_MAC*"||name=~"*RV32X.CV_CPLXMUL*")]] +set DPF_checks [lsort -dictionary [get_checks -filter excluded==false&&(name=~"*RV32F.*"||name=~"*RV32Zfinx.*")]] + +set group_1_checks [lsort -dictionary [concat core_i.RV_chk.ops.RESET_a [get_checks -filter excluded==false&&type==assertion]]] +set group_2_checks [lsort -dictionary [list core_i.RV_chk.ops.XCPT_IF_ID_a core_i.RV_chk.RV32C.ARITH_a core_i.RV_chk.RV32C.BRANCH_Taken_a core_i.RV_chk.RV32C.BRANCH_a core_i.RV_chk.RV32C.JUMP_a core_i.RV_chk.RV32I.EBREAK_BreakPoint_a core_i.RV_chk.RV32I.MEM_MultiAccess_a core_i.RV_chk.RV32I.xRET_a core_i.RV_chk.RV32X.CV_ADD_X_a core_i.RV_chk.RV32X.CV_BITMAN_OTHER_a core_i.RV_chk.RV32X.CV_EXTRACTX_X_a core_i.RV_chk.RV32X.CV_INSERTX_a core_i.RV_chk.RV32X.CV_PACKXX_X_a core_i.RV_chk.RV32X.CV_SETUPX_a core_i.RV_chk.RV32X.CV_SHUFFLE2_X_a core_i.RV_chk.RV32Zicsr.CSRx_a]] +set group_3_checks [lsort -dictionary [list core_i.RV_chk.ops.BUBBLE_a core_i.RV_chk.RV32I.ARITH_a core_i.RV_chk.RV32I.EBREAK_HaltReq_a core_i.RV_chk.RV32I.ECALL_a core_i.RV_chk.RV32I.FENCE_a core_i.RV_chk.RV32I.WFI_a core_i.RV_chk.RV32X.CV_ABS_X_a core_i.RV_chk.RV32X.CV_CLIPXX_a core_i.RV_chk.RV32X.CV_CMPEQ_X_a core_i.RV_chk.RV32X.CV_EXTRACTXX_a core_i.RV_chk.RV32X.CV_EXTXX_a core_i.RV_chk.RV32X.CV_INSERT_X_a core_i.RV_chk.RV32X.CV_SX_I_a core_i.RV_chk.RV32X.CV_SX_RI_a core_i.RV_chk.RV32X.CV_ADDXXNR_a core_i.RV_chk.RV32X.CV_SHUFFLEIX_SCI_B_a core_i.RV_chk.RV32X.CV_BSETX_a core_i.RV_chk.RV32X.CV_BXXIMM_Taken_a core_i.RV_chk.RV32X.CV_ENDX_a core_i.RV_chk.RV32X.CV_LXX_I_a core_i.RV_chk.RV32X.CV_LXX_RI_a core_i.RV_chk.RV32X.CV_SLL_X_a core_i.RV_chk.RV32X.CV_STARTX_a core_i.RV_chk.RV32X.CV_ADD_DIVX_a core_i.RV_chk.RV32X.CV_ADDXXN_a core_i.RV_chk.RV32X.CV_AVGU_X_a core_i.RV_chk.RV32X.CV_BCLRX_a core_i.RV_chk.RV32X.CV_SUB_DIVX_a core_i.RV_chk.RV32X.CV_SUBROTMJ_X_a core_i.RV_chk.RV32X.CV_SUBXXN_a core_i.RV_chk.RV32X.CV_SUBXXNR_a core_i.RV_chk.RV32X.CV_MAXU_X_a]] +set group_4_checks [lsort -dictionary [concat [get_checks -filter excluded==false&&name=~"*RV32X.CV_ELW*"] core_i.RV_chk.RV32I.EBREAK_ForcedEntry_a core_i.RV_chk.RV32X.CV_COUNTX_a core_i.RV_chk.RV32X.CV_LXX_R_a core_i.RV_chk.RV32X.CV_MAXX_a core_i.RV_chk.RV32X.CV_SX_R_a core_i.RV_chk.RV32C.MEM_a core_i.RV_chk.RV32C.MEM_MultiAccess_a core_i.RV_chk.RV32I.BRANCH_a core_i.RV_chk.RV32I.BRANCH_Taken_a core_i.RV_chk.RV32I.JUMP_a core_i.RV_chk.RV32I.MEM_a core_i.RV_chk.RV32X.CV_ABS_a core_i.RV_chk.RV32X.CV_AND_X_a core_i.RV_chk.RV32X.CV_AVG_X_a core_i.RV_chk.RV32X.CV_BXXIMM_a core_i.RV_chk.RV32X.CV_CMPGE_X_a core_i.RV_chk.RV32X.CV_CMPGEU_X_a core_i.RV_chk.RV32X.CV_CMPGT_X_a core_i.RV_chk.RV32X.CV_CMPGTU_X_a core_i.RV_chk.RV32X.CV_CMPLE_X_a core_i.RV_chk.RV32X.CV_CMPLEU_X_a core_i.RV_chk.RV32X.CV_CMPLT_X_a core_i.RV_chk.RV32X.CV_CMPLTU_X_a core_i.RV_chk.RV32X.CV_CMPNE_X_a core_i.RV_chk.RV32X.CV_CPLXCONJ_a core_i.RV_chk.RV32X.CV_LXX_I_MultiAccess_a core_i.RV_chk.RV32X.CV_LXX_R_MultiAccess_a core_i.RV_chk.RV32X.CV_LXX_RI_MultiAccess_a core_i.RV_chk.RV32X.CV_MAX_X_a core_i.RV_chk.RV32X.CV_MIN_X_a core_i.RV_chk.RV32X.CV_MINU_X_a core_i.RV_chk.RV32X.CV_MINX_a core_i.RV_chk.RV32X.CV_OR_X_a core_i.RV_chk.RV32X.CV_SHUFFLE_X_a core_i.RV_chk.RV32X.CV_SLEX_a core_i.RV_chk.RV32X.CV_SRA_X_a core_i.RV_chk.RV32X.CV_SRL_X_a core_i.RV_chk.RV32X.CV_SUB_X_a core_i.RV_chk.RV32X.CV_SX_I_MultiAccess_a core_i.RV_chk.RV32X.CV_SX_R_MultiAccess_a core_i.RV_chk.RV32X.CV_SX_RI_MultiAccess_a core_i.RV_chk.RV32X.CV_XOR_X_a core_i.RV_chk.RV32Zifencei.FENCE_I_a]] +set group_5_checks [lsort -dictionary [get_checks -filter excluded==false&&(name=~"*RV32M.DIV16_a*"||name=~"*RV32M.DIV32_a*"||name=~"*RV32M.MUL_a*"||name=~"*RV32X.CV_XDOT*"||name=~"*RV32X.CV_MUL*"||name=~"*RV32X.CV_MAC*"||name=~"*RV32X.CV_CPLXMUL*")]] +set group_6_checks [lsort -dictionary [get_checks -filter excluded==false&&(name=~"*RV32F.*"||name=~"*RV32Zfinx.*")]] + +set skipped_files "*/fpnew_* {} */gated_clk_cell* {} */lzc* {} */pa_fdsu_* {} */pa_fpu_* {} */rr_arb_tree* {}" + +puts "\n-INFO- Compile options::\n\n\t[dict get $apps $app compile]\n" +puts "\n-INFO- Elaborate options::\n\n\t[dict get $configs $cfg elab]\n" +puts "\n-INFO- Defines::\n\n\t$defines\n" +puts "\n-INFO- Cut signals::\n\n\t$rtl_signals_to_cut\n" + +if {$app eq "PRC"} { + +# set_check_option -prover_exec_order { { approver1 approver4 prover2:0 prover2:8 prover2:11 disprover1 disprover3 } } + set_check_option -prover_exec_order { { approver1 prover2:0 prover2:8 prover2:11 } } +# set_check_option -prover_exec_order { { disprover1 disprover3 } } -disprover1_steps 20 -disprover3_steps 20 + + set all_checks [set ${pve_mode}_checks] + set checks_nb [llength $all_checks] + set nb_round [expr $checks_nb / $nb_processes] + set nb_remain [expr $checks_nb % $nb_processes] + puts "nb_round = $nb_round, nb_remain = $nb_remain" + for {set i 0} {$i < $nb_round} {incr i} { + set checks [lrange $all_checks [expr $i * $nb_processes] [expr ((($i + 1) * $nb_processes) - 1)]] + puts "[expr $i * $nb_processes] [expr ((($i + 1) * $nb_processes) - 1)]" + puts "\n-INFO- Launching Check Command::\n\ncheck $checks\n" + check $checks + report_result -details + cd $app_dir + save_database -force round_[expr $i + 1] + cd $cwd + } + if {$nb_remain > 0} { + set checks [lrange $all_checks [expr $nb_round * $nb_processes] [expr (($nb_round * $nb_processes) + $nb_remain - 1)]] + puts "[expr $nb_round * $nb_processes] [expr (($nb_round * $nb_processes) + $nb_remain - 1)]" + puts "\n-INFO- Launching Check Command::\n\ncheck $checks\n" + check $checks + report_result -details + cd $app_dir + save_database -force round_[expr $nb_round + 1] + cd $cwd + } + + report_result -signoff -details + +# set_check_option -prover_exec_order { { disprover1 disprover3 } } +# puts "\n-INFO- Launching Check Command::\n\ncheck RV32M.DIV16_a\n" +# check [get_checks -filter name=~"*RV32M.DIV16_a*"] +# cd $app_dir +# save_database -force +# cd $cwd + +} + +if {$app eq "QTF"} { + + source basics.tcl.obf + + set_check_option -prover_exec_order { { disprover1 disprover3 } } -disprover1_steps 20 -disprover3_steps 20 + + set html "${app_dir}/html_results_${cfg}_${pve_mode}" + set results "${app_dir}/qtf_results_${cfg}_${pve_mode}_R" + set log "${app_dir}/${app}_${cfg}_${pve_mode}_R" + + if {$pve_mode eq "DEF"} { + + for {set i 1} {$i < 7} {incr i} { + puts "\nGroup (${i}) checks:\n\nTotal number of checks is: [llength [set group_${i}_checks]] \n" + foreach j [set group_${i}_checks] { + puts "$j" + } + } + + for {set i 1} {$i < 7} {incr i} { + puts "Group (${i}) checks: Total number of checks is: [llength [set group_${i}_checks]]" + } + +# for {set i 1} {$i < 7} {incr i} { + + set i 5 + + start_message_log ${log}${i}.log + if {$i == 1} { + quantify_run 0 $i {-no_cuts} 1.0 2 1 ${html}_L2_S1_R${i} ${results}${i} $group_1_checks {} {} + } elseif {$i == 2} { + quantify_run 0 $i {-no_cuts} 4.0 4 3 ${html}_L4_S4_R${i} ${results}${i} $group_2_checks ${results}[expr $i-1] $skipped_files + } elseif {$i == 3} { + quantify_run 0 $i {-no_cuts} 2.0 4 3 ${html}_L4_S2_R${i} ${results}${i} $group_3_checks ${results}[expr $i-1] $skipped_files + } elseif {$i == 4} { + quantify_run 0 $i {-no_cuts} 2.0 4 3 ${html}_L4_S2_R${i} ${results}${i} $group_4_checks ${results}[expr $i-1] $skipped_files + } elseif {$i == 5} { +# quantify_run 0 $i {-no_cuts} 4.0 4 3 ${html}_L4_S4_R${i} ${results}${i} $group_5_checks ${results}[expr $i-1] $skipped_files + quantify_run 0 $i {} 6.0 4 3 ${html}_L4_S4_R${i} ${results}${i} $group_5_checks ${results}[expr $i-1] $skipped_files + } elseif {($i == 6) && ("CFG_F" in $defines || "CFG_ZFINX" in $defines)} { + quantify_run 0 $i {-no_cuts} 4.0 4 3 ${html}_L4_S4_R${i} ${results}${i} $group_6_checks ${results}[expr $i-1] {} + } + stop_message_log +# } + + } elseif {$pve_mode eq "DPM"} { + + if {("CFG_F" in $defines || "CFG_ZFINX" in $defines)} { + set i 7 + } else { + set i 6 + } + + start_message_log ${log}${i}.log +# quantify_run 0 $i {-no_cuts} 4.0 4 3 ${html}_L4_S4_R${i} ${results}${i} $group_5_checks {} $skipped_files +# file copy -force ${cfg_dir}/DEF/QTF/qtf_results_${cfg}_DEF_R[expr $i-1] ${cfg_dir}/DEF/QTF/qtf_results_${cfg}_DEF_R[expr $i-1]-Xr +# fileutil::updateInPlace ${cfg_dir}/DEF/QTF/qtf_results_${cfg}_DEF_R[expr $i-1] [list string map [list " Xr" " U0"]] +# quantify_run 0 $i {-no_cuts} 4.0 4 3 ${html}_L4_S4_R${i} ${results}${i} $group_5_checks ${cfg_dir}/DEF/QTF/qtf_results_${cfg}_DEF_R[expr $i-1] $skipped_files + quantify_run 0 $i {} 6.0 4 3 ${html}_L4_S4_R${i} ${results}${i} $group_5_checks ${cfg_dir}/DEF/QTF/qtf_results_${cfg}_DEF_R[expr $i-1] $skipped_files + stop_message_log + + } elseif {$pve_mode eq "DPF"} { + + set i 8 + + start_message_log ${log}${i}.log +# quantify_run 0 $i -no_cuts 2.0 4 3 ${html}_L4_S4_R${i} ${results}${i} $group_6_checks {} {} +# file copy -force ${cfg_dir}/DPM/QTF/qtf_results_${cfg}_DPM_R[expr $i-1] ${cfg_dir}/DPM/QTF/qtf_results_${cfg}_DPM_R[expr $i-1]-Xr +# fileutil::updateInPlace ${cfg_dir}/DPM/QTF/qtf_results_${cfg}_DPM_R[expr $i-1] [list string map [list " Xr" " U0"]] + quantify_run 0 $i -no_cuts 2.0 4 3 ${html}_L4_S4_R${i} ${results}${i} $group_6_checks ${cfg_dir}/DPM/QTF/qtf_results_${cfg}_DPM_R[expr $i-1] {} + stop_message_log + + } + +} + +if {$app eq "VCI"} { + + set_check_option -prover_exec_order { { disprover1 disprover3 } } -disprover1_steps 20 -disprover3_steps 20 + + set output_dir "${app_dir}/qtf_coverage_${cfg}_${pve_mode}" + set checks "[set ${pve_mode}_checks]" + set results "${cfg_dir}/${pve_mode}/QTF/qtf_results_${cfg}_${pve_mode}_R" + set log "${app_dir}/${app}_${cfg}_${pve_mode}" + + if {$pve_mode eq "DEF"} { + if {("CFG_F" in $defines || "CFG_ZFINX" in $defines)} { + set i 6 + } else { + set i 5 + } + } elseif {$pve_mode eq "DPM"} { + if {("CFG_F" in $defines || "CFG_ZFINX" in $defines)} { + set i 7 + } else { + set i 6 + } + } elseif {$pve_mode eq "DPF"} { + set i 8 + } + + start_message_log ${log}.log + puts "\n-INFO- Launching VCI Command::\nexport_quantify_coverage -call_script t.sh -generate_flist -output_dir $output_dir -checks $checks ${results}${i}\n" + export_quantify_coverage -call_script t.sh -generate_flist -output_dir $output_dir -checks $checks ${results}${i} + stop_message_log +# report_quantify_result -quantify_result qtf_results_run_${run} -html html_results_run_${run} + +} diff --git a/scripts/riscv_isa_formal/common/setup_mv.tcl b/scripts/riscv_isa_formal/common/setup_mv.tcl new file mode 100755 index 000000000..84eb4523c --- /dev/null +++ b/scripts/riscv_isa_formal/common/setup_mv.tcl @@ -0,0 +1,8 @@ +if {![info exists ::env(DESIGN_RTL_DIR)]} { + set ::env(DESIGN_RTL_DIR) [pwd]/rtl +} +set_read_hdl_option -verilog_version sv2012 -pragma_ignore {translate_} +vlog -sv -f cv32e40p_fpu_manifest.flist +elaborate +compile +set_mode mv diff --git a/scripts/riscv_isa_formal/common/t.sh b/scripts/riscv_isa_formal/common/t.sh new file mode 100755 index 000000000..eca98e09f --- /dev/null +++ b/scripts/riscv_isa_formal/common/t.sh @@ -0,0 +1,12 @@ +#!/bin/bash +# +# This script is a template representing a customization to integrate OneSpin 360 with VCS simulator +# +# onespin calls the script as follows: +# template_vcs_flow.sh +# +# In this script you need to set up the environment for the simulator, +# +ARG1=$1 + +vsim -64 -c -do "source ${ARG1}; quit -f" diff --git a/scripts/riscv_isa_formal/common/vips/obi_dmem.sv b/scripts/riscv_isa_formal/common/vips/obi_dmem.sv new file mode 100755 index 000000000..7ca5866e2 --- /dev/null +++ b/scripts/riscv_isa_formal/common/vips/obi_dmem.sv @@ -0,0 +1,60 @@ +/////////////////////////////////////////////////////////////////////////////////////////////////////////////// +// // +// General remarks: // +// // +// Just replace below with the name of the module you want to connect the VIP to // +// and add the appropriate parameter values and DUT signals in braces. // +// // +// Leave unused signals (and parameters that just have the default value) simply unconnected // +// because optional signals are pulled up/down appropriately in the checker file. // +// // +// The VIP uses an active LOW reset. // +// If your DUT reset signal, called "rst", is active high, use "!rst" in the instantiation // +// // +// For external interfaces (bus signals are primary inputs/outputs), set parameter ASSUME=1. // +// In that case, make sure MASTER=1 in case the DUT is the bus master (driving the address signal output), // +// or MASTER=0 in case the DUT is the bus slave (address signal is input). // +// // +// In case you instantiate the VIP several times for different interfaces in the DUT, // +// make sure to pick individual instance names (line with comment "non-ambiguous instance name" below) // +// // +/////////////////////////////////////////////////////////////////////////////////////////////////////////////// + +bind cv32e40p_core obi_checker #( + .ADDR_WIDTH (), // (default 32) number of bits in addr + .DATA_WIDTH (), // (default 32) number of bits in wdata, rdata + .ASSUME (1), // (default 0) switch to create assumes + .MASTER (1), // (default 0) switch to select master/slave side (when switched off, i.e., slave side, important in case of ASSUME) + .ASSERT_ON (), // (default 1) switch to generate assertions, + // useful to switch off (ASSERT_ON=0) together with ASSUME=1 just to constrain a block for Inspect + .COVER_ON (), // (default 1) switch to additionally generate cover statements + .X_CHECKING_ON(), // (default 0) switch to create no-X assertions (to be used in conjunction with x_checking_setup) + .LIVENESS_ON (), // (default 0) switch to create liveness assertions + .MAX_WAIT (`RESTRICT_DMEM_STALL_CYCLES), // (default $) number of cycles for waiting period checks (for creating liveness checks in case LIVENESS_ON=1) + .AUSER_WIDTH (), // (default 32) number of bits in auser (if used) + .WUSER_WIDTH (), // (default 32) number of bits in wuser (if used) + .RUSER_WIDTH (), // (default 32) number of bits in ruser (if used) + .ID_WIDTH (), // (default 32) number of bits in aid, rid (if used) + .MAX_OUTSTANDING_TRANSACTIONS(), // (default 2) maximum number of outstanding transactions in the system + .RESPONSE_PREDICTOR(1) // (default 0) switch to introduce a signal to predict the response at the beginning of the data phase +) obi_dmem_checker ( // non-ambiguous instance name + .clk (clk_i), // required + .reset_n(rst_ni), // required +// Address channel + .req (data_req_o), // required + .gnt (data_gnt_i), // required + .addr (data_addr_o), // required /*ADDRESS*/ + .we (data_we_o), // optional, default is 1'b0 + .be (data_be_o), // optional, default is '1 + .wdata (data_wdata_o), // required /*DATA*/ + .auser (), // optional, default is '0 + .wuser (), // optional, default is '0 + .aid (), // optional, default is '0 +// Response channel + .rvalid (data_rvalid_i), // required + .rready (), // optional, default is 1'b1 + .rdata (data_rdata_i), // required /*DATA*/ + .err (), // optional, default is 1'b0 + .ruser (), // optional, default is '0 + .rid () // optional, default is '0 +); diff --git a/scripts/riscv_isa_formal/common/vips/obi_imem.sv b/scripts/riscv_isa_formal/common/vips/obi_imem.sv new file mode 100755 index 000000000..126152246 --- /dev/null +++ b/scripts/riscv_isa_formal/common/vips/obi_imem.sv @@ -0,0 +1,59 @@ +/////////////////////////////////////////////////////////////////////////////////////////////////////////////// +// // +// General remarks: // +// // +// Just replace below with the name of the module you want to connect the VIP to // +// and add the appropriate parameter values and DUT signals in braces. // +// // +// Leave unused signals (and parameters that just have the default value) simply unconnected // +// because optional signals are pulled up/down appropriately in the checker file. // +// // +// The VIP uses an active LOW reset. // +// If your DUT reset signal, called "rst", is active high, use "!rst" in the instantiation // +// // +// For external interfaces (bus signals are primary inputs/outputs), set parameter ASSUME=1. // +// In that case, make sure MASTER=1 in case the DUT is the bus master (driving the address signal output), // +// or MASTER=0 in case the DUT is the bus slave (address signal is input). // +// // +// In case you instantiate the VIP several times for different interfaces in the DUT, // +// make sure to pick individual instance names (line with comment "non-ambiguous instance name" below) // +// // +/////////////////////////////////////////////////////////////////////////////////////////////////////////////// + +bind cv32e40p_core obi_checker #( + .ADDR_WIDTH (), // (default 32) number of bits in addr + .DATA_WIDTH (), // (default 32) number of bits in wdata, rdata + .ASSUME (1), // (default 0) switch to create assumes + .MASTER (1), // (default 0) switch to select master/slave side (when switched off, i.e., slave side, important in case of ASSUME) + .ASSERT_ON (), // (default 1) switch to generate assertions, + // useful to switch off (ASSERT_ON=0) together with ASSUME=1 just to constrain a block for Inspect + .COVER_ON (), // (default 1) switch to additionally generate cover statements + .X_CHECKING_ON(), // (default 0) switch to create no-X assertions (to be used in conjunction with x_checking_setup) + .LIVENESS_ON (), // (default 0) switch to create liveness assertions + .MAX_WAIT (), // (default $) number of cycles for waiting period checks (for creating liveness checks in case LIVENESS_ON=1) + .AUSER_WIDTH (), // (default 32) number of bits in auser (if used) + .WUSER_WIDTH (), // (default 32) number of bits in wuser (if used) + .RUSER_WIDTH (), // (default 32) number of bits in ruser (if used) + .ID_WIDTH (), // (default 32) number of bits in aid, rid (if used) + .MAX_OUTSTANDING_TRANSACTIONS() // (default 2) maximum number of outstanding transactions in the system +) obi_imem_checker ( // non-ambiguous instance name + .clk (clk_i), // required + .reset_n(rst_ni), // required +// Address channel + .req (instr_req_o), // required + .gnt (instr_gnt_i), // required + .addr (instr_addr_o), // required /*ADDRESS*/ + .we (), // optional, default is 1'b0 + .be (), // optional, default is '1 + .wdata ('0), // required /*DATA*/ + .auser (), // optional, default is '0 + .wuser (), // optional, default is '0 + .aid (), // optional, default is '0 +// Response channel + .rvalid (instr_rvalid_i), // required + .rready (), // optional, default is 1'b1 + .rdata (instr_rdata_i), // required /*DATA*/ + .err (), // optional, default is 1'b0 + .ruser (), // optional, default is '0 + .rid () // optional, default is '0 +); diff --git a/scripts/riscv_isa_formal/launch_command example b/scripts/riscv_isa_formal/launch_command example new file mode 100755 index 000000000..6b7f3a0a3 --- /dev/null +++ b/scripts/riscv_isa_formal/launch_command example @@ -0,0 +1,58 @@ +# Setup tool and licenses +#source SourceMe + +set instructions="v1_8_0"; set name_cmd="NAME=${instructions} ; + +set config=XP ; set config_cmd="CONF=${config}" +set config=XPF0 ; set config_cmd="CONF=${config}" +set config=XPF1 ; set config_cmd="CONF=${config}" +set config=XPF2 ; set config_cmd="CONF=${config}" +set config=XPZF0 ; set config_cmd="CONF=${config}" +set config=XPZF1 ; set config_cmd="CONF=${config}" +set config=XPZF2 ; set config_cmd="CONF=${config}" + +set app=PRC ; set app_cmd="APP=${app}" +set app=QTF ; set app_cmd="APP=${app}" +set app=VCI ; set app_cmd="APP=${app}" + +set mode=DEF ; set mode_cmd="MODE=${mode}" +set mode=DPM ; set mode_cmd="MODE=${mode}" +set mode=DPF ; set mode_cmd="MODE=${mode}" + +# Prepare the working directory (common files and design copy) or reuse existing one (no copy) +set prepare="" +set prepare="PREPARE=1" + +set verbose="" +set verbose="VERBOSE=1" + +set timeout="" +set timeout="DBG=1800" + +# Interactive or batch run on local server +set gui="gui" ; set gui_cmd="GUI=1" +set gui="batch" ; set gui_cmd="" + +set my_time = `date '+%Y-%m-%d-%Hh%Mm%Ss'` ; set logname=run_${gui}-${app}-cfg_${config}-mode_${mode}-${instructions}-${my_time}.log ; echo "\n vi ${logname}\n" ; \ +echo "make ${gui_cmd} ${app_cmd} ${config_cmd} ${mode_cmd} ${name_cmd} ${verbose} ${prepare} ${timeout} all\n" > ${logname} && echo "" >>& ${logname} ; \ +/usr/bin/time make ${gui_cmd} ${app_cmd} ${config_cmd} ${mode_cmd} ${name_cmd} ${verbose} ${prepare} ${timeout} all >> & ! ${logname} & + +# Interactive or batch run on compute farm server using LSF +set gui="lsf" ; set gui_cmd="" ; set queue="long" +set gui="lsf_gui" ; set gui_cmd="GUI=1" ; set queue="gui -XF" +set gui="lsf_gui" ; set gui_cmd="GUI=1" ; set queue="gui -XF -Is -tty" + +set nb_cpus="1" +set nb_cpus="2" +set nb_cpus="4" +set nb_cpus="8" +set nb_cpus="12" +set nb_cpus="16" +set nb_cpus="24" +set nb_cpus="32" +set nb_cpus="36" +set nb_cpus="48" + +set my_time = `date '+%Y-%m-%d-%Hh%Mm%Ss'` ; set logname=run_${gui}-${app}-cfg_${config}-mode_${mode}-${instructions}-${my_time}.log ; echo "\n vi ${logname}\n" ; \ +echo "make ${gui_cmd} ${app_cmd} ${config_cmd} ${mode_cmd} ${name_cmd} ${verbose} ${prepare} ${timeout} all\n" > ${logname} && echo "" >>& ${logname} ; \ +bsub -J ${app}-cfg_${config}-mode_${mode}-${instructions} -P cv32e40p -q ${queue} -oo ${logname} -n ${nb_cpus} -R "select[cpuf>=15.0] span[hosts=1] rusage[mem=64G]" make ${gui_cmd} ${app_cmd} ${config_cmd} ${mode_cmd} ${name_cmd} ${verbose} ${prepare} ${timeout} all From 3b9cd10e9764b35ce3844443ffd0cc5039d9350b Mon Sep 17 00:00:00 2001 From: Pascal Gouedo Date: Wed, 12 Jun 2024 12:38:09 +0200 Subject: [PATCH 17/29] Added signoff report generation. Signed-off-by: Pascal Gouedo --- scripts/riscv_isa_formal/common/setup.tcl | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) diff --git a/scripts/riscv_isa_formal/common/setup.tcl b/scripts/riscv_isa_formal/common/setup.tcl index 0bcce5472..428103cd2 100755 --- a/scripts/riscv_isa_formal/common/setup.tcl +++ b/scripts/riscv_isa_formal/common/setup.tcl @@ -427,8 +427,10 @@ if {$app eq "PRC"} { puts "[expr $i * $nb_processes] [expr ((($i + 1) * $nb_processes) - 1)]" puts "\n-INFO- Launching Check Command::\n\ncheck $checks\n" check $checks - report_result -details cd $app_dir + start_message_log round_[expr $i + 1].log + report_result -details + stop_message_log save_database -force round_[expr $i + 1] cd $cwd } @@ -437,13 +439,19 @@ if {$app eq "PRC"} { puts "[expr $nb_round * $nb_processes] [expr (($nb_round * $nb_processes) + $nb_remain - 1)]" puts "\n-INFO- Launching Check Command::\n\ncheck $checks\n" check $checks - report_result -details cd $app_dir + start_message_log round_[expr $i + 1].log + report_result -details + stop_message_log save_database -force round_[expr $nb_round + 1] cd $cwd } + cd $app_dir + start_message_log report_signoff_${app}_${cfg}_${pve_mode}.log report_result -signoff -details + stop_message_log + cd $cwd # set_check_option -prover_exec_order { { disprover1 disprover3 } } # puts "\n-INFO- Launching Check Command::\n\ncheck RV32M.DIV16_a\n" From e77b13bd19f49ef9d2e651fde06ce34c884d34f4 Mon Sep 17 00:00:00 2001 From: Pascal Gouedo Date: Wed, 19 Jun 2024 12:24:16 +0200 Subject: [PATCH 18/29] License header addition except in json files which don't accept comments. Signed-off-by: Pascal Gouedo --- scripts/riscv_isa_formal/common/constraints.sv | 16 ++++++++++++++++ scripts/riscv_isa_formal/common/io.sv | 16 ++++++++++++++++ .../riscv_isa_formal/common/other_bindings.sv | 16 ++++++++++++++++ scripts/riscv_isa_formal/common/setup.tcl | 16 ++++++++++++++++ scripts/riscv_isa_formal/common/setup_mv.tcl | 16 ++++++++++++++++ scripts/riscv_isa_formal/common/t.sh | 16 ++++++++++++++++ scripts/riscv_isa_formal/common/vips/obi_dmem.sv | 16 ++++++++++++++++ scripts/riscv_isa_formal/common/vips/obi_imem.sv | 16 ++++++++++++++++ 8 files changed, 128 insertions(+) diff --git a/scripts/riscv_isa_formal/common/constraints.sv b/scripts/riscv_isa_formal/common/constraints.sv index 02bf694d0..bbd3d60bf 100755 --- a/scripts/riscv_isa_formal/common/constraints.sv +++ b/scripts/riscv_isa_formal/common/constraints.sv @@ -1,3 +1,19 @@ +// Copyright 2024 Siemens EDA +// 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. + /*********************/ // CONSTRAINTS /*********************/ diff --git a/scripts/riscv_isa_formal/common/io.sv b/scripts/riscv_isa_formal/common/io.sv index cb7c9c1e2..0b5f23d3d 100755 --- a/scripts/riscv_isa_formal/common/io.sv +++ b/scripts/riscv_isa_formal/common/io.sv @@ -1,3 +1,19 @@ +// Copyright 2024 Siemens EDA +// 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. + // Data memory interface input dmem_req_we ='0, // Data memory request type input[3:0] dmem_req_be ='0, // Data memory request byte enable diff --git a/scripts/riscv_isa_formal/common/other_bindings.sv b/scripts/riscv_isa_formal/common/other_bindings.sv index 41c929d20..362966093 100755 --- a/scripts/riscv_isa_formal/common/other_bindings.sv +++ b/scripts/riscv_isa_formal/common/other_bindings.sv @@ -1,3 +1,19 @@ +// Copyright 2024 Siemens EDA +// 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. + // Data memory interface .dmem_req_we (data_we_o), .dmem_req_be (data_be_o), diff --git a/scripts/riscv_isa_formal/common/setup.tcl b/scripts/riscv_isa_formal/common/setup.tcl index 428103cd2..793fc9f30 100755 --- a/scripts/riscv_isa_formal/common/setup.tcl +++ b/scripts/riscv_isa_formal/common/setup.tcl @@ -1,3 +1,19 @@ +# Copyright 2024 Siemens EDA +# 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. + proc duration {int_time} { set timeList [list] if {$int_time == 0} { diff --git a/scripts/riscv_isa_formal/common/setup_mv.tcl b/scripts/riscv_isa_formal/common/setup_mv.tcl index 84eb4523c..b87289465 100755 --- a/scripts/riscv_isa_formal/common/setup_mv.tcl +++ b/scripts/riscv_isa_formal/common/setup_mv.tcl @@ -1,3 +1,19 @@ +# Copyright 2024 Siemens EDA +# 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. + if {![info exists ::env(DESIGN_RTL_DIR)]} { set ::env(DESIGN_RTL_DIR) [pwd]/rtl } diff --git a/scripts/riscv_isa_formal/common/t.sh b/scripts/riscv_isa_formal/common/t.sh index eca98e09f..dfa71f9c1 100755 --- a/scripts/riscv_isa_formal/common/t.sh +++ b/scripts/riscv_isa_formal/common/t.sh @@ -1,5 +1,21 @@ #!/bin/bash # +# Copyright 2024 Siemens EDA +# 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. + # This script is a template representing a customization to integrate OneSpin 360 with VCS simulator # # onespin calls the script as follows: diff --git a/scripts/riscv_isa_formal/common/vips/obi_dmem.sv b/scripts/riscv_isa_formal/common/vips/obi_dmem.sv index 7ca5866e2..9efd68737 100755 --- a/scripts/riscv_isa_formal/common/vips/obi_dmem.sv +++ b/scripts/riscv_isa_formal/common/vips/obi_dmem.sv @@ -1,3 +1,19 @@ +// Copyright 2024 Siemens EDA +// 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. + /////////////////////////////////////////////////////////////////////////////////////////////////////////////// // // // General remarks: // diff --git a/scripts/riscv_isa_formal/common/vips/obi_imem.sv b/scripts/riscv_isa_formal/common/vips/obi_imem.sv index 126152246..74f58a918 100755 --- a/scripts/riscv_isa_formal/common/vips/obi_imem.sv +++ b/scripts/riscv_isa_formal/common/vips/obi_imem.sv @@ -1,3 +1,19 @@ +// Copyright 2024 Siemens EDA +// 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. + /////////////////////////////////////////////////////////////////////////////////////////////////////////////// // // // General remarks: // From 9de461c4ce9b46e0e2467ddb32a68bffc4c5fa30 Mon Sep 17 00:00:00 2001 From: Pascal Gouedo Date: Thu, 20 Jun 2024 10:57:22 +0200 Subject: [PATCH 19/29] Changed Siemens EDA to Siemens and Onespin to Questa Processor. Signed-off-by: Pascal Gouedo --- scripts/riscv_isa_formal/README.md | 6 ++-- .../riscv_isa_formal/common/constraints.sv | 2 +- .../riscv_isa_formal/common/core_checker.sv | 29 +++++++++++-------- scripts/riscv_isa_formal/common/io.sv | 2 +- .../riscv_isa_formal/common/other_bindings.sv | 2 +- scripts/riscv_isa_formal/common/setup.tcl | 2 +- scripts/riscv_isa_formal/common/setup_mv.tcl | 2 +- scripts/riscv_isa_formal/common/t.sh | 2 +- .../riscv_isa_formal/common/vips/obi_dmem.sv | 2 +- .../riscv_isa_formal/common/vips/obi_imem.sv | 2 +- 10 files changed, 28 insertions(+), 23 deletions(-) diff --git a/scripts/riscv_isa_formal/README.md b/scripts/riscv_isa_formal/README.md index 84ab2f05e..4ba93b08e 100755 --- a/scripts/riscv_isa_formal/README.md +++ b/scripts/riscv_isa_formal/README.md @@ -1,6 +1,6 @@ # RISC-V ISA Formal Verification -RISC-V ISA Formal Verification methodology has been used with Siemens EDA Onespin tool and its RISC-V ISA Processor Verification app. +RISC-V ISA Formal Verification methodology has been used with Siemens Questa Processor tool and its RISC-V ISA Processor Verification app. ## Configurations @@ -34,8 +34,8 @@ RISC-V ISA Formal Verification methodology has been used with Siemens EDA Onespi Contains all files to create assertions and to launch different tool apps on different configurations and using different modes. > [!CAUTION] -> core_checker.sv contains proprietary information and is only available to Siemens EDA OneSpin customers. -> Once OneSpin licenses have been purchased, this file can be requested to Siemens support center. +> core_checker.sv contains proprietary information and is only available to Siemens Questa Processor customers. +> Once Questa Processor licenses have been purchased, this file can be requested to Siemens support center. ## How to launch a run diff --git a/scripts/riscv_isa_formal/common/constraints.sv b/scripts/riscv_isa_formal/common/constraints.sv index bbd3d60bf..082432653 100755 --- a/scripts/riscv_isa_formal/common/constraints.sv +++ b/scripts/riscv_isa_formal/common/constraints.sv @@ -1,4 +1,4 @@ -// Copyright 2024 Siemens EDA +// Copyright 2024 Siemens // SPDX-License-Identifier: Apache-2.0 WITH SHL-2.1 // // Licensed under the Solderpad Hardware License v 2.1 (the "License"); diff --git a/scripts/riscv_isa_formal/common/core_checker.sv b/scripts/riscv_isa_formal/common/core_checker.sv index 74755ca9f..439347bc5 100755 --- a/scripts/riscv_isa_formal/common/core_checker.sv +++ b/scripts/riscv_isa_formal/common/core_checker.sv @@ -1,21 +1,26 @@ +// Copyright 2024 Siemens +// 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. + /////////////////////////////////////////////////////////////////////////////// // // // RISC-V Checker // // // -// This material contains trade secrets or otherwise confidential // -// information owned by Siemens Industry Software Inc. or its affiliates // -// (collectively, "SISW"), or its licensors. Access to and use of this // -// information is strictly limited as set forth in the Customer's applicable // -// agreements with SISW. // -// // -// This material may not be copied, distributed, or otherwise disclosed // -// outside of the Customer's facilities without the express written // -// permission of SISW, and may not be used in any way not expressly // -// authorized by SISW. // -// // /////////////////////////////////////////////////////////////////////////////// -This file is available only to Siemens EDA OneSpin customers and is available by submitting a request to Siemens support center to get it. +This file is available only to Siemens Questa Processor customers and is available by submitting a request to Siemens support center to get it. diff --git a/scripts/riscv_isa_formal/common/io.sv b/scripts/riscv_isa_formal/common/io.sv index 0b5f23d3d..ae97b2456 100755 --- a/scripts/riscv_isa_formal/common/io.sv +++ b/scripts/riscv_isa_formal/common/io.sv @@ -1,4 +1,4 @@ -// Copyright 2024 Siemens EDA +// Copyright 2024 Siemens // SPDX-License-Identifier: Apache-2.0 WITH SHL-2.1 // // Licensed under the Solderpad Hardware License v 2.1 (the "License"); diff --git a/scripts/riscv_isa_formal/common/other_bindings.sv b/scripts/riscv_isa_formal/common/other_bindings.sv index 362966093..b026c1484 100755 --- a/scripts/riscv_isa_formal/common/other_bindings.sv +++ b/scripts/riscv_isa_formal/common/other_bindings.sv @@ -1,4 +1,4 @@ -// Copyright 2024 Siemens EDA +// Copyright 2024 Siemens // SPDX-License-Identifier: Apache-2.0 WITH SHL-2.1 // // Licensed under the Solderpad Hardware License v 2.1 (the "License"); diff --git a/scripts/riscv_isa_formal/common/setup.tcl b/scripts/riscv_isa_formal/common/setup.tcl index 793fc9f30..8f68ea6b3 100755 --- a/scripts/riscv_isa_formal/common/setup.tcl +++ b/scripts/riscv_isa_formal/common/setup.tcl @@ -1,4 +1,4 @@ -# Copyright 2024 Siemens EDA +# Copyright 2024 Siemens # SPDX-License-Identifier: Apache-2.0 WITH SHL-2.1 # # Licensed under the Solderpad Hardware License v 2.1 (the "License"); diff --git a/scripts/riscv_isa_formal/common/setup_mv.tcl b/scripts/riscv_isa_formal/common/setup_mv.tcl index b87289465..021a6a430 100755 --- a/scripts/riscv_isa_formal/common/setup_mv.tcl +++ b/scripts/riscv_isa_formal/common/setup_mv.tcl @@ -1,4 +1,4 @@ -# Copyright 2024 Siemens EDA +# Copyright 2024 Siemens # SPDX-License-Identifier: Apache-2.0 WITH SHL-2.1 # # Licensed under the Solderpad Hardware License v 2.1 (the "License"); diff --git a/scripts/riscv_isa_formal/common/t.sh b/scripts/riscv_isa_formal/common/t.sh index dfa71f9c1..fe536fc63 100755 --- a/scripts/riscv_isa_formal/common/t.sh +++ b/scripts/riscv_isa_formal/common/t.sh @@ -1,6 +1,6 @@ #!/bin/bash # -# Copyright 2024 Siemens EDA +# Copyright 2024 Siemens # SPDX-License-Identifier: Apache-2.0 WITH SHL-2.1 # # Licensed under the Solderpad Hardware License v 2.1 (the "License"); diff --git a/scripts/riscv_isa_formal/common/vips/obi_dmem.sv b/scripts/riscv_isa_formal/common/vips/obi_dmem.sv index 9efd68737..8f155c2b4 100755 --- a/scripts/riscv_isa_formal/common/vips/obi_dmem.sv +++ b/scripts/riscv_isa_formal/common/vips/obi_dmem.sv @@ -1,4 +1,4 @@ -// Copyright 2024 Siemens EDA +// Copyright 2024 Siemens // SPDX-License-Identifier: Apache-2.0 WITH SHL-2.1 // // Licensed under the Solderpad Hardware License v 2.1 (the "License"); diff --git a/scripts/riscv_isa_formal/common/vips/obi_imem.sv b/scripts/riscv_isa_formal/common/vips/obi_imem.sv index 74f58a918..38bc2f884 100755 --- a/scripts/riscv_isa_formal/common/vips/obi_imem.sv +++ b/scripts/riscv_isa_formal/common/vips/obi_imem.sv @@ -1,4 +1,4 @@ -// Copyright 2024 Siemens EDA +// Copyright 2024 Siemens // SPDX-License-Identifier: Apache-2.0 WITH SHL-2.1 // // Licensed under the Solderpad Hardware License v 2.1 (the "License"); From 052253bcd2cfb691719636d7ce46db1152111c40 Mon Sep 17 00:00:00 2001 From: Pascal Gouedo Date: Wed, 26 Jun 2024 19:05:15 +0200 Subject: [PATCH 20/29] Up-to-date files for RISC-V ISA Formal Verification. Signed-off-by: Pascal Gouedo --- scripts/riscv_isa_formal/Makefile | 2 +- scripts/riscv_isa_formal/README.md | 2 +- ...command example => launch_command_example} | 2 +- .../{common => verif}/constraints.sv | 2 +- .../{common => verif}/core_checker.sv | 0 .../riscv_isa_formal/verif/cv32e40p/info.txt | 17 ++ .../{common => verif/cv32e40p}/setup_mv.tcl | 0 .../riscv_isa_formal/{common => verif}/io.sv | 0 .../{common => verif}/other_bindings.sv | 0 .../{common => verif}/setup.tcl | 162 +++++------------- .../riscv_isa_formal/{common => verif}/t.sh | 0 .../{common => verif}/vips/obi_dmem.sv | 0 .../{common => verif}/vips/obi_imem.sv | 0 13 files changed, 68 insertions(+), 119 deletions(-) rename scripts/riscv_isa_formal/{launch_command example => launch_command_example} (96%) rename scripts/riscv_isa_formal/{common => verif}/constraints.sv (99%) rename scripts/riscv_isa_formal/{common => verif}/core_checker.sv (100%) create mode 100755 scripts/riscv_isa_formal/verif/cv32e40p/info.txt rename scripts/riscv_isa_formal/{common => verif/cv32e40p}/setup_mv.tcl (100%) rename scripts/riscv_isa_formal/{common => verif}/io.sv (100%) rename scripts/riscv_isa_formal/{common => verif}/other_bindings.sv (100%) rename scripts/riscv_isa_formal/{common => verif}/setup.tcl (68%) rename scripts/riscv_isa_formal/{common => verif}/t.sh (100%) rename scripts/riscv_isa_formal/{common => verif}/vips/obi_dmem.sv (100%) rename scripts/riscv_isa_formal/{common => verif}/vips/obi_imem.sv (100%) diff --git a/scripts/riscv_isa_formal/Makefile b/scripts/riscv_isa_formal/Makefile index f344b819b..ac71fb275 100755 --- a/scripts/riscv_isa_formal/Makefile +++ b/scripts/riscv_isa_formal/Makefile @@ -1,4 +1,4 @@ -commonPath=../../common +commonPath=../../verif PREPARE?=0 RTL?=../../cv32e40p/ GUI?=0 diff --git a/scripts/riscv_isa_formal/README.md b/scripts/riscv_isa_formal/README.md index 4ba93b08e..02adc09bb 100755 --- a/scripts/riscv_isa_formal/README.md +++ b/scripts/riscv_isa_formal/README.md @@ -30,7 +30,7 @@ RISC-V ISA Formal Verification methodology has been used with Siemens Questa Pro - Makefile - launch_command_example -### common +### verif Contains all files to create assertions and to launch different tool apps on different configurations and using different modes. > [!CAUTION] diff --git a/scripts/riscv_isa_formal/launch_command example b/scripts/riscv_isa_formal/launch_command_example similarity index 96% rename from scripts/riscv_isa_formal/launch_command example rename to scripts/riscv_isa_formal/launch_command_example index 6b7f3a0a3..804a8dcf1 100755 --- a/scripts/riscv_isa_formal/launch_command example +++ b/scripts/riscv_isa_formal/launch_command_example @@ -19,7 +19,7 @@ set mode=DEF ; set mode_cmd="MODE=${mode}" set mode=DPM ; set mode_cmd="MODE=${mode}" set mode=DPF ; set mode_cmd="MODE=${mode}" -# Prepare the working directory (common files and design copy) or reuse existing one (no copy) +# Prepare the working directory (verif files and design copy) or reuse existing one (no copy) set prepare="" set prepare="PREPARE=1" diff --git a/scripts/riscv_isa_formal/common/constraints.sv b/scripts/riscv_isa_formal/verif/constraints.sv similarity index 99% rename from scripts/riscv_isa_formal/common/constraints.sv rename to scripts/riscv_isa_formal/verif/constraints.sv index 082432653..d615cf6a6 100755 --- a/scripts/riscv_isa_formal/common/constraints.sv +++ b/scripts/riscv_isa_formal/verif/constraints.sv @@ -112,7 +112,7 @@ endfunction `ifdef RESTRICT_REGS // Restrict instruction decoding & register file verification to a subset of registers restrict_regs_c: assume property (disable iff (~rst_n) - restrict_regs(execute.dec) + restrict_regs(my_dec) `ifndef COMPLETENESS `ifndef RESTRICT_REGISTER_INDEX // && (reg_idx<4 || (MISA.C|Zca) && reg_idx inside {5'd8,5'd9}) diff --git a/scripts/riscv_isa_formal/common/core_checker.sv b/scripts/riscv_isa_formal/verif/core_checker.sv similarity index 100% rename from scripts/riscv_isa_formal/common/core_checker.sv rename to scripts/riscv_isa_formal/verif/core_checker.sv diff --git a/scripts/riscv_isa_formal/verif/cv32e40p/info.txt b/scripts/riscv_isa_formal/verif/cv32e40p/info.txt new file mode 100755 index 000000000..76123a920 --- /dev/null +++ b/scripts/riscv_isa_formal/verif/cv32e40p/info.txt @@ -0,0 +1,17 @@ +# Copyright 2024 Siemens +# 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. + +github clone from https://github.com/openhwgroup/cv32e40p.git on the 24th of Jun 2024, tag cv32e40p_v1.8.0 is selected. diff --git a/scripts/riscv_isa_formal/common/setup_mv.tcl b/scripts/riscv_isa_formal/verif/cv32e40p/setup_mv.tcl similarity index 100% rename from scripts/riscv_isa_formal/common/setup_mv.tcl rename to scripts/riscv_isa_formal/verif/cv32e40p/setup_mv.tcl diff --git a/scripts/riscv_isa_formal/common/io.sv b/scripts/riscv_isa_formal/verif/io.sv similarity index 100% rename from scripts/riscv_isa_formal/common/io.sv rename to scripts/riscv_isa_formal/verif/io.sv diff --git a/scripts/riscv_isa_formal/common/other_bindings.sv b/scripts/riscv_isa_formal/verif/other_bindings.sv similarity index 100% rename from scripts/riscv_isa_formal/common/other_bindings.sv rename to scripts/riscv_isa_formal/verif/other_bindings.sv diff --git a/scripts/riscv_isa_formal/common/setup.tcl b/scripts/riscv_isa_formal/verif/setup.tcl similarity index 68% rename from scripts/riscv_isa_formal/common/setup.tcl rename to scripts/riscv_isa_formal/verif/setup.tcl index 8f68ea6b3..f545d6b68 100755 --- a/scripts/riscv_isa_formal/common/setup.tcl +++ b/scripts/riscv_isa_formal/verif/setup.tcl @@ -14,6 +14,9 @@ # See the License for the specific language governing permissions and # limitations under the License. +# clean up local files (that would be read instead of the one in the include dir due to local folder being first in include list) +file delete RISCV_ISA.sv bind.sv generated_assertions.sv vplan.csv + proc duration {int_time} { set timeList [list] if {$int_time == 0} { @@ -32,14 +35,15 @@ proc duration {int_time} { } } -proc quantify_run {{cmd_limit 0} {run 0} {no_cuts {}} {limit_scale 2.0} {effort 4} {skip_effort_level 0} {html_dir {}} {result_file {}} {checks {}} {prev_run_result {}} {skip_files {}}} { +proc quantify_run {{cmd_limit 0} {run 0} {limit_scale 2.0} {effort 4} {skip_effort_level 0} {html_dir {}} {result_file {}} {checks {}} {prev_run_result {}} {skip_files {}}} { puts "\n-INFO- Start of Quantify Run ($run)::\n\nChecks Included::\n\n$checks" set_limit -command_real_time $cmd_limit set run_start_t [clock seconds] - puts "\n-INFO- Launching Quantify Command::\n\nquantify -assume_hold -additional_args \[list $no_cuts -limit_scale $limit_scale -use_single_prover\] -effort $effort -skip_effort_level $skip_effort_level -html $html_dir -save $result_file -checks $checks -incremental $prev_run_result -skip_files $skip_files\n" - catch {quantify -assume_hold -additional_args [list $no_cuts -limit_scale $limit_scale -use_single_prover] -effort $effort -skip_effort_level $skip_effort_level -html $html_dir -save $result_file -checks $checks -incremental $prev_run_result -skip_files $skip_files} + set cmd [list quantify -assume_hold -additional_args [list -no_cuts -use_single_prover -limit_scale $limit_scale] -effort $effort -skip_effort_level $skip_effort_level -html $html_dir -save $result_file -checks $checks -incremental $prev_run_result -skip_files $skip_files] + puts "\n-INFO- Launching Quantify Command::\n\n$cmd\n" + catch $cmd set run_end_t [expr [clock seconds] - $run_start_t] set_limit -default @@ -48,11 +52,11 @@ proc quantify_run {{cmd_limit 0} {run 0} {no_cuts {}} {limit_scale 2.0} {effort ## 0. DESIGN SETUP ## -### SETTING UP THE DESIRED CONFIGURATION, RUN & APP ### -## source the setup.inc as the following: [onespin -i setup.inc ] -## arg1: what configuration to set . +### SETTING UP THE DESIRED CONFIGURATION, RUN & APP ### +## source the setup.inc as the following: [onespin -i setup.inc ] +## arg1: what configuration to set . ## arg2: what processor verification mode to set . -## arg3: what app to launch on top of the processor app. +## arg3: what app to launch on top of the processor app. ## ------------------------------------------------------------------------------------------------------------------ set configs [dict create \ @@ -161,7 +165,7 @@ set apps [dict create \ ] if {$::argc>0} { - lassign $::argv cfg pve_mode app + lassign $::argv cfg pve_mode app prev_run if {$cfg ni [dict keys $configs]} { onespin::message -error "Only configurations [join [dict keys $configs] ,] are supported!" return -code error @@ -171,7 +175,7 @@ if {$::argc>0} { return -code error } elseif {$pve_mode eq "DPF" && $cfg in {"DEF" "XP" "XPXC"} } { onespin::message -error "Floating-point configuration must be selected in order to perform data path verification!" - return -code error + return -code error } if {$app ni [dict keys $apps]} { onespin::message -error "Only apps [join [dict keys $apps] ,] are supported!" @@ -179,28 +183,31 @@ if {$::argc>0} { } } else { if {[get_tool_info -gui]} { - set cfg [string index [onespin::ask_user -default 0 -alternatives [lmap {k d} $configs {string cat "$k - " [dict get $d description]}] "Select which RISC-V configuration to set up:"] 0] - set pve_mode [string index [onespin::ask_user -default "DEF" -alternatives [lmap {k d} $pve_modes {string cat "$k - " [dict get $d description]}] "Select which processor verification mode to set:"] 0] - set app [string index [onespin::ask_user -default "PRC" -alternatives [lmap {k d} $apps {string cat "$k - " [dict get $d description]}] "Select which app to launch:"] 0] + set cfg [lindex [onespin::ask_user -default DEF -alternatives [lmap {k d} $configs {string cat "$k - " [dict get $d description]}] "Select which RISC-V configuration to set up:"] 0] + set pve_mode [lindex [onespin::ask_user -default "DEF" -alternatives [lmap {k d} $pve_modes {string cat "$k - " [dict get $d description]}] "Select which processor verification mode to set:"] 0] + set app [lindex [onespin::ask_user -default "PRC" -alternatives [lmap {k d} $apps {string cat "$k - " [dict get $d description]}] "Select which app to launch:"] 0] } else { set cfg "DEF" set pve_mode "DEF" set app "PRC" } } -set target cv32e40p_top -set core_inst core_i -set prefix ${core_inst}. ## ### ADJUST TO READ-IN THE NEW DESIGN ### onespin::set_parameter disable_intermediate_arithmetic_signals 1 set cwd [pwd] set_session_option -naming_style sv +set target cv32e40p_top +if {$target=="cv32e40p_top"} { + set core_inst core_i + set prefix ${core_inst}. +} set_compile_option {*}[dict get $apps $app compile] set_elaborate_option {*}[dict get $configs $cfg elab] -top $target +# The RTL directory cloned from GitHub, where tag cv32e40p_v1.8.0 is checked out cd cv32e40p -source $cwd/setup_mv.tcl +source setup_mv.tcl set_reset_sequence -low rst_ni cd $cwd @@ -212,6 +219,7 @@ file mkdir $pve_mode_dir file mkdir $app_dir ## + ### PROCESSOR APP FLOW ### ## --------------------------------------------------------------------------------------------------------------------------------- @@ -247,6 +255,7 @@ file mkdir $app_dir ## 0. APP SETUP ## package require processor_integrity +processor_integrity::clear_data -core_checker_version 2024.2 ### APPEND THE FOLLOWING SET OF DEFINES (ONLY IF NECESSARY) ### ## --------------------------------------------------------------------------------------------------------------------------------- @@ -385,38 +394,17 @@ foreach i ${rtl_signals_to_disassemble} { } ## -#set nb_processes 2 -#set nb_processes 3 -#set nb_processes 4 -#set nb_processes 5 -#set nb_processes 6 -#set nb_processes 8 -#set nb_processes 12 -set nb_processes 16 -#set nb_processes 24 -#set nb_processes 32 - -set_check_option -verbose -set_check_option -local_processes $nb_processes -set_check_option -engine_licensing unlimited - -puts "\n-INFO- Launching $app app in $pve_mode mode with $nb_processes parallel processes.\n" - -#set_check_option -prover_exec_order { { approver1 approver4 prover2:0 prover2:8 prover2:11 disprover1 disprover3 } } -set_check_option -prover_exec_order { { approver1 prover2:0 prover2:8 prover2:11 } } -#set_check_option -disprover1_steps 40 -disprover3_steps 40 - -check_consistency -category model_building -effort maximum exclude_check [get_checks -filter name=~"*hdl*"||name=~"*FSQRT_S_a*"||name=~"**FDIV_S_a*"] +check_consistency -category model_building -effort maximum set DEF_checks [lsort -dictionary [get_checks -filter excluded==false&&(type==property||type==assertion)]] set DPM_checks [lsort -dictionary [get_checks -filter excluded==false&&(name=~"*RV32M.*"||name=~"*RV32X.CV_XDOT*"||name=~"*RV32X.CV_MUL*"||name=~"*RV32X.CV_MAC*"||name=~"*RV32X.CV_CPLXMUL*")]] set DPF_checks [lsort -dictionary [get_checks -filter excluded==false&&(name=~"*RV32F.*"||name=~"*RV32Zfinx.*")]] set group_1_checks [lsort -dictionary [concat core_i.RV_chk.ops.RESET_a [get_checks -filter excluded==false&&type==assertion]]] -set group_2_checks [lsort -dictionary [list core_i.RV_chk.ops.XCPT_IF_ID_a core_i.RV_chk.RV32C.ARITH_a core_i.RV_chk.RV32C.BRANCH_Taken_a core_i.RV_chk.RV32C.BRANCH_a core_i.RV_chk.RV32C.JUMP_a core_i.RV_chk.RV32I.EBREAK_BreakPoint_a core_i.RV_chk.RV32I.MEM_MultiAccess_a core_i.RV_chk.RV32I.xRET_a core_i.RV_chk.RV32X.CV_ADD_X_a core_i.RV_chk.RV32X.CV_BITMAN_OTHER_a core_i.RV_chk.RV32X.CV_EXTRACTX_X_a core_i.RV_chk.RV32X.CV_INSERTX_a core_i.RV_chk.RV32X.CV_PACKXX_X_a core_i.RV_chk.RV32X.CV_SETUPX_a core_i.RV_chk.RV32X.CV_SHUFFLE2_X_a core_i.RV_chk.RV32Zicsr.CSRx_a]] -set group_3_checks [lsort -dictionary [list core_i.RV_chk.ops.BUBBLE_a core_i.RV_chk.RV32I.ARITH_a core_i.RV_chk.RV32I.EBREAK_HaltReq_a core_i.RV_chk.RV32I.ECALL_a core_i.RV_chk.RV32I.FENCE_a core_i.RV_chk.RV32I.WFI_a core_i.RV_chk.RV32X.CV_ABS_X_a core_i.RV_chk.RV32X.CV_CLIPXX_a core_i.RV_chk.RV32X.CV_CMPEQ_X_a core_i.RV_chk.RV32X.CV_EXTRACTXX_a core_i.RV_chk.RV32X.CV_EXTXX_a core_i.RV_chk.RV32X.CV_INSERT_X_a core_i.RV_chk.RV32X.CV_SX_I_a core_i.RV_chk.RV32X.CV_SX_RI_a core_i.RV_chk.RV32X.CV_ADDXXNR_a core_i.RV_chk.RV32X.CV_SHUFFLEIX_SCI_B_a core_i.RV_chk.RV32X.CV_BSETX_a core_i.RV_chk.RV32X.CV_BXXIMM_Taken_a core_i.RV_chk.RV32X.CV_ENDX_a core_i.RV_chk.RV32X.CV_LXX_I_a core_i.RV_chk.RV32X.CV_LXX_RI_a core_i.RV_chk.RV32X.CV_SLL_X_a core_i.RV_chk.RV32X.CV_STARTX_a core_i.RV_chk.RV32X.CV_ADD_DIVX_a core_i.RV_chk.RV32X.CV_ADDXXN_a core_i.RV_chk.RV32X.CV_AVGU_X_a core_i.RV_chk.RV32X.CV_BCLRX_a core_i.RV_chk.RV32X.CV_SUB_DIVX_a core_i.RV_chk.RV32X.CV_SUBROTMJ_X_a core_i.RV_chk.RV32X.CV_SUBXXN_a core_i.RV_chk.RV32X.CV_SUBXXNR_a core_i.RV_chk.RV32X.CV_MAXU_X_a]] -set group_4_checks [lsort -dictionary [concat [get_checks -filter excluded==false&&name=~"*RV32X.CV_ELW*"] core_i.RV_chk.RV32I.EBREAK_ForcedEntry_a core_i.RV_chk.RV32X.CV_COUNTX_a core_i.RV_chk.RV32X.CV_LXX_R_a core_i.RV_chk.RV32X.CV_MAXX_a core_i.RV_chk.RV32X.CV_SX_R_a core_i.RV_chk.RV32C.MEM_a core_i.RV_chk.RV32C.MEM_MultiAccess_a core_i.RV_chk.RV32I.BRANCH_a core_i.RV_chk.RV32I.BRANCH_Taken_a core_i.RV_chk.RV32I.JUMP_a core_i.RV_chk.RV32I.MEM_a core_i.RV_chk.RV32X.CV_ABS_a core_i.RV_chk.RV32X.CV_AND_X_a core_i.RV_chk.RV32X.CV_AVG_X_a core_i.RV_chk.RV32X.CV_BXXIMM_a core_i.RV_chk.RV32X.CV_CMPGE_X_a core_i.RV_chk.RV32X.CV_CMPGEU_X_a core_i.RV_chk.RV32X.CV_CMPGT_X_a core_i.RV_chk.RV32X.CV_CMPGTU_X_a core_i.RV_chk.RV32X.CV_CMPLE_X_a core_i.RV_chk.RV32X.CV_CMPLEU_X_a core_i.RV_chk.RV32X.CV_CMPLT_X_a core_i.RV_chk.RV32X.CV_CMPLTU_X_a core_i.RV_chk.RV32X.CV_CMPNE_X_a core_i.RV_chk.RV32X.CV_CPLXCONJ_a core_i.RV_chk.RV32X.CV_LXX_I_MultiAccess_a core_i.RV_chk.RV32X.CV_LXX_R_MultiAccess_a core_i.RV_chk.RV32X.CV_LXX_RI_MultiAccess_a core_i.RV_chk.RV32X.CV_MAX_X_a core_i.RV_chk.RV32X.CV_MIN_X_a core_i.RV_chk.RV32X.CV_MINU_X_a core_i.RV_chk.RV32X.CV_MINX_a core_i.RV_chk.RV32X.CV_OR_X_a core_i.RV_chk.RV32X.CV_SHUFFLE_X_a core_i.RV_chk.RV32X.CV_SLEX_a core_i.RV_chk.RV32X.CV_SRA_X_a core_i.RV_chk.RV32X.CV_SRL_X_a core_i.RV_chk.RV32X.CV_SUB_X_a core_i.RV_chk.RV32X.CV_SX_I_MultiAccess_a core_i.RV_chk.RV32X.CV_SX_R_MultiAccess_a core_i.RV_chk.RV32X.CV_SX_RI_MultiAccess_a core_i.RV_chk.RV32X.CV_XOR_X_a core_i.RV_chk.RV32Zifencei.FENCE_I_a]] +set group_2_checks [lsort -dictionary [list core_i.RV_chk.xcpt.XCPT_IF_ID_a core_i.RV_chk.RV32C.ARITH_a core_i.RV_chk.RV32C.BRANCH_Taken_a core_i.RV_chk.RV32C.BRANCH_a core_i.RV_chk.RV32C.JUMP_a core_i.RV_chk.xcpt.EBREAK_a core_i.RV_chk.RV32I.MEM_MultiAccess_a core_i.RV_chk.RV32I.RETURN_a core_i.RV_chk.RV32X.CV_ADD_X_a core_i.RV_chk.RV32X.CV_BITMAN_OTHER_a core_i.RV_chk.RV32X.CV_EXTRACTX_X_a core_i.RV_chk.RV32X.CV_INSERTX_a core_i.RV_chk.RV32X.CV_PACKXX_X_a core_i.RV_chk.RV32X.CV_SETUPX_a core_i.RV_chk.RV32X.CV_SHUFFLE2_X_a core_i.RV_chk.RV32Zicsr.CSRx_a]] +set group_3_checks [lsort -dictionary [list core_i.RV_chk.ops.BUBBLE_a core_i.RV_chk.RV32I.ARITH_a core_i.RV_chk.xcpt.ECALL_a core_i.RV_chk.RV32I.FENCE_a core_i.RV_chk.RV32I.WFI_a core_i.RV_chk.RV32X.CV_ABS_X_a core_i.RV_chk.RV32X.CV_CLIPXX_a core_i.RV_chk.RV32X.CV_CMPEQ_X_a core_i.RV_chk.RV32X.CV_EXTRACTXX_a core_i.RV_chk.RV32X.CV_EXTXX_a core_i.RV_chk.RV32X.CV_INSERT_X_a core_i.RV_chk.RV32X.CV_SX_I_a core_i.RV_chk.RV32X.CV_SX_RI_a core_i.RV_chk.RV32X.CV_ADDXXNR_a core_i.RV_chk.RV32X.CV_SHUFFLEIX_SCI_B_a core_i.RV_chk.RV32X.CV_BSETX_a core_i.RV_chk.RV32X.CV_BXXIMM_Taken_a core_i.RV_chk.RV32X.CV_ENDX_a core_i.RV_chk.RV32X.CV_LXX_I_a core_i.RV_chk.RV32X.CV_LXX_RI_a core_i.RV_chk.RV32X.CV_SLL_X_a core_i.RV_chk.RV32X.CV_STARTX_a core_i.RV_chk.RV32X.CV_ADD_DIVX_a core_i.RV_chk.RV32X.CV_ADDXXN_a core_i.RV_chk.RV32X.CV_AVGU_X_a core_i.RV_chk.RV32X.CV_BCLRX_a core_i.RV_chk.RV32X.CV_SUB_DIVX_a core_i.RV_chk.RV32X.CV_SUBROTMJ_X_a core_i.RV_chk.RV32X.CV_SUBXXN_a core_i.RV_chk.RV32X.CV_SUBXXNR_a core_i.RV_chk.RV32X.CV_MAXU_X_a]] +set group_4_checks [lsort -dictionary [concat [get_checks -filter excluded==false&&name=~"*RV32X.CV_ELW*"] core_i.RV_chk.RV32X.CV_COUNTX_a core_i.RV_chk.RV32X.CV_LXX_R_a core_i.RV_chk.RV32X.CV_MAXX_a core_i.RV_chk.RV32X.CV_SX_R_a core_i.RV_chk.RV32C.MEM_a core_i.RV_chk.RV32C.MEM_MultiAccess_a core_i.RV_chk.RV32I.BRANCH_a core_i.RV_chk.RV32I.BRANCH_Taken_a core_i.RV_chk.RV32I.JUMP_a core_i.RV_chk.RV32I.MEM_a core_i.RV_chk.RV32X.CV_ABS_a core_i.RV_chk.RV32X.CV_AND_X_a core_i.RV_chk.RV32X.CV_AVG_X_a core_i.RV_chk.RV32X.CV_BXXIMM_a core_i.RV_chk.RV32X.CV_CMPGE_X_a core_i.RV_chk.RV32X.CV_CMPGEU_X_a core_i.RV_chk.RV32X.CV_CMPGT_X_a core_i.RV_chk.RV32X.CV_CMPGTU_X_a core_i.RV_chk.RV32X.CV_CMPLE_X_a core_i.RV_chk.RV32X.CV_CMPLEU_X_a core_i.RV_chk.RV32X.CV_CMPLT_X_a core_i.RV_chk.RV32X.CV_CMPLTU_X_a core_i.RV_chk.RV32X.CV_CMPNE_X_a core_i.RV_chk.RV32X.CV_CPLXCONJ_a core_i.RV_chk.RV32X.CV_LXX_I_MultiAccess_a core_i.RV_chk.RV32X.CV_LXX_R_MultiAccess_a core_i.RV_chk.RV32X.CV_LXX_RI_MultiAccess_a core_i.RV_chk.RV32X.CV_MAX_X_a core_i.RV_chk.RV32X.CV_MIN_X_a core_i.RV_chk.RV32X.CV_MINU_X_a core_i.RV_chk.RV32X.CV_MINX_a core_i.RV_chk.RV32X.CV_OR_X_a core_i.RV_chk.RV32X.CV_SHUFFLE_X_a core_i.RV_chk.RV32X.CV_SLEX_a core_i.RV_chk.RV32X.CV_SRA_X_a core_i.RV_chk.RV32X.CV_SRL_X_a core_i.RV_chk.RV32X.CV_SUB_X_a core_i.RV_chk.RV32X.CV_SX_I_MultiAccess_a core_i.RV_chk.RV32X.CV_SX_R_MultiAccess_a core_i.RV_chk.RV32X.CV_SX_RI_MultiAccess_a core_i.RV_chk.RV32X.CV_XOR_X_a core_i.RV_chk.RV32Zifencei.FENCE_I_a]] set group_5_checks [lsort -dictionary [get_checks -filter excluded==false&&(name=~"*RV32M.DIV16_a*"||name=~"*RV32M.DIV32_a*"||name=~"*RV32M.MUL_a*"||name=~"*RV32X.CV_XDOT*"||name=~"*RV32X.CV_MUL*"||name=~"*RV32X.CV_MAC*"||name=~"*RV32X.CV_CPLXMUL*")]] set group_6_checks [lsort -dictionary [get_checks -filter excluded==false&&(name=~"*RV32F.*"||name=~"*RV32Zfinx.*")]] @@ -429,58 +417,13 @@ puts "\n-INFO- Cut signals::\n\n\t$rtl_signals_to_cut\n" if {$app eq "PRC"} { -# set_check_option -prover_exec_order { { approver1 approver4 prover2:0 prover2:8 prover2:11 disprover1 disprover3 } } - set_check_option -prover_exec_order { { approver1 prover2:0 prover2:8 prover2:11 } } -# set_check_option -prover_exec_order { { disprover1 disprover3 } } -disprover1_steps 20 -disprover3_steps 20 - - set all_checks [set ${pve_mode}_checks] - set checks_nb [llength $all_checks] - set nb_round [expr $checks_nb / $nb_processes] - set nb_remain [expr $checks_nb % $nb_processes] - puts "nb_round = $nb_round, nb_remain = $nb_remain" - for {set i 0} {$i < $nb_round} {incr i} { - set checks [lrange $all_checks [expr $i * $nb_processes] [expr ((($i + 1) * $nb_processes) - 1)]] - puts "[expr $i * $nb_processes] [expr ((($i + 1) * $nb_processes) - 1)]" - puts "\n-INFO- Launching Check Command::\n\ncheck $checks\n" - check $checks - cd $app_dir - start_message_log round_[expr $i + 1].log - report_result -details - stop_message_log - save_database -force round_[expr $i + 1] - cd $cwd - } - if {$nb_remain > 0} { - set checks [lrange $all_checks [expr $nb_round * $nb_processes] [expr (($nb_round * $nb_processes) + $nb_remain - 1)]] - puts "[expr $nb_round * $nb_processes] [expr (($nb_round * $nb_processes) + $nb_remain - 1)]" - puts "\n-INFO- Launching Check Command::\n\ncheck $checks\n" - check $checks - cd $app_dir - start_message_log round_[expr $i + 1].log - report_result -details - stop_message_log - save_database -force round_[expr $nb_round + 1] - cd $cwd - } - - cd $app_dir - start_message_log report_signoff_${app}_${cfg}_${pve_mode}.log - report_result -signoff -details - stop_message_log - cd $cwd - -# set_check_option -prover_exec_order { { disprover1 disprover3 } } -# puts "\n-INFO- Launching Check Command::\n\ncheck RV32M.DIV16_a\n" -# check [get_checks -filter name=~"*RV32M.DIV16_a*"] -# cd $app_dir -# save_database -force -# cd $cwd - -} +# set_check_option -prover_exec_order { { disprover1 disprover3 } } -disprover1_steps 20 -disprover3_steps 20 +# check [set ${pve_mode}_checks] +# report_result -details -if {$app eq "QTF"} { +} - source basics.tcl.obf +if {$app eq "QTF"} { set_check_option -prover_exec_order { { disprover1 disprover3 } } -disprover1_steps 20 -disprover3_steps 20 @@ -501,27 +444,24 @@ if {$app eq "QTF"} { puts "Group (${i}) checks: Total number of checks is: [llength [set group_${i}_checks]]" } -# for {set i 1} {$i < 7} {incr i} { - - set i 5 + for {set i 1} {$i < 7} {incr i} { - start_message_log ${log}${i}.log + start_message_log -force ${log}${i}.log if {$i == 1} { - quantify_run 0 $i {-no_cuts} 1.0 2 1 ${html}_L2_S1_R${i} ${results}${i} $group_1_checks {} {} + quantify_run 0 $i 1.0 2 1 ${html}_L2_S1_R${i} ${results}${i} $group_1_checks {} {} } elseif {$i == 2} { - quantify_run 0 $i {-no_cuts} 4.0 4 3 ${html}_L4_S4_R${i} ${results}${i} $group_2_checks ${results}[expr $i-1] $skipped_files + quantify_run 0 $i 4.0 4 3 ${html}_L4_S4_R${i} ${results}${i} $group_2_checks ${results}[expr $i-1] $skipped_files } elseif {$i == 3} { - quantify_run 0 $i {-no_cuts} 2.0 4 3 ${html}_L4_S2_R${i} ${results}${i} $group_3_checks ${results}[expr $i-1] $skipped_files + quantify_run 0 $i 2.0 4 3 ${html}_L4_S2_R${i} ${results}${i} $group_3_checks ${results}[expr $i-1] $skipped_files } elseif {$i == 4} { - quantify_run 0 $i {-no_cuts} 2.0 4 3 ${html}_L4_S2_R${i} ${results}${i} $group_4_checks ${results}[expr $i-1] $skipped_files + quantify_run 0 $i 2.0 4 3 ${html}_L4_S2_R${i} ${results}${i} $group_4_checks ${results}[expr $i-1] $skipped_files } elseif {$i == 5} { -# quantify_run 0 $i {-no_cuts} 4.0 4 3 ${html}_L4_S4_R${i} ${results}${i} $group_5_checks ${results}[expr $i-1] $skipped_files - quantify_run 0 $i {} 6.0 4 3 ${html}_L4_S4_R${i} ${results}${i} $group_5_checks ${results}[expr $i-1] $skipped_files + quantify_run 0 $i 4.0 4 3 ${html}_L4_S4_R${i} ${results}${i} $group_5_checks ${results}[expr $i-1] $skipped_files } elseif {($i == 6) && ("CFG_F" in $defines || "CFG_ZFINX" in $defines)} { - quantify_run 0 $i {-no_cuts} 4.0 4 3 ${html}_L4_S4_R${i} ${results}${i} $group_6_checks ${results}[expr $i-1] {} + quantify_run 0 $i 4.0 4 3 ${html}_L4_S4_R${i} ${results}${i} $group_6_checks ${results}[expr $i-1] {} } stop_message_log -# } + } } elseif {$pve_mode eq "DPM"} { @@ -532,11 +472,7 @@ if {$app eq "QTF"} { } start_message_log ${log}${i}.log -# quantify_run 0 $i {-no_cuts} 4.0 4 3 ${html}_L4_S4_R${i} ${results}${i} $group_5_checks {} $skipped_files -# file copy -force ${cfg_dir}/DEF/QTF/qtf_results_${cfg}_DEF_R[expr $i-1] ${cfg_dir}/DEF/QTF/qtf_results_${cfg}_DEF_R[expr $i-1]-Xr -# fileutil::updateInPlace ${cfg_dir}/DEF/QTF/qtf_results_${cfg}_DEF_R[expr $i-1] [list string map [list " Xr" " U0"]] -# quantify_run 0 $i {-no_cuts} 4.0 4 3 ${html}_L4_S4_R${i} ${results}${i} $group_5_checks ${cfg_dir}/DEF/QTF/qtf_results_${cfg}_DEF_R[expr $i-1] $skipped_files - quantify_run 0 $i {} 6.0 4 3 ${html}_L4_S4_R${i} ${results}${i} $group_5_checks ${cfg_dir}/DEF/QTF/qtf_results_${cfg}_DEF_R[expr $i-1] $skipped_files + quantify_run 0 $i 4.0 4 3 ${html}_L4_S4_R${i} ${results}${i} $group_5_checks ${cfg_dir}/DEF/QTF/qtf_results_${cfg}_DEF_R[expr $i-1] $skipped_files stop_message_log } elseif {$pve_mode eq "DPF"} { @@ -544,15 +480,12 @@ if {$app eq "QTF"} { set i 8 start_message_log ${log}${i}.log -# quantify_run 0 $i -no_cuts 2.0 4 3 ${html}_L4_S4_R${i} ${results}${i} $group_6_checks {} {} -# file copy -force ${cfg_dir}/DPM/QTF/qtf_results_${cfg}_DPM_R[expr $i-1] ${cfg_dir}/DPM/QTF/qtf_results_${cfg}_DPM_R[expr $i-1]-Xr -# fileutil::updateInPlace ${cfg_dir}/DPM/QTF/qtf_results_${cfg}_DPM_R[expr $i-1] [list string map [list " Xr" " U0"]] - quantify_run 0 $i -no_cuts 2.0 4 3 ${html}_L4_S4_R${i} ${results}${i} $group_6_checks ${cfg_dir}/DPM/QTF/qtf_results_${cfg}_DPM_R[expr $i-1] {} + quantify_run 0 $i 2.0 4 3 ${html}_L4_S4_R${i} ${results}${i} $group_6_checks ${cfg_dir}/DPM/QTF/qtf_results_${cfg}_DPM_R[expr $i-1] {} stop_message_log } -} +} if {$app eq "VCI"} { @@ -581,8 +514,7 @@ if {$app eq "VCI"} { start_message_log ${log}.log puts "\n-INFO- Launching VCI Command::\nexport_quantify_coverage -call_script t.sh -generate_flist -output_dir $output_dir -checks $checks ${results}${i}\n" - export_quantify_coverage -call_script t.sh -generate_flist -output_dir $output_dir -checks $checks ${results}${i} + export_quantify_coverage -call_script t.sh -generate_flist -output_dir $output_dir -checks $checks ${results}${i} stop_message_log -# report_quantify_result -quantify_result qtf_results_run_${run} -html html_results_run_${run} } diff --git a/scripts/riscv_isa_formal/common/t.sh b/scripts/riscv_isa_formal/verif/t.sh similarity index 100% rename from scripts/riscv_isa_formal/common/t.sh rename to scripts/riscv_isa_formal/verif/t.sh diff --git a/scripts/riscv_isa_formal/common/vips/obi_dmem.sv b/scripts/riscv_isa_formal/verif/vips/obi_dmem.sv similarity index 100% rename from scripts/riscv_isa_formal/common/vips/obi_dmem.sv rename to scripts/riscv_isa_formal/verif/vips/obi_dmem.sv diff --git a/scripts/riscv_isa_formal/common/vips/obi_imem.sv b/scripts/riscv_isa_formal/verif/vips/obi_imem.sv similarity index 100% rename from scripts/riscv_isa_formal/common/vips/obi_imem.sv rename to scripts/riscv_isa_formal/verif/vips/obi_imem.sv From 211d290c3b2cd8c32a9c4f75342a6c197ccaa337 Mon Sep 17 00:00:00 2001 From: Pascal Gouedo Date: Thu, 27 Jun 2024 11:31:35 +0200 Subject: [PATCH 21/29] Updated PRC commands. Signed-off-by: Pascal Gouedo --- scripts/riscv_isa_formal/verif/setup.tcl | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/scripts/riscv_isa_formal/verif/setup.tcl b/scripts/riscv_isa_formal/verif/setup.tcl index f545d6b68..c1c2639f7 100755 --- a/scripts/riscv_isa_formal/verif/setup.tcl +++ b/scripts/riscv_isa_formal/verif/setup.tcl @@ -417,9 +417,9 @@ puts "\n-INFO- Cut signals::\n\n\t$rtl_signals_to_cut\n" if {$app eq "PRC"} { -# set_check_option -prover_exec_order { { disprover1 disprover3 } } -disprover1_steps 20 -disprover3_steps 20 -# check [set ${pve_mode}_checks] -# report_result -details + set_check_option -prover_exec_order { { approver1 approver4 prover2:0 prover2:8 prover2:11 } } + check [set ${pve_mode}_checks] + report_result -signoff -details } From 6993959245643f0c04d04a60c3dd83964f29aea0 Mon Sep 17 00:00:00 2001 From: Pascal Gouedo Date: Thu, 27 Jun 2024 11:43:51 +0200 Subject: [PATCH 22/29] Added Siemens Questa Processor version requirement. Signed-off-by: Pascal Gouedo --- scripts/riscv_isa_formal/README.md | 3 +++ 1 file changed, 3 insertions(+) diff --git a/scripts/riscv_isa_formal/README.md b/scripts/riscv_isa_formal/README.md index 02adc09bb..8999d0be2 100755 --- a/scripts/riscv_isa_formal/README.md +++ b/scripts/riscv_isa_formal/README.md @@ -39,6 +39,9 @@ Contains all files to create assertions and to launch different tool apps on dif ## How to launch a run +> [!CAUTION] +> Siemens Questa Processor 2024.2 and above must be used. + - Locally clone cv32e40p github repository or make a symbolic link to an existing repo. - launch following command:
make GUI=1 APP=PRC CONF=XP MODE=DEF NAME=v1_8_0 VERBOSE=1 PREPARE=1 all >&! run_gui-PRC-cfg_XP-mode_DEF-v1_8_0.log From 9aa989003306c97f59d685f2a9f7a39b188d5111 Mon Sep 17 00:00:00 2001 From: Pascal Gouedo Date: Thu, 6 Jun 2024 17:40:09 +0200 Subject: [PATCH 23/29] Cleanup. Signed-off-by: Pascal Gouedo --- docs/source/corev_hw_loop.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/source/corev_hw_loop.rst b/docs/source/corev_hw_loop.rst index 6653ce1f5..e28345d85 100644 --- a/docs/source/corev_hw_loop.rst +++ b/docs/source/corev_hw_loop.rst @@ -181,7 +181,7 @@ If ebreak is used to enter in Debug Mode (:ref:`ebreak_scenario_2`) and put at t When ebreak instruction is used as Software Breakpoint by a debugger when in debug mode and is placed at the last instruction location of an HWLoop in instruction memory, no special management is foreseen. When executing the Software Breakpoint/ebreak instruction, control is given back to the debugger which will manage the different cases. -For instance in Single-Step case, original instruction is put back in instruction memory, a Single-Step command is executed on this last instruction (with desgin updating PC and lpcountX to correct values) and Software Breakpoint/ebreak is put back by the debugger in memory. +For instance in Single-Step case, original instruction is put back in instruction memory, a Single-Step command is executed on this last instruction (with design updating PC and lpcountX to correct values) and Software Breakpoint/ebreak is put back by the debugger in memory. When ecall instruction is used by a debugger to execute System Calls and is placed at the last instruction location of an HWLoop in instruction memory, debugger ecall handler in debug program should do the same than described above for application case. From 2ef116360aa8d40f9b083a7e9d4fa3dd9c308817 Mon Sep 17 00:00:00 2001 From: Pascal Gouedo Date: Wed, 3 Jul 2024 18:17:20 +0200 Subject: [PATCH 24/29] Added FPU sleep information. Signed-off-by: Pascal Gouedo --- docs/source/fpu.rst | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/docs/source/fpu.rst b/docs/source/fpu.rst index 23245a970..5a93a45e3 100644 --- a/docs/source/fpu.rst +++ b/docs/source/fpu.rst @@ -163,9 +163,6 @@ host the floating-point operands. The latency of the individual instructions are explained in :ref:`instructions_latency_table` table. -To allow FPU unit to be put in sleep mode at the same time the core is doing so, a clock gating cell is instantiated in ``cv32e40p_top`` top level module as well -with its enable signal being inverted ``core_sleep_o`` core output. - FP CSR ------ @@ -175,6 +172,11 @@ exceptions that occurred since it was last reset and the rounding mode. :ref:`csr-fflags` and :ref:`csr-frm` can be accessed directly or via :ref:`csr-fcsr` which is mapped to those two registers. +FPU Sleeping mode +----------------- + +To reduce power consumption, FPU clock is stopped when no FP instruction is being executed. To do so a dedicated clock gating cell is instantiated in ``cv32e40p_top`` top level module with its enable signal depending of both ``apu_req_o`` and ``apu_busy_o`` core outputs. + Reminder for programmers ------------------------ From 35acdef6008d6253b430e168b1e1301ac9c2d948 Mon Sep 17 00:00:00 2001 From: Pascal Gouedo Date: Wed, 3 Jul 2024 18:17:51 +0200 Subject: [PATCH 25/29] Added ASIC size numbers for different configurations. Signed-off-by: Pascal Gouedo --- docs/source/integration.rst | 56 ++++++++++++++++++++++++++++++++----- 1 file changed, 49 insertions(+), 7 deletions(-) diff --git a/docs/source/integration.rst b/docs/source/integration.rst index f98e29fcd..420d0e47d 100644 --- a/docs/source/integration.rst +++ b/docs/source/integration.rst @@ -248,13 +248,55 @@ The ``constraints/cv32e40p_core.sdc`` file provides an example of synthesis cons ASIC Synthesis ^^^^^^^^^^^^^^ -ASIC synthesis is supported for CV32E40P. The whole design is completely -synchronous and uses positive-edge triggered flip-flops. The -core occupies an area of about XX kGE. -With the FPU, the area increases to about XX kGE (XX kGE -FPU, XX kGE additional register file). A technology specific implementation -of a clock gating cell as described in :ref:`clock-gating-cell` needs to -be provided. +ASIC synthesis is supported for CV32E40P. The whole design is completely synchronous and uses positive-edge triggered flip-flops. + +To give some size numbers, it has been synthetized at 100 MHz with a 32 KB memory connected on each of its OBI interface, DFT scan chains have been implemented and it went down to full back-end implementation with Clock Tree synthesis. +But no memory bist are inserted and there are no scan compression for DFT. + +And a technology specific implementation of a clock gating cell as described in :ref:`clock-gating-cell` has been provided. + +Following table gives CV32E40P size in Kilo-Gates numbers using a 2-input NAND gate with X1 drive for different top parameters settings (COREV_CLUSTER = 0 for all cases). + +.. table:: CV32E40P size + :name: CV32E40P size + :widths: 45 45 10 + :class: no-scrollbar-table + + +-----------------------+--------------------+--------+ + | **Configuration** | **Top Parameters** | **KG** | + +=======================+====================+========+ + | V1 | COREV_PULP = 0 | 40 | + | | | | + | | FPU = 0 | | + | | | | + | | ZFINX = 0 | | + +-----------------------+--------------------+--------+ + | V2 PULP | COREV_PULP = 1 | 57 | + | | | | + | | FPU = 0 | | + | | | | + | | ZFINX = 0 | | + +-----------------------+--------------------+--------+ + | V2 PULP & FPU | COREV_PULP = 1 | 93 | + | | | | + | | FPU = 1 | | + | | | | + | | ZFINX = 0 | | + | | | | + | | FPU_ADDMUL_LAT = 0 | | + | | | | + | | FPU_OTHERS_LAT = 0 | | + +-----------------------+--------------------+--------+ + | V2 PULP & FPU & ZFINX | COREV_PULP = 1 | 77 | + | | | | + | | FPU = 1 | | + | | | | + | | ZFINX = 1 | | + | | | | + | | FPU_ADDMUL_LAT = 0 | | + | | | | + | | FPU_OTHERS_LAT = 0 | | + +-----------------------+--------------------+--------+ FPGA Synthesis ^^^^^^^^^^^^^^^ From 8ca252271fcbfad6481f2b802ae63b4f0d0f5a7d Mon Sep 17 00:00:00 2001 From: Pascal Gouedo Date: Wed, 3 Jul 2024 18:18:15 +0200 Subject: [PATCH 26/29] User Manual Verification section final version. Signed-off-by: Pascal Gouedo --- docs/source/verification.rst | 88 ++++++++++++++++++++---------------- 1 file changed, 49 insertions(+), 39 deletions(-) diff --git a/docs/source/verification.rst b/docs/source/verification.rst index 3b0de4bd8..944c00105 100644 --- a/docs/source/verification.rst +++ b/docs/source/verification.rst @@ -108,14 +108,13 @@ Additional details are available as part of the `CV32E40P v1.0.0 Report `_. -Summary and all reports links (RTL code, functional, tests) can be found here: `CV32E40P v2.0.0 Summary and Reports `_. +CV32E40Pv2 achieved RTL Freeze (released with cv32e40p_v1.8.3 version) end of June 2024, meaning that is has been fully verified as per its +`Simulation Verification Plan `_ and `RISC-V ISA Formal Verification Plan `_. +Summary and all reports links (RTL code, functional, tests) can be found here: `CV32E40P v1.8.3 Verification Summary and Reports `_. + +It is to be mentioned that CV32E40Pv2 has successfully executed `RISCOF (RISC-V COmpatibility Framework) `_ for RV32IMCF extensions. +The official RISCOF reports can be found `here `_. -It is to be mentioned that CV32E40Pv2 has successfully executed `RISCOF (RISC-V COmpatibility Framework) `_ for RV32IMCF extensions . -The official RISCOF reports can be found following the link mentioned above. +All issues (User Manual or RTL) mentioned below can be found at `CV32E40Pv2 Design Issues Summary `_. RISC-V ISA Formal verification ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -To accelerate the verification of more than 300 XPULP instructions, RISC-V ISA Formal Verification methodology has been used with Siemens EDA Onespin tool and its RISC-V ISA Processor Verification app. +To accelerate the verification of more than 300 XPULP instructions, RISC-V ISA Formal Verification methodology has been used with Siemens Questa Processor tool and its RISC-V ISA Processor Verification app. The XPULP instructions pseudo-code description using Sail language have been added to the RISC-V ISA app to successfully formally verify all the CV32E40P instructions, including the previously verified standard IMC together with the new F, Zfinx and XPULP extensions and all additional custom CSRs. @@ -174,33 +175,35 @@ Example: EXTZ(mul(X(rs1)[31..24],X(rs2)[31..24]))" }, -Those SAIL instructions description are then used to automatically generate 277 assertions and 29 CSRs descriptions. -Those assertions have been applied on the 7 different configurations listed in :ref:`Verified configurations` table on intermediate RTL version and were proven as correct. +Those SAIL instructions description are then used to automatically generate assertions and CSRs descriptions that are grouped by classes. Additionally to those instructions and CSR assertions there are some of them to check specific features (e.g. OBI interfaces protocol, legal CSRs reset values..). +So globally it is resulting in 198 assertions to be checked on the 7 different configurations listed in :ref:`Verified configurations` table. + +RTL code coverage is generated using Siemens Questa Processor Quantify tool which uses RTL mutation to check assertions quality and can produce standard UCDB database that can be merged with simulation ones afterwards. -RTL code coverage is generated using Siemens EDA Onespin Quantify tool which uses RTL mutation to check assertions quality and can produce standard UCDB database that can be merged with simulation one afterwards. +A document explaining the RISC-V ISA Formal Verication methodology using Siemens Questa Processor tool can be found `here `_. Simulation verification ^^^^^^^^^^^^^^^^^^^^^^^ core-v-verif verification environment for v1.0.0 was using a *step&compare* methodology with an instruction set simulator (ISS) from Imperas Software as the reference model. This strategy was successful, but inefficient because the *step&compare* logic in the testbench must compensate for the cycle-time effects of events that are asynchronous to the instruction stream such as interrupts, debug resets plus bus errors and random delays on instruction fetch and load/store memory buses. -For verification of v2.0.0 release of the CV32E40P core, the step-and-compare and the ISS have been replaced by a true reference model (RM) called ImperasDV. In addition, the Imperas Reference Model has been extended to support the v2 XPULP instructions specification. +For verification of v1.8.3 release of the CV32E40P core, the step-and-compare and the ISS have been replaced by a true reference model (RM) called ImperasDV. In addition, the Imperas Reference Model has been extended to support the v2 XPULP instructions specification. -Another innovation for v2.0.0 was the adoption of a standardized tracer interface to the DUT and RM, based on the open-source RISC-V Verification Interface (RVVI). The use of well documented, standardized interfaces greatly simplifies the integration of the DUT with the RM. +Another innovation for v1.8.3 was the adoption of a standardized interface to the DUT and RM, based on the open-source RISC-V Verification Interface (RVVI). The use of well documented, standardized interfaces greatly simplifies the integration of the DUT with the RM. Results summary ^^^^^^^^^^^^^^^ RISC-V ISA Formal Verification has been successfully launched on intermediate RTL versions of the 7 different configurations. -But on v1.8.0 RTL tag, only PULP configuration (CFG_P) was fully proven, run-time of more than a month on configurations including the Floating-Point unit prevented to have full results. -Properties status can be found in `CV32E40P v2.0.0 Report `_. +On v1.8.3 RTL tag, only PULP (CFG_P) and PULP with FPU (CFG_P_F0) configurations were fully proven, nearly all properties being unbounded hold, some being bounded hold with a high number of cycles. +Properties status can be found in `CV32E40P v1.8.3 Report `_. 30 issues were identified by Formal Verification, 20 by Simulation methodologies and 4 by Lint/RTL code review, all have been resolved except 1 about Lint warnings. Here is the breakdown of all the issues: -.. table:: How Issues Were Found in v2.0.0 - :name: How Issues Were Found in v2.0.0 +.. table:: How Issues Were Found in v1.8.3 + :name: How Issues Were Found in v1.8.3 :widths: 27 9 64 :class: no-scrollbar-table @@ -216,8 +219,8 @@ Here is the breakdown of all the issues: A classification of the RISC-V ISA Formal Verification issues by type and their description are listed in the following tables: -.. table:: Breakdown of Issues found by RISC-V ISA Formal Verification in v2.0.0 - :name: Breakdown of Issues found by RISC-V ISA Formal Verification in v2.0.0 +.. table:: Breakdown of Issues found by RISC-V ISA Formal Verification in v1.8.3 + :name: Breakdown of Issues found by RISC-V ISA Formal Verification in v1.8.3 :widths: 27 9 64 :class: no-scrollbar-table @@ -229,8 +232,8 @@ A classification of the RISC-V ISA Formal Verification issues by type and their | RTL bugs | 18 | Details below | +------------------------------+-----------+----------------------------------------------------------------------------------------+ -.. table:: RISC-V ISA Formal Verification Issues Classification in v2.0.0 - :name: RISC-V ISA Formal Verification Issues Classification in v2.0.0 +.. table:: RISC-V ISA Formal Verification Issues Classification in v1.8.3 + :name: RISC-V ISA Formal Verification Issues Classification in v1.8.3 :widths: 27 9 64 :class: no-scrollbar-table @@ -240,9 +243,9 @@ A classification of the RISC-V ISA Formal Verification issues by type and their | Illegal instructions exception | 5 | F and XPULP instructions corner cases or CSR accesses not flagged as Illegal | | | | instructions exception. | +--------------------------------+-----------+---------------------------------------------------------------------------------------+ - | Multi-cycle F instructions | 8 | FDIV, FSQRT or respective F instructions (when FPU_ADDMUL_LAT or FPU_OTHERS_LAT = 2) | - | | | are executed in the background and the pipeline can continue to execute other | - | | | instructions as long as there is no Read-After-Write or Write-After-Write dependency. | + | Multi-cycle F instructions | 8 | FDIV, FSQRT or all F instructions when FPU_ADDMUL_LAT/FPU_OTHERS_LAT = 2 are executed | + | | | in the background and the pipeline can continue to execute other instructions | + | | | as long as there is no Read-After-Write or Write-After-Write dependency. | | | | When the multi-cycle F instructions are finally writing back their result in the | | | | Register File, this register update can corrupt on-going instructions behaviour or | | | | result. This is the case for Misaligned Loads, Post-Incremented Load/Stores, MULH, | @@ -253,8 +256,8 @@ A classification of the RISC-V ISA Formal Verification issues by type and their A classification of the Simulation issues by type and their description are listed in the following tables: -.. table:: Breakdown of Issues found by Simulation in v2.0.0 - :name: Breakdown of Issues found by Simulation in v2.0.0 +.. table:: Breakdown of Issues found by Simulation in v1.8.3 + :name: Breakdown of Issues found by Simulation in v1.8.3 :widths: 27 9 64 :class: no-scrollbar-table @@ -264,15 +267,15 @@ A classification of the Simulation issues by type and their description are list | RTL bugs | 20 | See classification below | +------------------------------+-----------+----------------------------------------------------------------------------------------+ -.. table:: Simulation Issues Classification in v2.0.0 - :name: Simulation Issues Classification in v2.0.0 +.. table:: Simulation Issues Classification in v1.8.3 + :name: Simulation Issues Classification in v1.8.3 :widths: 38 9 53 :class: no-scrollbar-table +------------------------------------------+-----------+---------------------------------------------------------------------------------------+ | **Issue Type** | **Count** | **Note** | +==========================================+===========+=======================================================================================+ - | Multi-cycle F instructions | 5 | Data forward violation between XPULP instructions and muticycle F instructions. | + | Multi-cycle F instructions | 5 | Data forward violation between muticycle F instructions and XPULP instructions. | +------------------------------------------+-----------+---------------------------------------------------------------------------------------+ | Hardware Loops | 4 | Conflict between CSR write and cv.lp* instructions. | | | | | @@ -284,12 +287,12 @@ A classification of the Simulation issues by type and their description are list +------------------------------------------+-----------+---------------------------------------------------------------------------------------+ | Illegal instructions exception | 3 | Illegal immediates values | +------------------------------------------+-----------+---------------------------------------------------------------------------------------+ - | Incorrect Register file control | 1 | ZFINX = 1 case | + | Incorrect Register file control | 1 | When ZFINX = 1 | +------------------------------------------+-----------+---------------------------------------------------------------------------------------+ | MIMPID incorrect value | 1 | Value depending of FPU, COREV_PULP and COREV_CLUSTER paremeters. | +------------------------------------------+-----------+---------------------------------------------------------------------------------------+ | Deadlock | 1 | Bug resolution for multicycle F instructions created a deadlock when conflicting | - | | | Register File write between ALU and FPU. | + | | | Register File write between FPU and ALU. | +------------------------------------------+-----------+---------------------------------------------------------------------------------------+ | MSTATUS.FS incorrect value | 1 | FS was not updated following any Floating Point Load instruction. | +------------------------------------------+-----------+---------------------------------------------------------------------------------------+ @@ -323,20 +326,27 @@ The trace output is in tab-separated columns. 3. **PC**: The program counter 4. **Instr**: The executed instruction (base 16). 32 bit wide instructions (8 hex digits) are uncompressed instructions, 16 bit wide instructions (4 hex digits) are compressed instructions. -5. **Decoded instruction**: The decoded (disassembled) instruction in a format equal to what objdump produces when calling it like ``objdump -Mnumeric -Mno-aliases -D``. +5. **Ctx**: When an illegal instruction is cancelled, this field shows (C) information together with the instruction which caused cancellation. +6. **Decoded instruction**: The decoded (disassembled) instruction in a format equal to what objdump produces when calling it like ``objdump -Mnumeric -Mno-aliases -D``. - Unsigned numbers are given in hex (prefixed with ``0x``), signed numbers are given as decimal numbers. - Numeric register names are used (e.g. ``x1``). - Symbolic CSR names are used. - Jump/branch targets are given as absolute address if possible (PC + immediate). -6. **Register and memory contents**: For all accessed registers, the value before and after the instruction execution is given. Writes to registers are indicated as ``registername=value``, reads as ``registername:value``. For memory accesses, the physical address (PA) of the loaded or stored data is reported as well. +7. **Register and memory contents**: For all accessed registers, the value before and after the instruction execution is given. Writes to registers are indicated as ``registername=value``, reads as ``registername:value``. For memory accesses, the physical address (PA) of the loaded or stored data is reported as well. +8. **Stop cycle Stop time**: For long multi-cycle instructions like Floating-Point Division or Square-root, these columns are indicating when the result and the flags are returned by the FPU. .. code-block:: text - Time Cycle PC Instr Decoded instruction Register and memory contents - 130 61 00000150 4481 c.li x9,0 x9=0x00000000 - 132 62 00000152 00008437 lui x8,0x8 x8=0x00008000 - 134 63 00000156 fff40413 addi x8,x8,-1 x8=0x00007fff x8:0x00008000 - 136 64 0000015a 8c65 c.and x8,x9 x8=0x00000000 x8:0x00007fff x9:0x00000000 - 142 67 0000015c c622 c.swsp x8,12(x2) x2:0x00002000 x8:0x00000000 PA:0x0000200c + Time Cycle PC Instr Ctx Decoded instruction Register and memory contents Stop cycle Stop time + 130.000 ns 61 00000150 4481 c.li x9,0 x9=0x00000000 + 132.000 ns 62 00000152 00008437 lui x8,0x8 x8=0x00008000 + 134.000 ns 63 00000156 fff40413 addi x8,x8,-1 x8=0x00007fff x8:0x00008000 + 136.000 ns 64 0000015a 18e50353 fdiv.s f6, f10, f14 f6=59463c68 f10:990dcef4 f14:8016e429 67 142.000 ns + 138.000 ns 65 0000015c 8c65 c.and x8,x9 x8=0x00000000 x8:0x00007fff x9:0x00000000 + 142.000 ns 67 0000015e c622 c.swsp x8,12(x2) x2:0x00002000 x8:0x00000000 PA:0x0000200c + 144.000 ns 68 00000160 36067a73 (C) csrrci x0, 0x00000000, 0x360 + 152.000 ns 72 00033200 0800006f jal x0, 128 + + From 4e7b2ec81fbbac066843d33141133c3307e43e09 Mon Sep 17 00:00:00 2001 From: Pascal Gouedo Date: Wed, 3 Jul 2024 18:18:35 +0200 Subject: [PATCH 27/29] Changed User Manual version to v1.8.3 Signed-off-by: Pascal Gouedo --- docs/source/conf.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/source/conf.py b/docs/source/conf.py index 3e24854b3..f9df04545 100644 --- a/docs/source/conf.py +++ b/docs/source/conf.py @@ -44,7 +44,7 @@ # The short X.Y version version = u'' # The full version, including alpha/beta/rc tags -release = u'v1.8.0' +release = u'v1.8.3' # -- General configuration --------------------------------------------------- From c0823cf2bea6c60f84a08599dfb207c3db237fad Mon Sep 17 00:00:00 2001 From: Pascal Gouedo Date: Thu, 11 Jul 2024 10:21:16 +0200 Subject: [PATCH 28/29] All links updated to cv32e40p_v1.8.3 tag for the 3 target repos (core-v-docs, cv32e40p, core-v-verif). Signed-off-by: Pascal Gouedo --- docs/source/verification.rst | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/docs/source/verification.rst b/docs/source/verification.rst index 944c00105..34b33b09e 100644 --- a/docs/source/verification.rst +++ b/docs/source/verification.rst @@ -30,7 +30,7 @@ v1.0.0 verification In early 2021 the CV32E40P achieved Functional RTL Freeze (released with cv32e40p_v1.0.0 version), meaning that is has been fully verified as per its `Verification Plan `_. -Final functional, code and test coverage reports can be found `here `_. +Final functional, code and test coverage reports can be found `here `_. The unofficial start date for the CV32E40P verification effort is 2020-02-27, which is the date the core-v-verif environment "went live". Between then and @@ -97,7 +97,7 @@ A classification of the issues themselves: | Invalid | 1 | | +------------------------------+-----------+----------------------------------------------------------------------------------------+ -Additional details are available as part of the `CV32E40P v1.0.0 Report `_. +Additional details are available as part of the `CV32E40P v1.0.0 Report `_. .. [1] It is a testament on the quality of the work done by the PULP platform team @@ -145,13 +145,13 @@ Verification environment is described in `CORE-V Verification Strategy `_ and `RISC-V ISA Formal Verification Plan `_. -Summary and all reports links (RTL code, functional, tests) can be found here: `CV32E40P v1.8.3 Verification Summary and Reports `_. +`Simulation Verification Plan `_ and `RISC-V ISA Formal Verification Plan `_. +Summary and all reports links (RTL code, functional, tests) can be found here: `CV32E40P v1.8.3 Verification Summary and Reports `_. It is to be mentioned that CV32E40Pv2 has successfully executed `RISCOF (RISC-V COmpatibility Framework) `_ for RV32IMCF extensions. -The official RISCOF reports can be found `here `_. +The official RISCOF reports can be found `here `_. -All issues (User Manual or RTL) mentioned below can be found at `CV32E40Pv2 Design Issues Summary `_. +All issues (User Manual or RTL) mentioned below can be found at `CV32E40Pv2 Design Issues Summary `_. RISC-V ISA Formal verification ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ @@ -180,7 +180,7 @@ So globally it is resulting in 198 assertions to be checked on the 7 different c RTL code coverage is generated using Siemens Questa Processor Quantify tool which uses RTL mutation to check assertions quality and can produce standard UCDB database that can be merged with simulation ones afterwards. -A document explaining the RISC-V ISA Formal Verication methodology using Siemens Questa Processor tool can be found `here `_. +A document explaining the RISC-V ISA Formal Verication methodology using Siemens Questa Processor tool can be found `here `_. Simulation verification ^^^^^^^^^^^^^^^^^^^^^^^ @@ -196,7 +196,7 @@ Results summary RISC-V ISA Formal Verification has been successfully launched on intermediate RTL versions of the 7 different configurations. On v1.8.3 RTL tag, only PULP (CFG_P) and PULP with FPU (CFG_P_F0) configurations were fully proven, nearly all properties being unbounded hold, some being bounded hold with a high number of cycles. -Properties status can be found in `CV32E40P v1.8.3 Report `_. +Properties status can be found in `CV32E40P v1.8.3 Report `_. 30 issues were identified by Formal Verification, 20 by Simulation methodologies and 4 by Lint/RTL code review, all have been resolved except 1 about Lint warnings. From 43e6af1d0b7260c4935b0c6cfff6c3c947d09f3c Mon Sep 17 00:00:00 2001 From: Pascal Gouedo Date: Thu, 11 Jul 2024 14:41:26 +0200 Subject: [PATCH 29/29] core-v-docs changed to programs Signed-off-by: Pascal Gouedo --- docs/source/verification.rst | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/docs/source/verification.rst b/docs/source/verification.rst index 34b33b09e..ceed0b5f3 100644 --- a/docs/source/verification.rst +++ b/docs/source/verification.rst @@ -30,7 +30,7 @@ v1.0.0 verification In early 2021 the CV32E40P achieved Functional RTL Freeze (released with cv32e40p_v1.0.0 version), meaning that is has been fully verified as per its `Verification Plan `_. -Final functional, code and test coverage reports can be found `here `_. +Final functional, code and test coverage reports can be found `here `_. The unofficial start date for the CV32E40P verification effort is 2020-02-27, which is the date the core-v-verif environment "went live". Between then and @@ -97,7 +97,7 @@ A classification of the issues themselves: | Invalid | 1 | | +------------------------------+-----------+----------------------------------------------------------------------------------------+ -Additional details are available as part of the `CV32E40P v1.0.0 Report `_. +Additional details are available as part of the `CV32E40P v1.0.0 Report `_. .. [1] It is a testament on the quality of the work done by the PULP platform team @@ -146,12 +146,12 @@ Verification environment is described in `CORE-V Verification Strategy `_ and `RISC-V ISA Formal Verification Plan `_. -Summary and all reports links (RTL code, functional, tests) can be found here: `CV32E40P v1.8.3 Verification Summary and Reports `_. +Summary and all reports links (RTL code, functional, tests) can be found here: `CV32E40P v1.8.3 Verification Summary and Reports `_. It is to be mentioned that CV32E40Pv2 has successfully executed `RISCOF (RISC-V COmpatibility Framework) `_ for RV32IMCF extensions. -The official RISCOF reports can be found `here `_. +The official RISCOF reports can be found `here `_. -All issues (User Manual or RTL) mentioned below can be found at `CV32E40Pv2 Design Issues Summary `_. +All issues (User Manual or RTL) mentioned below can be found at `CV32E40Pv2 Design Issues Summary `_. RISC-V ISA Formal verification ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ @@ -196,7 +196,7 @@ Results summary RISC-V ISA Formal Verification has been successfully launched on intermediate RTL versions of the 7 different configurations. On v1.8.3 RTL tag, only PULP (CFG_P) and PULP with FPU (CFG_P_F0) configurations were fully proven, nearly all properties being unbounded hold, some being bounded hold with a high number of cycles. -Properties status can be found in `CV32E40P v1.8.3 Report `_. +Properties status can be found in `CV32E40P v1.8.3 Report `_. 30 issues were identified by Formal Verification, 20 by Simulation methodologies and 4 by Lint/RTL code review, all have been resolved except 1 about Lint warnings.