Add support for the Zvkned extension

[charmitro]

Implements the Zvkned (NIST Suite: Vector AES Block Cipher) extension, as of version Draft: 20230303
.

The following instructions are included:

• vaesef.[vv,vs]
• vaesem.[vv,vs]
• vaesdf.[vv,vs]
• vaesdm.[vv,vs]
• vaeskf1.vi
• vaeskf2.vi
• vaesz.vs

All instructions were tested with VLEN=128 and results were compared with QEMU results of each instruction.

Current revision is rebased with the latest changes of vector-dev branch.

Note
It's better to merge all of Zvk extension support PRs in the created order, as this is going to create conflicts and it would be easier to resolve them.

[charmitro]

One note, the latest revision of vector-dev branch fails to build, therefore this PR , #235 & #236 are failing to build also since they are synchronized.

[charmitro]

Updated the PR:

• Correction on iterating based on the specification
• Correctly Load & Store from/to vector registers

This update is adjusting the implementation to match the Spike implenentation and as a follow-up, ACT Signatures matching.

[charmitro]

Rebased from vector-dev branch.

[nibrunieAtSi5]

SAIL newbie question: the vector crypto spec distinguishes illegal cases ((LMUL*VLEN) < (num_elem*SEW)) and reserved cases (((unsigned(vl)%num_elem) != 0) | ((unsigned(vstart)%num_elem) != 0)) (which can legally raise an illegal exception or not). Does this difference is required in the sail model ?

[allenjbaum]

I would argue that it does if we want to be able to test that DUTs that support either behavior do so correctly. This is an Archie rural option, and the Sail model should support ALL architectural options.

…

On Thursday, May 25, 2023, Nicolas Brunie ***@***.***> wrote: ***@***.**** commented on this pull request. ------------------------------ In model/riscv_insts_zvkned.sail <#234 (comment)>: > @@ -0,0 +1,550 @@ +/* + * Vector Cryptography Extension - NIST Suite: Vecttor AES Block Cipher ⬇️ Suggested change - * Vector Cryptography Extension - NIST Suite: Vecttor AES Block Cipher + * Vector Cryptography Extension - NIST Suite: Vector AES Block Cipher ------------------------------ In model/riscv_insts_zvkned.sail <#234 (comment)>: > +function zvk_check_elements(VLEN, num_elem, LMUL, SEW) = { + ((unsigned(vl)%num_elem) != 0) | ((unsigned(vstart)%num_elem) != 0) | (LMUL*VLEN) < (num_elem*SEW) +} SAIL newbie question: the vector crypto spec distinguishes illegal cases ((LMUL*VLEN) < (num_elem*SEW)) and reserved cases (((unsigned(vl)%num_elem) != 0) | ((unsigned(vstart)%num_elem) != 0)) (which can legally raise an illegal exception or not). Does this difference is required in the sail model ? ------------------------------ In model/riscv_insts_zvkned.sail <#234 (comment)>: > + +function clause execute (RISCV_VAESEF(vs2, vd, suffix)) = { + let SEW = get_sew(); + let LMUL_pow = get_lmul_pow(); + let LMUL = if LMUL_pow < 0 then 0 else LMUL_pow; + let VLEN = int_power(2, get_vlen_pow()); + let num_elem = get_num_elem(LMUL_pow, SEW); + + if (zvk_check_elements(VLEN, num_elem, LMUL, SEW) == false) + then { + handle_illegal(); + RETIRE_FAIL + } else { + let 'n = num_elem; + let 'm = SEW; + assert('m == 32); what is the difference between the assert here and the handle_illegal before ? (Are they both equivalent to raising the illegal instruction exception or is it assumed SEW should be equal to 32 by that point and else the illegal instruction exception was raised before ?) — Reply to this email directly, view it on GitHub <#234 (review)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AHPXVJQ77OKGRP7KNAMEQLTXH64XBANCNFSM6AAAAAAWFGXXLI> . You are receiving this because you are subscribed to this thread.Message ID: ***@***.***>

[nibrunieAtSi5]

Would it make sense to define both vd_state and vs2_key within the scope of the foreach since they are only used in the loop body and their live range does not exceed one iteration ?

[charmitro]

ACK., good catch!

[nibrunieAtSi5]

There are reserved encodings for the .vs form (for example when vs2 scalar element groups overlaps the vd register group), where would such constraint appear in the SAIL code ?

[charmitro]

I'm handling he .vs && .vv forms conditionally using the suffix of each instruction.

 if suffix == "vv" then { ... } else { ... }

But I might misunderstood this one.

[nibrunieAtSi5]

the last term looks suspicious, is it trying to implement EGW <= VLEN * LMUL / EGS <= VLMAX ?
If so I do not think this is correct, for example I don't understand how the EGS / EGW is injected. Could a comment be added to explain which checks this function is supposed to perform ?

[charmitro]

This is implementing the following found in the specification, Version v0.4.2, 03 March, 2023.

if( ((vl%EGS)<>0) | ((vstart%EGS)<>0) | (LMUL*VLEN < EGW))  then {
      handle_illegal();  // illegal instruction exception
      RETIRE_SUCCESS
    } else {
    . . . 

[nibrunieAtSi5]

How is EGW derived from num_elen * SEW ?

[charmitro]

From the Vector Crypto Spec we have,

• Element Group Width (EGW) - total number of bits in an element group 
• Effective Element Width (EEW) - number of bits in each element
• Element Group Size (EGS) - number of elements in an element group
For all of the vector crypto instructions in this specification, EEW=SEW.

So here we're doing EGS * EEW, given the above:

• num_elem = EGS
• SEW = EEW

[nibrunieAtSi5]

Sorry but I am still missing something, it looks like num_elem comes from get_num_elem and I do not get how EGS appears here:

$ git grep -A8 "fun.*get_num_elem" *.sail
model/riscv_vext_regs.sail:function get_num_elem(LMUL_pow, SEW) = {
model/riscv_vext_regs.sail-  let VLEN = int_power(2, get_vlen_pow());
model/riscv_vext_regs.sail-  let LMUL_pow_reg = if LMUL_pow < 0 then 0 else LMUL_pow;
model/riscv_vext_regs.sail-  /* Ignore lmul < 1 so that the entire vreg is read, allowing all masking to
model/riscv_vext_regs.sail-   * be handled in init_masked_result */
model/riscv_vext_regs.sail-  let num_elem = int_power(2, LMUL_pow_reg) * VLEN / SEW;
model/riscv_vext_regs.sail-  assert(num_elem > 0);
model/riscv_vext_regs.sail-  num_elem
model/riscv_vext_regs.sail-}

[charmitro]

I'll analyse this SAIL internal first and reach back. I'm positive get_num_elem returns the correct value, but a double-check is not a problem.

[github-actions]

Unit Test Results

712 tests  ±0   712 ✔️ ±0   0s ⏱️ ±0s
    6 suites ±0       0 💤 ±0 
    1 files   ±0       0 ❌ ±0 

Results for commit c4858f3. ± Comparison against base commit 5872908.

♻️ This comment has been updated with latest results.

[nibrunieAtSi5]

@charmitro , when I tried to build this branch, I get the following error:

Type error:
model/riscv_insts_vext_utils.sail:422.23-32:
422 |    16 => (xf[15..15], xf[14..0]),
    |                       ^-------^
    | Tried performing type coercion from bitvector(((14 - 0) + 1), dec) to bitvector(('n * 1), dec) on subrange_bits(xf, 14, 0)
    | Coercion failed because:
    | Failed to prove constraint: ((14 - 0) + 1) == ('n * 1)
make: *** [Makefile:315: generated_definitions/lem/RV64/riscv.lem] Error 1

Do you know if this is a known issue ?

[charmitro]

@charmitro , when I tried to build this branch, I get the following error:

Type error:
model/riscv_insts_vext_utils.sail:422.23-32:
422 |    16 => (xf[15..15], xf[14..0]),
    |                       ^-------^
    | Tried performing type coercion from bitvector(((14 - 0) + 1), dec) to bitvector(('n * 1), dec) on subrange_bits(xf, 14, 0)
    | Coercion failed because:
    | Failed to prove constraint: ((14 - 0) + 1) == ('n * 1)
make: *** [Makefile:315: generated_definitions/lem/RV64/riscv.lem] Error 1

Do you know if this is a known issue ?

I can't seem to reproduce it on my side. Could it be a problem in the upstream vector-dev branch(I believe at some point it was force-pushed, try resetting it(?)), but on my forked vector-dev branch everything seems fine.