Zvkned: add infrastructure for Zvkned #752
Conversation
To support the implementation of Zvkned extension in SAIL, this creates the necessary infrastructure(i.e., a file to hold it, and the extension macro), preparing the tree for the Zvkned implementation. Signed-off-by: Charalampos Mitrodimas <charalampos.mitrodimas@vrull.eu> Co-authored-by: KotorinMinami <98281165+KotorinMinami@users.noreply.github.com>
| let LMUL = if LMUL_pow < 0 then 0 else LMUL_pow; | ||
| let num_elem = get_num_elem(LMUL_pow, SEW); | ||
|
|
||
| if (zvk_check_elements(VLEN, num_elem, LMUL, SEW) == false) |
There was a problem hiding this comment.
| if (zvk_check_elements(VLEN, num_elem, LMUL, SEW) == false) | |
| if not(zvk_check_elements(VLEN, num_elem, LMUL, SEW)) |
(And in the other places.)
|
|
||
| val aes_rotword : bits(32) -> bits(32) | ||
| function aes_rotword(x) = { | ||
| let a0 : bits (8) = x[ 7.. 0]; |
There was a problem hiding this comment.
I think I would just simplify this to
function aes_rotword(x) = x[7 .. 0] @ x[15 .. 8] @ x[23 .. 16] @ x[31 .. 24]
| } else { | ||
| let 'n = num_elem; | ||
| let 'm = SEW; | ||
| assert('m == 32); |
There was a problem hiding this comment.
Is this necessarily true? Definitely worth a comment explaining why at least.
|
|
||
| let eg_len = (unsigned(vl) / 'n); | ||
| let eg_start = (unsigned(vstart) / 'n); | ||
| let keyelem = if suffix == "vv" then 1 else 0; |
There was a problem hiding this comment.
I think we should avoid having behaviour encoded in strings. suffix should be an enum, not strings.
| assert(0 <= ((i * 4) + 3) & ((i * 4) + 3) < 'n); | ||
|
|
||
| let vd_state = get_velem(vd_val, i); | ||
| let vs2_key = get_velem(vs2_val, keyelem * i); |
There was a problem hiding this comment.
So this would be something like:
let vs2_key = get_velem(vs2_val, match suffix { something_VV => i, something_VS => 0 });
(I'll leave you to come up with suitable names for whatever VV and VS mean!)
| let vs2_key = get_velem(vs2_val, keyelem * i); | ||
| let sb : bitvector(128) = aes_subbytes_fwd(vd_state); | ||
| let sr : bitvector(128) = aes_shift_rows_fwd(sb); | ||
| let ark : bitvector(128) = sr ^ vs2_key; |
There was a problem hiding this comment.
bits? Maybe before my time; is bitvector an old version of bits?
| let sb : bitvector(128, dec) = aes_subbytes_fwd(vd_state); | ||
| let sr : bitvector(128, dec) = aes_shift_rows_fwd(sb); | ||
| let mix : bitvector(128, dec) = aes_mixcolumns_fwd(sr); | ||
| let ark : bitvector(128, dec) = mix ^ vs2_key; |
There was a problem hiding this comment.
bits(128). You could just delete all these, though it may be appropriate for readability.
| assert('m == 32); | ||
|
|
||
| let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); | ||
| let vd_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); |
There was a problem hiding this comment.
Remove , dec - Sail doesn't support per-vector orders now.
You could just delete the type annotations (I would, but up to you).
| /* VAESDM.VV */ | ||
|
|
||
| mapping vaesdm_mnemonic : bits(7) <-> string = { | ||
| 0b1010001 <-> "vaesem.vv", | ||
| 0b1010011 <-> "vaesem.vs", | ||
| } |
There was a problem hiding this comment.
Comment and mapping name states vaesdm but the mapping itself is happening for vaesem.[vv, vs] mnemonics.
There was a problem hiding this comment.
Also the rest of the model maps ast to assembly; not the bits directly.
| function get_velem(v, i) = v[4 * i + 3] @ v[4 * i + 2] @ v[4 * i + 1] @ v[4 * i] | ||
|
|
||
| val zvk_check_elements : (int, int, int, int) -> bool | ||
| function zvk_check_elements(VLEN, num_elem, LMUL, SEW) = { |
There was a problem hiding this comment.
With simple function declarations like this, it’s usually easier to eliminate the val line and directly integrate the types into the function line.
| @@ -0,0 +1,428 @@ | |||
| /* | |||
There was a problem hiding this comment.
Missing copyright header
| @@ -23,6 +23,7 @@ enum clause extension = Ext_C | |||
| enum clause extension = Ext_B | |||
| // Vector Operations | |||
| enum clause extension = Ext_V | |||
| enum clause extension = Ext_Zvkned | |||
There was a problem hiding this comment.
Missing comment with long form name of the extension. This should also be moved down to be with the rest of the Z* extensions in a new Zv* section.
Implements the Zvkned (NIST Suite: Vector AES Block Cipher) extension, as of version Release 1.0.0.
The following instructions are included:
All instructions were tested with VLEN=128 and results were compared with QEMU results of each instruction.
Note
This PR was originally developed by @charmitro , and now the Vector AES Block Cipher has been released.