From 2c48945b869762e9570ba4815342562a0bd87057 Mon Sep 17 00:00:00 2001 From: Ayoub Jalali Date: Fri, 3 Feb 2023 11:32:51 +0100 Subject: [PATCH] CVXIF: Verification plans Signed-off-by: Ayoub Jalali --- cva6/docs/VerifPlans/CVXIF/VP_IP000.pck | 998 ++++++++++++++++++++ cva6/docs/VerifPlans/CVXIF/VP_IP001.pck | 418 ++++++++ cva6/docs/VerifPlans/CVXIF/VP_IP002.pck | 860 +++++++++++++++++ cva6/docs/VerifPlans/CVXIF/runme.sh | 34 + cva6/docs/VerifPlans/source/dvplan_CVXIF.md | 556 +++++++++++ cva6/docs/VerifPlans/source/index.rst | 1 + 6 files changed, 2867 insertions(+) create mode 100644 cva6/docs/VerifPlans/CVXIF/VP_IP000.pck create mode 100644 cva6/docs/VerifPlans/CVXIF/VP_IP001.pck create mode 100644 cva6/docs/VerifPlans/CVXIF/VP_IP002.pck create mode 100644 cva6/docs/VerifPlans/CVXIF/runme.sh create mode 100644 cva6/docs/VerifPlans/source/dvplan_CVXIF.md diff --git a/cva6/docs/VerifPlans/CVXIF/VP_IP000.pck b/cva6/docs/VerifPlans/CVXIF/VP_IP000.pck new file mode 100644 index 0000000000..575c69110d --- /dev/null +++ b/cva6/docs/VerifPlans/CVXIF/VP_IP000.pck @@ -0,0 +1,998 @@ +(VIssue Interface +p0 +ccopy_reg +_reconstructor +p1 +(cvp_pack +Ip +p2 +c__builtin__ +object +p3 +Ntp4 +Rp5 +(dp6 +Vprop_count +p7 +I9 +sVname +p8 +g0 +sVprop_list +p9 +(dp10 +sVip_num +p11 +I0 +sVwid_order +p12 +I0 +sVrfu_dict +p13 +(dp14 +sVrfu_list +p15 +(lp16 +(V000_issue_req signals stable +p17 +g1 +(cvp_pack +Prop +p18 +g3 +Ntp19 +Rp20 +(dp21 +Vitem_count +p22 +I1 +sg8 +g17 +sVtag +p23 +VVP_CVXIF_F000_S000 +p24 +sVitem_list +p25 +(dp26 +sg12 +I0 +sg15 +(lp27 +(V000 +p28 +g1 +(cvp_pack +Item +p29 +g3 +Ntp30 +Rp31 +(dp32 +g8 +V000 +p33 +sg23 +VVP_CVXIF_F000_S000_I000 +p34 +sVdescription +p35 +VThe \u201cinstr\u201d and \u201cmode\u201d signals remain stable during an Issue request transaction. +p36 +sVpurpose +p37 +V +p38 +sVverif_goals +p39 +VCheck that \u201cmode\u201d and \u201cinstr\u201d are stable during an issue transaction (cannot be modified by an instruction when transaction issue is in process) +p40 +sVcoverage_loc +p41 +g38 +sVref_mode +p42 +Vpage +p43 +sVref_page +p44 +g38 +sVref_section +p45 +g38 +sVref_viewer +p46 +Vfirefox +p47 +sVpfc +p48 +I4 +sVtest_type +p49 +I3 +sVcov_method +p50 +I2 +sVcores +p51 +I56 +sVcomments +p52 +g38 +sVstatus +p53 +g38 +sVsimu_target_list +p54 +(lp55 +sg15 +(lp56 +sVrfu_list_2 +p57 +(lp58 +sg13 +(dp59 +Vlock_status +p60 +I0 +ssbtp61 +asVrfu_list_1 +p62 +(lp63 +sg57 +(lp64 +sg13 +(dp65 +sbtp66 +a(V001_mode signal value +p67 +g1 +(g18 +g3 +Ntp68 +Rp69 +(dp70 +g22 +I2 +sg8 +g67 +sg23 +VVP_CVXIF_F000_S001 +p71 +sg25 +(dp72 +sg12 +I1 +sg15 +(lp73 +(V000 +p74 +g1 +(g29 +g3 +Ntp75 +Rp76 +(dp77 +g8 +V000 +p78 +sg23 +VVP_CVXIF_F000_S001_I000 +p79 +sg35 +VWhen issue transaction starts, instruction and current CPU mode are provided +p80 +sg37 +g38 +sg39 +VCheck that a mode modification coming from execution of a first instruction is well provided to the following offloaded instruction +p81 +sg41 +g38 +sg42 +g43 +sg44 +g38 +sg45 +g38 +sg46 +g47 +sg48 +I3 +sg49 +I3 +sg50 +I1 +sg51 +I56 +sg52 +g38 +sg53 +g38 +sg54 +(lp82 +sg15 +(lp83 +sg57 +(lp84 +sg13 +(dp85 +g60 +I0 +ssbtp86 +a(V001 +p87 +g1 +(g29 +g3 +Ntp88 +Rp89 +(dp90 +g8 +V001 +p91 +sg23 +VVP_CVXIF_F000_S001_I001 +p92 +sg35 +VCheck \u201cmode\u201d signal values. +p93 +sg37 +g38 +sg39 +VCheck that mode take a value that the CPU supports : Privilege level (2\u2019b00 = User, 2\u2019b01 = Supervisor, 2\u2019b10 = Reserved,\u000a 2\u2019b11 = Machine). +p94 +sg41 +g38 +sg42 +g43 +sg44 +g38 +sg45 +g38 +sg46 +g47 +sg48 +I-1 +sg49 +I-1 +sg50 +I-1 +sg51 +I56 +sg52 +g38 +sg53 +g38 +sg54 +(lp95 +sg15 +(lp96 +sg57 +(lp97 +sg13 +(dp98 +g60 +I0 +ssbtp99 +asg62 +(lp100 +sg57 +(lp101 +sg13 +(dp102 +sbtp103 +a(V002_rs_valid signal transition order +p104 +g1 +(g18 +g3 +Ntp105 +Rp106 +(dp107 +g22 +I1 +sg8 +g104 +sg23 +VVP_CVXIF_F000_S002 +p108 +sg25 +(dp109 +sg12 +I2 +sg15 +(lp110 +(V000 +p111 +g1 +(g29 +g3 +Ntp112 +Rp113 +(dp114 +g8 +V000 +p115 +sg23 +VVP_CVXIF_F000_S002_I000 +p116 +sg35 +VDuring a transaction, each bit of \u201crs_valid\u201d can transition from 0 to 1 but are not allowed to transition back to 0. +p117 +sg37 +g38 +sg39 +VFor issue transaction which lasts more than one cycle, check that asserted \u201crs_valid\u201d signals do not transition back to 0.(for i in [0;2] if rs_valid[i] = 1 then rs_valid[i] \u2192 0 cannot happen) +p118 +sg41 +g38 +sg42 +g43 +sg44 +g38 +sg45 +g38 +sg46 +g47 +sg48 +I4 +sg49 +I3 +sg50 +I2 +sg51 +I56 +sg52 +g38 +sg53 +g38 +sg54 +(lp119 +sg15 +(lp120 +sg57 +(lp121 +sg13 +(dp122 +g60 +I0 +ssbtp123 +asg62 +(lp124 +sg57 +(lp125 +sg13 +(dp126 +sbtp127 +a(V003_rs signal value +p128 +g1 +(g18 +g3 +Ntp129 +Rp130 +(dp131 +g22 +I3 +sg8 +g128 +sg23 +VVP_CVXIF_F000_S003 +p132 +sg25 +(dp133 +sg12 +I3 +sg15 +(lp134 +(V000 +p135 +g1 +(g29 +g3 +Ntp136 +Rp137 +(dp138 +g8 +V000 +p139 +sg23 +VVP_CVXIF_F000_S003_I000 +p140 +sg35 +VIf XLEN = X_RFR_WIDTH, then rs[X_NUM_RS-1:0] correspond to rs1 and rs2 CPU registers (and rs3 if X_NUM_RS = 3). +p141 +sg37 +g38 +sg39 +VFor every issue transaction check that rs signal correspond to rs1,rs2(rs3) value in CPU register file. +p142 +sg41 +g38 +sg42 +g43 +sg44 +g38 +sg45 +g38 +sg46 +g47 +sg48 +I3 +sg49 +I3 +sg50 +I1 +sg51 +I56 +sg52 +g38 +sg53 +g38 +sg54 +(lp143 +sg15 +(lp144 +sg57 +(lp145 +sg13 +(dp146 +g60 +I0 +ssbtp147 +a(V001 +p148 +g1 +(g29 +g3 +Ntp149 +Rp150 +(dp151 +g8 +V001 +p152 +sg23 +VVP_CVXIF_F000_S003_I001 +p153 +sg35 +Vrs signals are only required to be stable during the part of a transaction in which these signals are considered to be valid. +p154 +sg37 +g38 +sg39 +VCheck that rs signals are stable when issue_valid==1 && the corresponding bit in rs_valid is 1. +p155 +sg41 +g38 +sg42 +g43 +sg44 +g38 +sg45 +g38 +sg46 +g47 +sg48 +I4 +sg49 +I-1 +sg50 +I2 +sg51 +I56 +sg52 +g38 +sg53 +g38 +sg54 +(lp156 +sg15 +(lp157 +sg57 +(lp158 +sg13 +(dp159 +g60 +I0 +ssbtp160 +a(V002 +p161 +g1 +(g29 +g3 +Ntp162 +Rp163 +(dp164 +g8 +V002 +p165 +sg23 +VVP_CVXIF_F000_S003_I002 +p166 +sg35 +VIf XLEN != X_RFR_WIDTH , then rs[X_NUM_RS-1:0] correspond to even/odd register pair with rs1, rs2, (rs3) are even register and even register is provided in the 32 lower bits of rs signal. +p167 +sg37 +g38 +sg39 +VFor every issue transaction check that rs signal correspond to the concatenation of rs1/rs1+1,rs2/rs2+1, (rs3/rs3+1) value in CPU register file and even register is in the 32 lower bits of rs. +p168 +sg41 +g38 +sg42 +g43 +sg44 +g38 +sg45 +g38 +sg46 +g47 +sg48 +I-1 +sg49 +I-1 +sg50 +I-1 +sg51 +I56 +sg52 +g38 +sg53 +g38 +sg54 +(lp169 +sg15 +(lp170 +sg57 +(lp171 +sg13 +(dp172 +g60 +I0 +ssbtp173 +asg62 +(lp174 +sg57 +(lp175 +sg13 +(dp176 +sbtp177 +a(V004_Default value for unaccepted instruction +p178 +g1 +(g18 +g3 +Ntp179 +Rp180 +(dp181 +g22 +I1 +sg8 +g178 +sg23 +VVP_CVXIF_F000_S004 +p182 +sg25 +(dp183 +sg12 +I4 +sg15 +(lp184 +(V000 +p185 +g1 +(g29 +g3 +Ntp186 +Rp187 +(dp188 +g8 +V000 +p189 +sg23 +VVP_CVXIF_F000_S004_I000 +p190 +sg35 +VIf accept == 0 :\u000aWriteback == 0; dualwrite == 0; dualread == 0; loadstore == 0; exc = 0. +p191 +sg37 +g38 +sg39 +VCheck that for writeback; dualwrite; dualread; loadstore; exc signals if accept == 0 then all those signals are 0. +p192 +sg41 +g38 +sg42 +g43 +sg44 +g38 +sg45 +g38 +sg46 +g47 +sg48 +I4 +sg49 +I3 +sg50 +I2 +sg51 +I56 +sg52 +g38 +sg53 +g38 +sg54 +(lp193 +sg15 +(lp194 +sg57 +(lp195 +sg13 +(dp196 +g60 +I0 +ssbtp197 +asg62 +(lp198 +sg57 +(lp199 +sg13 +(dp200 +sbtp201 +a(V005_Illegal Instruction causes +p202 +g1 +(g18 +g3 +Ntp203 +Rp204 +(dp205 +g22 +I1 +sg8 +g202 +sg23 +VVP_CVXIF_F000_S005 +p206 +sg25 +(dp207 +sg12 +I5 +sg15 +(lp208 +(V000 +p209 +g1 +(g29 +g3 +Ntp210 +Rp211 +(dp212 +g8 +V000 +p213 +sg23 +VVP_CVXIF_F000_S005_I000 +p214 +sg35 +VThe CPU shall cause an illegal instruction if:\u000a- an instruction is considered to be valid by the CPU and accepted by the coprocessor (accept = 1)\u000a- neither to be valid by the CPU nor accepted by the coprocessor (accept = 0) +p215 +sg37 +g38 +sg39 +V- CPU causes illegal instruction for instruction accepted by the core and the coprocessor.\u000a- CPU causes illegal instruction exception for instruction that are not valid for coprocessor and CPU +p216 +sg41 +g38 +sg42 +g43 +sg44 +g38 +sg45 +g38 +sg46 +g47 +sg48 +I3 +sg49 +I3 +sg50 +I1 +sg51 +I56 +sg52 +g38 +sg53 +g38 +sg54 +(lp217 +sg15 +(lp218 +sg57 +(lp219 +sg13 +(dp220 +g60 +I0 +ssbtp221 +asg62 +(lp222 +sg57 +(lp223 +sg13 +(dp224 +sbtp225 +a(V006_issue uniquness +p226 +g1 +(g18 +g3 +Ntp227 +Rp228 +(dp229 +g22 +I1 +sg8 +g226 +sg23 +VVP_CVXIF_F000_S006 +p230 +sg25 +(dp231 +sg12 +I6 +sg15 +(lp232 +(V000 +p233 +g1 +(g29 +g3 +Ntp234 +Rp235 +(dp236 +g8 +V000 +p237 +sg23 +VVP_CVXIF_F000_S006_I000 +p238 +sg35 +VCheck for issue id validity. +p239 +sg37 +g38 +sg39 +VCheck that the issue interface doesn't issue an "id" that isn't legal to be used (has not fully completed). +p240 +sg41 +g38 +sg42 +g43 +sg44 +g38 +sg45 +g38 +sg46 +g47 +sg48 +I11 +sg49 +I3 +sg50 +I10 +sg51 +I56 +sg52 +g38 +sg53 +g38 +sg54 +(lp241 +sg15 +(lp242 +sg57 +(lp243 +sg13 +(dp244 +g60 +I0 +ssbtp245 +asg62 +(lp246 +sg57 +(lp247 +sg13 +(dp248 +sbtp249 +a(V007_coprocessor decoding +p250 +g1 +(g18 +g3 +Ntp251 +Rp252 +(dp253 +g22 +I1 +sg8 +g250 +sg23 +VVP_CVXIF_F000_S007 +p254 +sg25 +(dp255 +sg12 +I7 +sg15 +(lp256 +(V000 +p257 +g1 +(g29 +g3 +Ntp258 +Rp259 +(dp260 +g8 +V000 +p261 +sg23 +VVP_CVXIF_F000_S007_I000 +p262 +sg35 +VAccept = 1 if: \u000a- coprocessor can handle the instruction based on decoding \u201cinstr\u201dand "mode".\u000a- \u201cissue_valid\u201d == 1 and required bit(s) of \u201crs_valid\u201d are 1. +p263 +sg37 +g38 +sg39 +VTo be checked in coprocessor. +p264 +sg41 +g38 +sg42 +g43 +sg44 +g38 +sg45 +g38 +sg46 +g47 +sg48 +I3 +sg49 +I3 +sg50 +I1 +sg51 +I56 +sg52 +g38 +sg53 +g38 +sg54 +(lp265 +sg15 +(lp266 +sg57 +(lp267 +sg13 +(dp268 +g60 +I0 +ssbtp269 +asg62 +(lp270 +sg57 +(lp271 +sg13 +(dp272 +sbtp273 +a(V008_Transaction definition +p274 +g1 +(g18 +g3 +Ntp275 +Rp276 +(dp277 +g22 +I1 +sg8 +g274 +sg23 +VVP_CVXIF_F000_S008 +p278 +sg25 +(dp279 +sg12 +I8 +sg15 +(lp280 +(V000 +p281 +g1 +(g29 +g3 +Ntp282 +Rp283 +(dp284 +g8 +V000 +p285 +sg23 +VVP_CVXIF_F000_S008_I000 +p286 +sg35 +V\u201cissue_resp\u201d signals and \u201cissue_req\u201d signals are accepted when \u201cissue_valid\u201d == \u201cissue_ready\u201d == 1\u000a\u201cissue_resp\u201d is valid when "valid==ready==1".\u000a\u201cissue_req\u201d is valid when "valid==1" +p287 +sg37 +g38 +sg39 +VThe definition of a transaction. \u000aNot to be verified. +p288 +sg41 +g38 +sg42 +g43 +sg44 +g38 +sg45 +g38 +sg46 +g47 +sg48 +I11 +sg49 +I10 +sg50 +I10 +sg51 +I56 +sg52 +g38 +sg53 +g38 +sg54 +(lp289 +sg15 +(lp290 +sg57 +(lp291 +sg13 +(dp292 +g60 +I0 +ssbtp293 +asg62 +(lp294 +sg57 +(lp295 +sg13 +(dp296 +sbtp297 +asVrfu_list_0 +p298 +(lp299 +sg62 +(lp300 +sVvptool_gitrev +p301 +V$Id: a782de3eec3de5ff99661fb165c09f541b4228d0 $ +p302 +sVio_fmt_gitrev +p303 +V$Id: 2f6f9e7bc800d8b831382463dc706473c6c6ad8c $ +p304 +sVconfig_gitrev +p305 +V$Id: 0422e19126dae20ffc4d5a84e4ce3de0b6eb4eb5 $ +p306 +sVymlcfg_gitrev +p307 +V$Id: 286c689bd48b7a58f9a37754267895cffef1270c $ +p308 +sbtp309 +. \ No newline at end of file diff --git a/cva6/docs/VerifPlans/CVXIF/VP_IP001.pck b/cva6/docs/VerifPlans/CVXIF/VP_IP001.pck new file mode 100644 index 0000000000..1a42a8fd32 --- /dev/null +++ b/cva6/docs/VerifPlans/CVXIF/VP_IP001.pck @@ -0,0 +1,418 @@ +(VCommit Interface +p0 +ccopy_reg +_reconstructor +p1 +(cvp_pack +Ip +p2 +c__builtin__ +object +p3 +Ntp4 +Rp5 +(dp6 +Vprop_count +p7 +I4 +sVname +p8 +g0 +sVprop_list +p9 +(dp10 +sVip_num +p11 +I1 +sVwid_order +p12 +I1 +sVrfu_dict +p13 +(dp14 +sVrfu_list +p15 +(lp16 +(V000_commit_valid pulse +p17 +g1 +(cvp_pack +Prop +p18 +g3 +Ntp19 +Rp20 +(dp21 +Vitem_count +p22 +I1 +sg8 +g17 +sVtag +p23 +VVP_CVXIF_F001_S000 +p24 +sVitem_list +p25 +(dp26 +sg12 +I0 +sg15 +(lp27 +(V000 +p28 +g1 +(cvp_pack +Item +p29 +g3 +Ntp30 +Rp31 +(dp32 +g8 +V000 +p33 +sg23 +VVP_CVXIF_F001_S000_I000 +p34 +sVdescription +p35 +VThe \u201ccommit_valid\u201d == 1 exactly one clk cycle for every offloaded Instruction by the coprocessor (whether accepted or not). +p36 +sVpurpose +p37 +V +p38 +sVverif_goals +p39 +VFor every offloaded instruction, check that commit_valid is asserted exactly one clk cycle ( is a pulse ). +p40 +sVcoverage_loc +p41 +g38 +sVref_mode +p42 +Vpage +p43 +sVref_page +p44 +g38 +sVref_section +p45 +g38 +sVref_viewer +p46 +Vfirefox +p47 +sVpfc +p48 +I4 +sVtest_type +p49 +I3 +sVcov_method +p50 +I2 +sVcores +p51 +I56 +sVcomments +p52 +g38 +sVstatus +p53 +g38 +sVsimu_target_list +p54 +(lp55 +sg15 +(lp56 +sVrfu_list_2 +p57 +(lp58 +sg13 +(dp59 +Vlock_status +p60 +I0 +ssbtp61 +asVrfu_list_1 +p62 +(lp63 +sg57 +(lp64 +sg13 +(dp65 +sbtp66 +a(V001_commit transaction uniquness +p67 +g1 +(g18 +g3 +Ntp68 +Rp69 +(dp70 +g22 +I1 +sg8 +g67 +sg23 +VVP_CVXIF_F001_S001 +p71 +sg25 +(dp72 +sg12 +I1 +sg15 +(lp73 +(V000 +p74 +g1 +(g29 +g3 +Ntp75 +Rp76 +(dp77 +g8 +V000 +p78 +sg23 +VVP_CVXIF_F001_S001_I000 +p79 +sg35 +VThere is a unique commit transaction for every issue transaction (unique until an instruction has "fully completed" = its result has been submitted). +p80 +sg37 +g38 +sg39 +VCheck that the commit interface doesn't commit an "id" that isn't legal to be used (hasn't been seen in earlier stages, or has not fully completed). +p81 +sg41 +g38 +sg42 +g43 +sg44 +g38 +sg45 +g38 +sg46 +g47 +sg48 +I1 +sg49 +I10 +sg50 +I10 +sg51 +I56 +sg52 +g38 +sg53 +g38 +sg54 +(lp82 +sg15 +(lp83 +sg57 +(lp84 +sg13 +(dp85 +g60 +I0 +ssbtp86 +asg62 +(lp87 +sg57 +(lp88 +sg13 +(dp89 +sbtp90 +a(V002_commit transaction for every issue transaction +p91 +g1 +(g18 +g3 +Ntp92 +Rp93 +(dp94 +g22 +I1 +sg8 +g91 +sg23 +VVP_CVXIF_F001_S002 +p95 +sg25 +(dp96 +sg12 +I2 +sg15 +(lp97 +(V000 +p98 +g1 +(g29 +g3 +Ntp99 +Rp100 +(dp101 +g8 +V000 +p102 +sg23 +VVP_CVXIF_F001_S002_I000 +p103 +sg35 +V- The CPU shall perform a commit transaction for every issue transaction, independent of the accept value of the issue transaction.\u000a- For each offloaded and accepted instruction the core is guaranteed to (eventually) signal that such an instruction is either no longer speculative and can be committed (commit_valid is 1 and commit_kill is 0) or that the instruction must be killed (commit_valid is 1 and commit_kill is 1). +p104 +sg37 +g38 +sg39 +VCheck that for each issue transaction, the commit transaction is sent at the same clock cycle than the issue transaction, or at any clock cycle after the issue transaction. +p105 +sg41 +g38 +sg42 +g43 +sg44 +g38 +sg45 +g38 +sg46 +g47 +sg48 +I4 +sg49 +I3 +sg50 +I2 +sg51 +I56 +sg52 +g38 +sg53 +g38 +sg54 +(lp106 +sg15 +(lp107 +sg57 +(lp108 +sg13 +(dp109 +g60 +I0 +ssbtp110 +asg62 +(lp111 +sg57 +(lp112 +sg13 +(dp113 +sbtp114 +a(V003_Transaction definition +p115 +g1 +(g18 +g3 +Ntp116 +Rp117 +(dp118 +g22 +I1 +sg8 +g115 +sg23 +VVP_CVXIF_F001_S003 +p119 +sg25 +(dp120 +sg12 +I3 +sg15 +(lp121 +(V000 +p122 +g1 +(g29 +g3 +Ntp123 +Rp124 +(dp125 +g8 +V000 +p126 +sg23 +VVP_CVXIF_F001_S003_I000 +p127 +sg35 +VThe signals in commit are valid when commit_valid is 1. +p128 +sg37 +g38 +sg39 +VThe definition of a transaction.\u000aNot to be verified. +p129 +sg41 +g38 +sg42 +g43 +sg44 +g38 +sg45 +g38 +sg46 +g47 +sg48 +I11 +sg49 +I-1 +sg50 +I10 +sg51 +I56 +sg52 +g38 +sg53 +g38 +sg54 +(lp130 +sg15 +(lp131 +sg57 +(lp132 +sg13 +(dp133 +g60 +I0 +ssbtp134 +asg62 +(lp135 +sg57 +(lp136 +sg13 +(dp137 +sbtp138 +asVrfu_list_0 +p139 +(lp140 +sg62 +(lp141 +sVvptool_gitrev +p142 +V$Id: a782de3eec3de5ff99661fb165c09f541b4228d0 $ +p143 +sVio_fmt_gitrev +p144 +V$Id: 2f6f9e7bc800d8b831382463dc706473c6c6ad8c $ +p145 +sVconfig_gitrev +p146 +V$Id: 0422e19126dae20ffc4d5a84e4ce3de0b6eb4eb5 $ +p147 +sVymlcfg_gitrev +p148 +V$Id: 286c689bd48b7a58f9a37754267895cffef1270c $ +p149 +sbtp150 +. \ No newline at end of file diff --git a/cva6/docs/VerifPlans/CVXIF/VP_IP002.pck b/cva6/docs/VerifPlans/CVXIF/VP_IP002.pck new file mode 100644 index 0000000000..7211f1b9e4 --- /dev/null +++ b/cva6/docs/VerifPlans/CVXIF/VP_IP002.pck @@ -0,0 +1,860 @@ +(VResult Interface +p0 +ccopy_reg +_reconstructor +p1 +(cvp_pack +Ip +p2 +c__builtin__ +object +p3 +Ntp4 +Rp5 +(dp6 +Vprop_count +p7 +I8 +sVname +p8 +g0 +sVprop_list +p9 +(dp10 +sVip_num +p11 +I2 +sVwid_order +p12 +I2 +sVrfu_dict +p13 +(dp14 +sVrfu_list +p15 +(lp16 +(V000_no speculative result transaction +p17 +g1 +(cvp_pack +Prop +p18 +g3 +Ntp19 +Rp20 +(dp21 +Vitem_count +p22 +I1 +sg8 +g17 +sVtag +p23 +VVP_CVXIF_F002_S000 +p24 +sVitem_list +p25 +(dp26 +sg12 +I0 +sg15 +(lp27 +(V000 +p28 +g1 +(cvp_pack +Item +p29 +g3 +Ntp30 +Rp31 +(dp32 +g8 +V000 +p33 +sg23 +VVP_CVXIF_F002_S000_I000 +p34 +sVdescription +p35 +VA coprocessor is not allowed to perform speculative result transactions. +p36 +sVpurpose +p37 +V +p38 +sVverif_goals +p39 +VThere is no result transaction for instructions that haven't been committed. Check that Result valid is only asserted for instructions that were committed (commit_valid == 1 && commit_kill == 0). +p40 +sVcoverage_loc +p41 +g38 +sVref_mode +p42 +Vpage +p43 +sVref_page +p44 +g38 +sVref_section +p45 +g38 +sVref_viewer +p46 +Vfirefox +p47 +sVpfc +p48 +I11 +sVtest_type +p49 +I10 +sVcov_method +p50 +I10 +sVcores +p51 +I56 +sVcomments +p52 +g38 +sVstatus +p53 +g38 +sVsimu_target_list +p54 +(lp55 +sg15 +(lp56 +sVrfu_list_2 +p57 +(lp58 +sg13 +(dp59 +Vlock_status +p60 +I0 +ssbtp61 +asVrfu_list_1 +p62 +(lp63 +sg57 +(lp64 +sg13 +(dp65 +sbtp66 +a(V001_out of order result transaction +p67 +g1 +(g18 +g3 +Ntp68 +Rp69 +(dp70 +g22 +I1 +sg8 +g67 +sg23 +VVP_CVXIF_F002_S001 +p71 +sg25 +(dp72 +sg12 +I1 +sg15 +(lp73 +(V000 +p74 +g1 +(g29 +g3 +Ntp75 +Rp76 +(dp77 +g8 +V000 +p78 +sg23 +VVP_CVXIF_F002_S001_I000 +p79 +sg35 +VA coprocessor is allowed to provide results to the core in an out of order fashion. +p80 +sg37 +g38 +sg39 +VCheck that the CPU is able to receive the result in an out of order fashion. +p81 +sg41 +g38 +sg42 +g43 +sg44 +g38 +sg45 +g38 +sg46 +g47 +sg48 +I3 +sg49 +I3 +sg50 +I1 +sg51 +I56 +sg52 +g38 +sg53 +g38 +sg54 +(lp82 +sg15 +(lp83 +sg57 +(lp84 +sg13 +(dp85 +g60 +I0 +ssbtp86 +asg62 +(lp87 +sg57 +(lp88 +sg13 +(dp89 +sbtp90 +a(V002_result transaction uniquness +p91 +g1 +(g18 +g3 +Ntp92 +Rp93 +(dp94 +g22 +I1 +sg8 +g91 +sg23 +VVP_CVXIF_F002_S002 +p95 +sg25 +(dp96 +sg12 +I2 +sg15 +(lp97 +(V000 +p98 +g1 +(g29 +g3 +Ntp99 +Rp100 +(dp101 +g8 +V000 +p102 +sg23 +VVP_CVXIF_F002_S002_I000 +p103 +sg35 +VEach accepted offloaded (committed and not killed) instruction shall have exactly one result group transaction (even if no data needs to be written back to the CPU\u2019s register file). +p104 +sg37 +g38 +sg39 +VThere is an unique result transaction for every accepted and commit instruction. +p105 +sg41 +g38 +sg42 +g43 +sg44 +g38 +sg45 +g38 +sg46 +g47 +sg48 +I11 +sg49 +I10 +sg50 +I10 +sg51 +I56 +sg52 +g38 +sg53 +g38 +sg54 +(lp106 +sg15 +(lp107 +sg57 +(lp108 +sg13 +(dp109 +g60 +I0 +ssbtp110 +asg62 +(lp111 +sg57 +(lp112 +sg13 +(dp113 +sbtp114 +a(V003_result packet stability +p115 +g1 +(g18 +g3 +Ntp116 +Rp117 +(dp118 +g22 +I1 +sg8 +g115 +sg23 +VVP_CVXIF_F002_S003 +p119 +sg25 +(dp120 +sg12 +I3 +sg15 +(lp121 +(V000 +p122 +g1 +(g29 +g3 +Ntp123 +Rp124 +(dp125 +g8 +V000 +p126 +sg23 +VVP_CVXIF_F002_S003_I000 +p127 +sg35 +VThe signals in result shall remain stable during a result transaction (except data ...) +p128 +sg37 +g38 +sg39 +VCheck that result signals (except data) are stable during result transaction (result_valid==1 jusqu'ŕ valid==ready ==1) +p129 +sg41 +g38 +sg42 +g43 +sg44 +g38 +sg45 +g38 +sg46 +g47 +sg48 +I4 +sg49 +I3 +sg50 +I2 +sg51 +I56 +sg52 +g38 +sg53 +g38 +sg54 +(lp130 +sg15 +(lp131 +sg57 +(lp132 +sg13 +(dp133 +g60 +I0 +ssbtp134 +asg62 +(lp135 +sg57 +(lp136 +sg13 +(dp137 +sbtp138 +a(V004_data stability +p139 +g1 +(g18 +g3 +Ntp140 +Rp141 +(dp142 +g22 +I1 +sg8 +g139 +sg23 +VVP_CVXIF_F002_S004 +p143 +sg25 +(dp144 +sg12 +I4 +sg15 +(lp145 +(V000 +p146 +g1 +(g29 +g3 +Ntp147 +Rp148 +(dp149 +g8 +V000 +p150 +sg23 +VVP_CVXIF_F002_S004_I000 +p151 +sg35 +VData is only required to remain stable during result transactions in which "we" is not 0. +p152 +sg37 +g38 +sg39 +VCheck that "data" remains stable when we==1. +p153 +sg41 +g38 +sg42 +g43 +sg44 +g38 +sg45 +g38 +sg46 +g47 +sg48 +I4 +sg49 +I3 +sg50 +I2 +sg51 +I56 +sg52 +g38 +sg53 +g38 +sg54 +(lp154 +sg15 +(lp155 +sg57 +(lp156 +sg13 +(dp157 +g60 +I0 +ssbtp158 +asg62 +(lp159 +sg57 +(lp160 +sg13 +(dp161 +sbtp162 +a(V005_synchronous exception +p163 +g1 +(g18 +g3 +Ntp164 +Rp165 +(dp166 +g22 +I3 +sg8 +g163 +sg23 +VVP_CVXIF_F002_S005 +p167 +sg25 +(dp168 +sg12 +I5 +sg15 +(lp169 +(V000 +p170 +g1 +(g29 +g3 +Ntp171 +Rp172 +(dp173 +g8 +V000 +p174 +sg23 +VVP_CVXIF_F002_S005_I000 +p175 +sg35 +VThe exc is used to signal synchronous exceptions. A synchronous exception will lead to a trap in CPU unless the corresponding instruction is killed. +p176 +sg37 +g38 +sg39 +VCheck that synchronous exception (exc ==1) leads to a trap in the CPU if the instruction is committed. +p177 +sg41 +g38 +sg42 +g43 +sg44 +g38 +sg45 +g38 +sg46 +g47 +sg48 +I3 +sg49 +I3 +sg50 +I1 +sg51 +I56 +sg52 +g38 +sg53 +g38 +sg54 +(lp178 +sg15 +(lp179 +sg57 +(lp180 +sg13 +(dp181 +g60 +I0 +ssbtp182 +a(V001 +p183 +g1 +(g29 +g3 +Ntp184 +Rp185 +(dp186 +g8 +V001 +p187 +sg23 +VVP_CVXIF_F002_S005_I001 +p188 +sg35 +Vexccode provides the least significant bits of the exception code bitfield of the mcause CSR. +p189 +sg37 +g38 +sg39 +VCheck that exccode signal is the value of the mcause CSR when exc == 1. +p190 +sg41 +g38 +sg42 +g43 +sg44 +g38 +sg45 +g38 +sg46 +g47 +sg48 +I-1 +sg49 +I-1 +sg50 +I-1 +sg51 +I56 +sg52 +g38 +sg53 +g38 +sg54 +(lp191 +sg15 +(lp192 +sg57 +(lp193 +sg13 +(dp194 +g60 +I0 +ssbtp195 +a(V002 +p196 +g1 +(g29 +g3 +Ntp197 +Rp198 +(dp199 +g8 +V002 +p200 +sg23 +VVP_CVXIF_F002_S005_I002 +p201 +sg35 +V "we" shall be driven to 0 by the coprocessor for synchronous exceptions. +p202 +sg37 +g38 +sg39 +VCheck that "we" signal == 0 when exc == 1. +p203 +sg41 +g38 +sg42 +g43 +sg44 +g38 +sg45 +g38 +sg46 +g47 +sg48 +I4 +sg49 +I-1 +sg50 +I2 +sg51 +I56 +sg52 +g38 +sg53 +g38 +sg54 +(lp204 +sg15 +(lp205 +sg57 +(lp206 +sg13 +(dp207 +g60 +I0 +ssbtp208 +asg62 +(lp209 +sg57 +(lp210 +sg13 +(dp211 +sbtp212 +a(V006_"we" value when dualwrite +p213 +g1 +(g18 +g3 +Ntp214 +Rp215 +(dp216 +g22 +I1 +sg8 +g213 +sg23 +VVP_CVXIF_F002_S006 +p217 +sg25 +(dp218 +sg12 +I6 +sg15 +(lp219 +(V000 +p220 +g1 +(g29 +g3 +Ntp221 +Rp222 +(dp223 +g8 +V000 +p224 +sg23 +VVP_CVXIF_F002_S006_I000 +p225 +sg35 +Vwe is 2 bits wide when XLEN` = 32 and X_RFW_WIDTH = 64, and 1 bit wide otherwise. If "we" is 2 bits wide, then we[1] is only allowed to be 1 if we[0] is 1 as well (i.e. for dual writeback). +p226 +sg37 +g38 +sg39 +VFor dualwrite instruction, check that we[1]==1 is only allowed if we[0] == 1. +p227 +sg41 +g38 +sg42 +g43 +sg44 +g38 +sg45 +g38 +sg46 +g47 +sg48 +I4 +sg49 +I3 +sg50 +I2 +sg51 +I56 +sg52 +g38 +sg53 +g38 +sg54 +(lp228 +sg15 +(lp229 +sg57 +(lp230 +sg13 +(dp231 +g60 +I0 +ssbtp232 +asg62 +(lp233 +sg57 +(lp234 +sg13 +(dp235 +sbtp236 +a(V007_proper result transaction +p237 +g1 +(g18 +g3 +Ntp238 +Rp239 +(dp240 +g22 +I1 +sg8 +g237 +sg23 +VVP_CVXIF_F002_S007 +p241 +sg25 +(dp242 +sg12 +I7 +sg15 +(lp243 +(V000 +p244 +g1 +(g29 +g3 +Ntp245 +Rp246 +(dp247 +g8 +V000 +p248 +sg23 +VVP_CVXIF_F002_S007_I000 +p249 +sg35 +VResult transaction starts in the cycle that result_valid = 1 and ends in the cycle that both result_valid == result_ready == 1. +p250 +sg37 +g38 +sg39 +VCheck that result transaction ends properly. +p251 +sg41 +g38 +sg42 +g43 +sg44 +g38 +sg45 +g38 +sg46 +g47 +sg48 +I4 +sg49 +I3 +sg50 +I2 +sg51 +I56 +sg52 +g38 +sg53 +g38 +sg54 +(lp252 +sg15 +(lp253 +sg57 +(lp254 +sg13 +(dp255 +g60 +I0 +ssbtp256 +asg62 +(lp257 +sg57 +(lp258 +sg13 +(dp259 +sbtp260 +asVrfu_list_0 +p261 +(lp262 +sg62 +(lp263 +sVvptool_gitrev +p264 +V$Id: a782de3eec3de5ff99661fb165c09f541b4228d0 $ +p265 +sVio_fmt_gitrev +p266 +V$Id: 2f6f9e7bc800d8b831382463dc706473c6c6ad8c $ +p267 +sVconfig_gitrev +p268 +V$Id: 0422e19126dae20ffc4d5a84e4ce3de0b6eb4eb5 $ +p269 +sVymlcfg_gitrev +p270 +V$Id: 286c689bd48b7a58f9a37754267895cffef1270c $ +p271 +sbtp272 +. \ No newline at end of file diff --git a/cva6/docs/VerifPlans/CVXIF/runme.sh b/cva6/docs/VerifPlans/CVXIF/runme.sh new file mode 100644 index 0000000000..f1be65625f --- /dev/null +++ b/cva6/docs/VerifPlans/CVXIF/runme.sh @@ -0,0 +1,34 @@ +############################################################################# +# Copyright (C) 2022 Thales DIS France SAS +# +# SPDX-License-Identifier: Apache-2.0 WITH SHL-2.0. +# +# Original Author: Zbigniew Chamski (zbigniew.chamski@thalesgroup.com) +############################################################################# +#!/bin/sh + +# Location of project-specific directories +ROOTDIR=`readlink -f $(dirname "${BASH_SOURCE[0]}")` + +# Set up platform location. It can be anywhere but should contain +# a valid `vp_config.py` file in `vptool` directory. +# Here we use the verification tree from the example directory. +export PLATFORM_TOP_DIR="$ROOTDIR" + +# Set the printable name for the project that will be used +# in the human-readable documentation. +export PROJECT_NAME="CVXIF" + +# Set the alphanumerical identifier of the project that +# will be used to construct file names etc. +export PROJECT_IDENT="CVXIF" + +# Set the destination directory of Markdown files for this project. +# Since it will be used by VPTOOL, it shall NOT be a relative path. +export MARKDOWN_OUTPUT_DIR=`readlink -f "$ROOTDIR/../source"` + +# Run VPTOOL overriding the default theme from Yaml config with 'winxpblue'. +# FIXME: Introduce a suitably named shell variable that points to the root +# directory of the tool set (TOOL_TOP etc.) +# FORNOW use a hardcoded relative path. +python3 $ROOTDIR/../../../../tools/vptool/vptool/vp.py -t winxpblue diff --git a/cva6/docs/VerifPlans/source/dvplan_CVXIF.md b/cva6/docs/VerifPlans/source/dvplan_CVXIF.md new file mode 100644 index 0000000000..24d31a54eb --- /dev/null +++ b/cva6/docs/VerifPlans/source/dvplan_CVXIF.md @@ -0,0 +1,556 @@ +# Module: CVXIF + +## Feature: Issue Interface + +### Sub-feature: 000_issue_req signals stable + +#### Item: 000 + +* **Requirement location:** +* **Feature Description** + + The “instr” and “mode” signals remain stable during an Issue request transaction. +* **Verification Goals** + + Check that “mode” and “instr” are stable during an issue transaction (cannot be modified by an instruction when transaction issue is in process) +* **Pass/Fail Criteria:** Assertion +* **Test Type:** Constrained Random +* **Coverage Method:** Assertion Coverage +* **Applicable Cores:** CV32A6_v0.1.0, CV32A6-step2, CV64A6-step3 +* **Unique verification tag:** VP_CVXIF_F000_S000_I000 +* **Link to Coverage:** +* **Comments** + + *(none)* + +### Sub-feature: 001_mode signal value + +#### Item: 000 + +* **Requirement location:** +* **Feature Description** + + When issue transaction starts, instruction and current CPU mode are provided +* **Verification Goals** + + Check that a mode modification coming from execution of a first instruction is well provided to the following offloaded instruction +* **Pass/Fail Criteria:** Check RM +* **Test Type:** Constrained Random +* **Coverage Method:** Functional Coverage +* **Applicable Cores:** CV32A6_v0.1.0, CV32A6-step2, CV64A6-step3 +* **Unique verification tag:** VP_CVXIF_F000_S001_I000 +* **Link to Coverage:** +* **Comments** + + *(none)* + +#### Item: 001 + +* **Requirement location:** +* **Feature Description** + + Check “mode” signal values. +* **Verification Goals** + + Check that mode take a value that the CPU supports : Privilege level (2’b00 = User, 2’b01 = Supervisor, 2’b10 = Reserved, + 2’b11 = Machine). +* **Pass/Fail Criteria:** NDY (Not Defined Yet) +* **Test Type:** NDY (Not Defined Yet) +* **Coverage Method:** NDY (Not Defined Yet) +* **Applicable Cores:** CV32A6_v0.1.0, CV32A6-step2, CV64A6-step3 +* **Unique verification tag:** VP_CVXIF_F000_S001_I001 +* **Link to Coverage:** +* **Comments** + + *(none)* + +### Sub-feature: 002_rs_valid signal transition order + +#### Item: 000 + +* **Requirement location:** +* **Feature Description** + + During a transaction, each bit of “rs_valid” can transition from 0 to 1 but are not allowed to transition back to 0. +* **Verification Goals** + + For issue transaction which lasts more than one cycle, check that asserted “rs_valid” signals do not transition back to 0.(for i in [0;2] if rs_valid[i] = 1 then rs_valid[i] → 0 cannot happen) +* **Pass/Fail Criteria:** Assertion +* **Test Type:** Constrained Random +* **Coverage Method:** Assertion Coverage +* **Applicable Cores:** CV32A6_v0.1.0, CV32A6-step2, CV64A6-step3 +* **Unique verification tag:** VP_CVXIF_F000_S002_I000 +* **Link to Coverage:** +* **Comments** + + *(none)* + +### Sub-feature: 003_rs signal value + +#### Item: 000 + +* **Requirement location:** +* **Feature Description** + + If XLEN = X_RFR_WIDTH, then rs[X_NUM_RS-1:0] correspond to rs1 and rs2 CPU registers (and rs3 if X_NUM_RS = 3). +* **Verification Goals** + + For every issue transaction check that rs signal correspond to rs1,rs2(rs3) value in CPU register file. +* **Pass/Fail Criteria:** Check RM +* **Test Type:** Constrained Random +* **Coverage Method:** Functional Coverage +* **Applicable Cores:** CV32A6_v0.1.0, CV32A6-step2, CV64A6-step3 +* **Unique verification tag:** VP_CVXIF_F000_S003_I000 +* **Link to Coverage:** +* **Comments** + + *(none)* + +#### Item: 001 + +* **Requirement location:** +* **Feature Description** + + rs signals are only required to be stable during the part of a transaction in which these signals are considered to be valid. +* **Verification Goals** + + Check that rs signals are stable when issue_valid==1 && the corresponding bit in rs_valid is 1. +* **Pass/Fail Criteria:** Assertion +* **Test Type:** NDY (Not Defined Yet) +* **Coverage Method:** Assertion Coverage +* **Applicable Cores:** CV32A6_v0.1.0, CV32A6-step2, CV64A6-step3 +* **Unique verification tag:** VP_CVXIF_F000_S003_I001 +* **Link to Coverage:** +* **Comments** + + *(none)* + +#### Item: 002 + +* **Requirement location:** +* **Feature Description** + + If XLEN != X_RFR_WIDTH , then rs[X_NUM_RS-1:0] correspond to even/odd register pair with rs1, rs2, (rs3) are even register and even register is provided in the 32 lower bits of rs signal. +* **Verification Goals** + + For every issue transaction check that rs signal correspond to the concatenation of rs1/rs1+1,rs2/rs2+1, (rs3/rs3+1) value in CPU register file and even register is in the 32 lower bits of rs. +* **Pass/Fail Criteria:** NDY (Not Defined Yet) +* **Test Type:** NDY (Not Defined Yet) +* **Coverage Method:** NDY (Not Defined Yet) +* **Applicable Cores:** CV32A6_v0.1.0, CV32A6-step2, CV64A6-step3 +* **Unique verification tag:** VP_CVXIF_F000_S003_I002 +* **Link to Coverage:** +* **Comments** + + *(none)* + +### Sub-feature: 004_Default value for unaccepted instruction + +#### Item: 000 + +* **Requirement location:** +* **Feature Description** + + If accept == 0 : + Writeback == 0; dualwrite == 0; dualread == 0; loadstore == 0; exc = 0. +* **Verification Goals** + + Check that for writeback; dualwrite; dualread; loadstore; exc signals if accept == 0 then all those signals are 0. +* **Pass/Fail Criteria:** Assertion +* **Test Type:** Constrained Random +* **Coverage Method:** Assertion Coverage +* **Applicable Cores:** CV32A6_v0.1.0, CV32A6-step2, CV64A6-step3 +* **Unique verification tag:** VP_CVXIF_F000_S004_I000 +* **Link to Coverage:** +* **Comments** + + *(none)* + +### Sub-feature: 005_Illegal Instruction causes + +#### Item: 000 + +* **Requirement location:** +* **Feature Description** + + The CPU shall cause an illegal instruction if: + - an instruction is considered to be valid by the CPU and accepted by the coprocessor (accept = 1) + - neither to be valid by the CPU nor accepted by the coprocessor (accept = 0) +* **Verification Goals** + + - CPU causes illegal instruction for instruction accepted by the core and the coprocessor. + - CPU causes illegal instruction exception for instruction that are not valid for coprocessor and CPU +* **Pass/Fail Criteria:** Check RM +* **Test Type:** Constrained Random +* **Coverage Method:** Functional Coverage +* **Applicable Cores:** CV32A6_v0.1.0, CV32A6-step2, CV64A6-step3 +* **Unique verification tag:** VP_CVXIF_F000_S005_I000 +* **Link to Coverage:** +* **Comments** + + *(none)* + +### Sub-feature: 006_issue uniquness + +#### Item: 000 + +* **Requirement location:** +* **Feature Description** + + Check for issue id validity. +* **Verification Goals** + + Check that the issue interface doesn't issue an "id" that isn't legal to be used (has not fully completed). +* **Pass/Fail Criteria:** Other +* **Test Type:** Constrained Random +* **Coverage Method:** N/A +* **Applicable Cores:** CV32A6_v0.1.0, CV32A6-step2, CV64A6-step3 +* **Unique verification tag:** VP_CVXIF_F000_S006_I000 +* **Link to Coverage:** +* **Comments** + + *(none)* + +### Sub-feature: 007_coprocessor decoding + +#### Item: 000 + +* **Requirement location:** +* **Feature Description** + + Accept = 1 if: + - coprocessor can handle the instruction based on decoding “instr”and "mode". + - “issue_valid” == 1 and required bit(s) of “rs_valid” are 1. +* **Verification Goals** + + To be checked in coprocessor. +* **Pass/Fail Criteria:** Check RM +* **Test Type:** Constrained Random +* **Coverage Method:** Functional Coverage +* **Applicable Cores:** CV32A6_v0.1.0, CV32A6-step2, CV64A6-step3 +* **Unique verification tag:** VP_CVXIF_F000_S007_I000 +* **Link to Coverage:** +* **Comments** + + *(none)* + +### Sub-feature: 008_Transaction definition + +#### Item: 000 + +* **Requirement location:** +* **Feature Description** + + “issue_resp” signals and “issue_req” signals are accepted when “issue_valid” == “issue_ready” == 1 + “issue_resp” is valid when "valid==ready==1". + “issue_req” is valid when "valid==1" +* **Verification Goals** + + The definition of a transaction. + Not to be verified. +* **Pass/Fail Criteria:** Other +* **Test Type:** Other +* **Coverage Method:** N/A +* **Applicable Cores:** CV32A6_v0.1.0, CV32A6-step2, CV64A6-step3 +* **Unique verification tag:** VP_CVXIF_F000_S008_I000 +* **Link to Coverage:** +* **Comments** + + *(none)* + +## Feature: Commit Interface + +### Sub-feature: 000_commit_valid pulse + +#### Item: 000 + +* **Requirement location:** +* **Feature Description** + + The “commit_valid” == 1 exactly one clk cycle for every offloaded Instruction by the coprocessor (whether accepted or not). +* **Verification Goals** + + For every offloaded instruction, check that commit_valid is asserted exactly one clk cycle ( is a pulse ). +* **Pass/Fail Criteria:** Assertion +* **Test Type:** Constrained Random +* **Coverage Method:** Assertion Coverage +* **Applicable Cores:** CV32A6_v0.1.0, CV32A6-step2, CV64A6-step3 +* **Unique verification tag:** VP_CVXIF_F001_S000_I000 +* **Link to Coverage:** +* **Comments** + + *(none)* + +### Sub-feature: 001_commit transaction uniquness + +#### Item: 000 + +* **Requirement location:** +* **Feature Description** + + There is a unique commit transaction for every issue transaction (unique until an instruction has "fully completed" = its result has been submitted). +* **Verification Goals** + + Check that the commit interface doesn't commit an "id" that isn't legal to be used (hasn't been seen in earlier stages, or has not fully completed). +* **Pass/Fail Criteria:** Self-Check +* **Test Type:** Other +* **Coverage Method:** N/A +* **Applicable Cores:** CV32A6_v0.1.0, CV32A6-step2, CV64A6-step3 +* **Unique verification tag:** VP_CVXIF_F001_S001_I000 +* **Link to Coverage:** +* **Comments** + + *(none)* + +### Sub-feature: 002_commit transaction for every issue transaction + +#### Item: 000 + +* **Requirement location:** +* **Feature Description** + + - The CPU shall perform a commit transaction for every issue transaction, independent of the accept value of the issue transaction. + - For each offloaded and accepted instruction the core is guaranteed to (eventually) signal that such an instruction is either no longer speculative and can be committed (commit_valid is 1 and commit_kill is 0) or that the instruction must be killed (commit_valid is 1 and commit_kill is 1). +* **Verification Goals** + + Check that for each issue transaction, the commit transaction is sent at the same clock cycle than the issue transaction, or at any clock cycle after the issue transaction. +* **Pass/Fail Criteria:** Assertion +* **Test Type:** Constrained Random +* **Coverage Method:** Assertion Coverage +* **Applicable Cores:** CV32A6_v0.1.0, CV32A6-step2, CV64A6-step3 +* **Unique verification tag:** VP_CVXIF_F001_S002_I000 +* **Link to Coverage:** +* **Comments** + + *(none)* + +### Sub-feature: 003_Transaction definition + +#### Item: 000 + +* **Requirement location:** +* **Feature Description** + + The signals in commit are valid when commit_valid is 1. +* **Verification Goals** + + The definition of a transaction. + Not to be verified. +* **Pass/Fail Criteria:** Other +* **Test Type:** NDY (Not Defined Yet) +* **Coverage Method:** N/A +* **Applicable Cores:** CV32A6_v0.1.0, CV32A6-step2, CV64A6-step3 +* **Unique verification tag:** VP_CVXIF_F001_S003_I000 +* **Link to Coverage:** +* **Comments** + + *(none)* + +## Feature: Result Interface + +### Sub-feature: 000_no speculative result transaction + +#### Item: 000 + +* **Requirement location:** +* **Feature Description** + + A coprocessor is not allowed to perform speculative result transactions. +* **Verification Goals** + + There is no result transaction for instructions that haven't been committed. Check that Result valid is only asserted for instructions that were committed (commit_valid == 1 && commit_kill == 0). +* **Pass/Fail Criteria:** Other +* **Test Type:** Other +* **Coverage Method:** N/A +* **Applicable Cores:** CV32A6_v0.1.0, CV32A6-step2, CV64A6-step3 +* **Unique verification tag:** VP_CVXIF_F002_S000_I000 +* **Link to Coverage:** +* **Comments** + + *(none)* + +### Sub-feature: 001_out of order result transaction + +#### Item: 000 + +* **Requirement location:** +* **Feature Description** + + A coprocessor is allowed to provide results to the core in an out of order fashion. +* **Verification Goals** + + Check that the CPU is able to receive the result in an out of order fashion. +* **Pass/Fail Criteria:** Check RM +* **Test Type:** Constrained Random +* **Coverage Method:** Functional Coverage +* **Applicable Cores:** CV32A6_v0.1.0, CV32A6-step2, CV64A6-step3 +* **Unique verification tag:** VP_CVXIF_F002_S001_I000 +* **Link to Coverage:** +* **Comments** + + *(none)* + +### Sub-feature: 002_result transaction uniquness + +#### Item: 000 + +* **Requirement location:** +* **Feature Description** + + Each accepted offloaded (committed and not killed) instruction shall have exactly one result group transaction (even if no data needs to be written back to the CPU’s register file). +* **Verification Goals** + + There is an unique result transaction for every accepted and commit instruction. +* **Pass/Fail Criteria:** Other +* **Test Type:** Other +* **Coverage Method:** N/A +* **Applicable Cores:** CV32A6_v0.1.0, CV32A6-step2, CV64A6-step3 +* **Unique verification tag:** VP_CVXIF_F002_S002_I000 +* **Link to Coverage:** +* **Comments** + + *(none)* + +### Sub-feature: 003_result packet stability + +#### Item: 000 + +* **Requirement location:** +* **Feature Description** + + The signals in result shall remain stable during a result transaction (except data ...) +* **Verification Goals** + + Check that result signals (except data) are stable during result transaction (result_valid==1 jusqu'Ă  valid==ready ==1) +* **Pass/Fail Criteria:** Assertion +* **Test Type:** Constrained Random +* **Coverage Method:** Assertion Coverage +* **Applicable Cores:** CV32A6_v0.1.0, CV32A6-step2, CV64A6-step3 +* **Unique verification tag:** VP_CVXIF_F002_S003_I000 +* **Link to Coverage:** +* **Comments** + + *(none)* + +### Sub-feature: 004_data stability + +#### Item: 000 + +* **Requirement location:** +* **Feature Description** + + Data is only required to remain stable during result transactions in which "we" is not 0. +* **Verification Goals** + + Check that "data" remains stable when we==1. +* **Pass/Fail Criteria:** Assertion +* **Test Type:** Constrained Random +* **Coverage Method:** Assertion Coverage +* **Applicable Cores:** CV32A6_v0.1.0, CV32A6-step2, CV64A6-step3 +* **Unique verification tag:** VP_CVXIF_F002_S004_I000 +* **Link to Coverage:** +* **Comments** + + *(none)* + +### Sub-feature: 005_synchronous exception + +#### Item: 000 + +* **Requirement location:** +* **Feature Description** + + The exc is used to signal synchronous exceptions. A synchronous exception will lead to a trap in CPU unless the corresponding instruction is killed. +* **Verification Goals** + + Check that synchronous exception (exc ==1) leads to a trap in the CPU if the instruction is committed. +* **Pass/Fail Criteria:** Check RM +* **Test Type:** Constrained Random +* **Coverage Method:** Functional Coverage +* **Applicable Cores:** CV32A6_v0.1.0, CV32A6-step2, CV64A6-step3 +* **Unique verification tag:** VP_CVXIF_F002_S005_I000 +* **Link to Coverage:** +* **Comments** + + *(none)* + +#### Item: 001 + +* **Requirement location:** +* **Feature Description** + + exccode provides the least significant bits of the exception code bitfield of the mcause CSR. +* **Verification Goals** + + Check that exccode signal is the value of the mcause CSR when exc == 1. +* **Pass/Fail Criteria:** NDY (Not Defined Yet) +* **Test Type:** NDY (Not Defined Yet) +* **Coverage Method:** NDY (Not Defined Yet) +* **Applicable Cores:** CV32A6_v0.1.0, CV32A6-step2, CV64A6-step3 +* **Unique verification tag:** VP_CVXIF_F002_S005_I001 +* **Link to Coverage:** +* **Comments** + + *(none)* + +#### Item: 002 + +* **Requirement location:** +* **Feature Description** + +  "we" shall be driven to 0 by the coprocessor for synchronous exceptions. +* **Verification Goals** + + Check that "we" signal == 0 when exc == 1. +* **Pass/Fail Criteria:** Assertion +* **Test Type:** NDY (Not Defined Yet) +* **Coverage Method:** Assertion Coverage +* **Applicable Cores:** CV32A6_v0.1.0, CV32A6-step2, CV64A6-step3 +* **Unique verification tag:** VP_CVXIF_F002_S005_I002 +* **Link to Coverage:** +* **Comments** + + *(none)* + +### Sub-feature: 006_"we" value when dualwrite + +#### Item: 000 + +* **Requirement location:** +* **Feature Description** + + we is 2 bits wide when XLEN` = 32 and X_RFW_WIDTH = 64, and 1 bit wide otherwise. If "we" is 2 bits wide, then we[1] is only allowed to be 1 if we[0] is 1 as well (i.e. for dual writeback). +* **Verification Goals** + + For dualwrite instruction, check that we[1]==1 is only allowed if we[0] == 1. +* **Pass/Fail Criteria:** Assertion +* **Test Type:** Constrained Random +* **Coverage Method:** Assertion Coverage +* **Applicable Cores:** CV32A6_v0.1.0, CV32A6-step2, CV64A6-step3 +* **Unique verification tag:** VP_CVXIF_F002_S006_I000 +* **Link to Coverage:** +* **Comments** + + *(none)* + +### Sub-feature: 007_proper result transaction + +#### Item: 000 + +* **Requirement location:** +* **Feature Description** + + Result transaction starts in the cycle that result_valid = 1 and ends in the cycle that both result_valid == result_ready == 1. +* **Verification Goals** + + Check that result transaction ends properly. +* **Pass/Fail Criteria:** Assertion +* **Test Type:** Constrained Random +* **Coverage Method:** Assertion Coverage +* **Applicable Cores:** CV32A6_v0.1.0, CV32A6-step2, CV64A6-step3 +* **Unique verification tag:** VP_CVXIF_F002_S007_I000 +* **Link to Coverage:** +* **Comments** + + *(none)* + diff --git a/cva6/docs/VerifPlans/source/index.rst b/cva6/docs/VerifPlans/source/index.rst index 4ef40bc021..cca28ad841 100644 --- a/cva6/docs/VerifPlans/source/index.rst +++ b/cva6/docs/VerifPlans/source/index.rst @@ -25,4 +25,5 @@ CV32A6-step1 Design Verification Plan dvplan_intro dvplan_FRONTEND dvplan_ISA + dvplan_CVXIF