diff --git a/Makefile.old b/Makefile.old index 270ebae31..c81d521b8 100644 --- a/Makefile.old +++ b/Makefile.old @@ -68,6 +68,8 @@ SAIL_DEFAULT_INST += riscv_insts_vext_fp_red.sail SAIL_DEFAULT_INST += riscv_insts_zicbom.sail SAIL_DEFAULT_INST += riscv_insts_zicboz.sail +SAIL_DEFAULT_INST += riscv_insts_zvkned.sail + SAIL_SEQ_INST = $(SAIL_DEFAULT_INST) riscv_jalr_seq.sail SAIL_RMEM_INST = $(SAIL_DEFAULT_INST) riscv_jalr_rmem.sail riscv_insts_rmem.sail diff --git a/model/CMakeLists.txt b/model/CMakeLists.txt index 15842b420..398a9295f 100644 --- a/model/CMakeLists.txt +++ b/model/CMakeLists.txt @@ -76,6 +76,7 @@ foreach (xlen IN ITEMS 32 64) "riscv_insts_zbkx.sail" "riscv_insts_zicond.sail" ${vext_srcs} + "riscv_insts_zvkned.sail" "riscv_insts_zicbom.sail" "riscv_insts_zicboz.sail" ) @@ -166,6 +167,7 @@ foreach (xlen IN ITEMS 32 64) ${sail_vm_srcs} # Shared/common code for the cryptography extension. "riscv_types_kext.sail" + "riscv_types_zvk.sail" ) if (variant STREQUAL "rvfi") diff --git a/model/riscv_extensions.sail b/model/riscv_extensions.sail index 8b5bf2bd8..56782d55a 100644 --- a/model/riscv_extensions.sail +++ b/model/riscv_extensions.sail @@ -100,6 +100,9 @@ enum clause extension = Ext_Zksed // Scalar & Entropy Source Instructions: ShangMi Suite: SM3 Hash Cipher Instructions enum clause extension = Ext_Zksh +// Vector Instructions: NIST Suite: Vector AES Block Cipher +enum clause extension = Ext_Zvkned + // Floating-Point in Integer Registers (half precision) enum clause extension = Ext_Zhinx diff --git a/model/riscv_insts_zvkned.sail b/model/riscv_insts_zvkned.sail new file mode 100644 index 000000000..6b0a02ced --- /dev/null +++ b/model/riscv_insts_zvkned.sail @@ -0,0 +1,413 @@ +/*=======================================================================================*/ +/* This Sail RISC-V architecture model, comprising all files and */ +/* directories except where otherwise noted is subject the BSD */ +/* two-clause license in the LICENSE file. */ +/* */ +/* SPDX-License-Identifier: BSD-2-Clause */ +/*=======================================================================================*/ +/* + * Vector Cryptography Extension - NIST Suite: Vector AES Block Cipher + * ---------------------------------------------------------------------- + */ + +function clause extensionEnabled(Ext_Zvkned) = true + +val get_velem : forall 'n 'm 'p, 'n > 0 & 'm > 0 & 'p >= 0 & 4 * 'p + 3 < 'n . (vector('n, bits('m)), int('p)) -> bits(4 * 'm) +function get_velem(v, i) = v[4 * i + 3] @ v[4 * i + 2] @ v[4 * i + 1] @ v[4 * i] + +val aes_rotword : bits(32) -> bits(32) +function aes_rotword(x) = x[ 7.. 0] @ x[31..24] @ x[23..16] @ x[15.. 8] + +val zvk_check_elements : (int, int, int, int) -> bool +function zvk_check_elements(VLEN, num_elem, LMUL, SEW) = { + ((unsigned(vl)%num_elem) != 0) | ((unsigned(vstart)%num_elem) != 0) | (LMUL*VLEN) < (num_elem*SEW) +} + +val vv_or_vs_index : forall 'n , 0 <= 'n . (suffix_kind , int('n)) -> range(0, 'n) +function vv_or_vs_index(suffix, i) = { + match suffix { + Vector_Vector => i, + Vector_Scalar => 0, + } +} + +mapping vv_or_vs : suffix_kind <-> bits(6) = { + Vector_Vector <-> 0b101000, + Vector_Scalar <-> 0b101001, +} + +mapping vv_or_vs_mnemonic : suffix_kind <-> string = { + Vector_Vector <-> "vv", + Vector_Scalar <-> "vs", +} + +/* VAESEF.[VV, VS] */ + +union clause ast = RISCV_VAESEF : (regidx, regidx, suffix_kind) + +mapping clause encdec = RISCV_VAESEF(vs2, vd, suffix) if extensionEnabled(Ext_Zvkned) + <-> vv_or_vs(suffix) @ 0b1 @ vs2 @ 0b00011 @ 0b010 @ vd @ 0b1110111 if extensionEnabled(Ext_Zvkned) + +mapping clause assembly = RISCV_VAESEF(vs2, vd, suffix) + <-> "vaesef." ^ vv_or_vs_mnemonic(suffix) ^ spc() ^ vreg_name(vd) + ^ spc() ^ vreg_name(vs2) + +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 num_elem = get_num_elem(LMUL_pow, SEW); + + if (not(zvk_check_elements(VLEN, num_elem, LMUL, SEW))) + then { + handle_illegal(); + RETIRE_FAIL + } else { + let 'n = num_elem; + let 'm = SEW; + assert('m == 32); + + let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); + let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); + + let eg_len = (unsigned(vl) / 'n); + let eg_start = (unsigned(vstart) / 'n); + + foreach (i from eg_start to (eg_len - 1)) { + assert(0 <= ((i * 4) + 3) & ((i * 4) + 3) < 'n); + + let vd_state = get_velem(vd_val, i); + let vs2_key = get_velem(vs2_val, vv_or_vs_index(suffix, i)); + let sb = aes_subbytes_fwd(vd_state); + let sr = aes_shift_rows_fwd(sb); + let ark = sr ^ vs2_key; + + write_single_element(128, i, vd, ark); + }; + + set_vstart(zeros()); + RETIRE_SUCCESS + } +} + +/* VAESEM.[VV, VS] */ + +union clause ast = RISCV_VAESEM : (regidx, regidx, suffix_kind) + +mapping clause encdec = RISCV_VAESEM(vs2, vd, suffix) if extensionEnabled(Ext_Zvkned) + <-> vv_or_vs(suffix) @ 0b1 @ vs2 @ 0b00010 @ 0b010 @ vd @ 0b1110111 if extensionEnabled(Ext_Zvkned) + +mapping clause assembly = RISCV_VAESEM(vs2, vd, suffix) + <-> "vaesem." ^ vv_or_vs_mnemonic(suffix) ^ spc() ^ vreg_name(vd) + ^ sep() ^ vreg_name(vs2) + +function clause execute (RISCV_VAESEM(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 num_elem = get_num_elem(LMUL_pow, SEW); + + if (not(zvk_check_elements(VLEN, num_elem, LMUL, SEW))) + then { + handle_illegal(); + RETIRE_FAIL + } else { + let 'n = num_elem; + let 'm = SEW; + assert('m == 32); + + let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); + let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); + + let eg_len = (unsigned(vl) / 'n); + let eg_start = (unsigned(vstart) / 'n); + + foreach (i from eg_start to (eg_len - 1)) { + assert(0 <= ((i * 4) + 3) & ((i * 4) + 3) < 'n); + + let vd_state = get_velem(vd_val, i); + let vs2_key = get_velem(vs2_val, vv_or_vs_index(suffix, i)); + let sb : bits(128) = aes_subbytes_fwd(vd_state); + let sr : bits(128) = aes_shift_rows_fwd(sb); + let mix : bits(128) = aes_mixcolumns_fwd(sr); + let ark : bits(128) = mix ^ vs2_key; + + write_single_element(128, i, vd, ark); + }; + + set_vstart(zeros()); + RETIRE_SUCCESS + } +} + +/* VAESDF.VV */ + +union clause ast = RISCV_VAESDF : (regidx, regidx, suffix_kind) + +mapping clause encdec = RISCV_VAESDF(vs2, vd, suffix) if extensionEnabled(Ext_Zvkned) + <-> vv_or_vs(suffix) @ 0b1 @ vs2 @ 0b00001 @ 0b010 @ vd @ 0b1110111 if extensionEnabled(Ext_Zvkned) + +mapping clause assembly = RISCV_VAESDF(vs2, vd, suffix) + <-> "vaesdf." ^ vv_or_vs_mnemonic(suffix) ^ sep() ^ vreg_name(vd) + ^ sep() ^ vreg_name(vs2) + +function clause execute (RISCV_VAESDF(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 num_elem = get_num_elem(LMUL_pow, SEW); + + if (not(zvk_check_elements(VLEN, num_elem, LMUL, SEW))) + then { + handle_illegal(); + RETIRE_FAIL + } else { + let 'n = num_elem; + let 'm = SEW; + assert('m == 32); + + let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); + let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); + + let eg_len = (unsigned(vl) / 'n); + let eg_start = (unsigned(vstart) / 'n); + + foreach (i from eg_start to (eg_len - 1)) { + assert(0 <= ((i * 4) + 3) & ((i * 4) + 3) < 'n); + + let vd_state = get_velem(vd_val, i); + let vs2_key = get_velem(vs2_val, vv_or_vs_index(suffix, i)); + let sr : bits(128) = aes_shift_rows_inv(vd_state); + let sb : bits(128) = aes_subbytes_inv(sr); + let ark : bits(128) = sb ^ vs2_key; + + write_single_element(128, i, vd, ark); + }; + + set_vstart(zeros()); + RETIRE_SUCCESS + } +} + +/* VAESDM.VV */ + +union clause ast = RISCV_VAESDM : (regidx, regidx, suffix_kind) + +mapping clause encdec = RISCV_VAESDM(vs2, vd, suffix) if extensionEnabled(Ext_Zvkned) + <-> vv_or_vs(suffix) @ 0b1 @ vs2 @ 0b00000 @ 0b010 @ vd @ 0b1110111 if extensionEnabled(Ext_Zvkned) + +mapping clause assembly = RISCV_VAESDM(vs2, vd, suffix) + <-> "vaesdm." ^ vv_or_vs_mnemonic(suffix) ^ spc() ^ vreg_name(vd) + ^ sep() ^ vreg_name(vs2) + +function clause execute (RISCV_VAESDM(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 num_elem = get_num_elem(LMUL_pow, SEW); + + if (not(zvk_check_elements(VLEN, num_elem, LMUL, SEW))) + then { + handle_illegal(); + RETIRE_FAIL + } else { + let 'n = num_elem; + let 'm = SEW; + assert('m == 32); + + let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); + let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); + + let eg_len = (unsigned(vl) / 'n); + let eg_start = (unsigned(vstart) / 'n); + + foreach (i from eg_start to (eg_len - 1)) { + assert(0 <= ((i * 4) + 3) & ((i * 4) + 3) < 'n); + + let vd_state = get_velem(vd_val, i); + let vs2_key = get_velem(vs2_val, vv_or_vs_index(suffix, i)); + let sr : bits(128) = aes_shift_rows_inv(vd_state); + let sb : bits(128) = aes_subbytes_inv(sr); + let ark : bits(128) = sb ^ vs2_key; + let mix : bits(128) = aes_mixcolumns_inv(ark); + + write_single_element(128, i, vd, mix); + }; + + set_vstart(zeros()); + RETIRE_SUCCESS + } +} + +/* VAESKF1.VI */ + +union clause ast = RISCV_VAESKF1_VI : (regidx, regidx, regidx) + +mapping clause encdec = RISCV_VAESKF1_VI(vs2, rnd, vd) if extensionEnabled(Ext_Zvkned) + <-> 0b1000101 @ vs2 @ rnd @ 0b010 @ vd @ 0b1110111 if extensionEnabled(Ext_Zvkned) + +mapping clause assembly = RISCV_VAESKF1_VI(vs2, rnd, vd) + <-> "vaeskf1.vi" ^ sep() ^ vreg_name(vd) + ^ sep() ^ vreg_name(vs2) + ^ sep() ^ reg_name(rnd) + +function clause execute (RISCV_VAESKF1_VI(vs2, rnd, vd)) = { + let SEW = get_sew(); + let LMUL_pow = get_lmul_pow(); + let LMUL = if LMUL_pow < 0 then 0 else LMUL_pow; + let num_elem = get_num_elem(LMUL_pow, SEW); + + if (not(zvk_check_elements(VLEN, num_elem, LMUL, SEW))) + then { + handle_illegal(); + RETIRE_FAIL + } else { + let 'n = num_elem; + let 'm = SEW; + assert('m == 32); + + var rnd_val : bits(5) = rnd; + 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); + + if (unsigned(rnd_val[3..0]) > 10) | (unsigned(rnd_val[3..0]) == 0) + then rnd_val[3] = not_bit(rnd_val[3]); + + let r : bits(4) = rnd_val[3..0] - 1; + + var w : bits(128) = zeros(); + + let eg_len = (unsigned(vl) / 'n); + let eg_start = (unsigned(vstart) / 'n); + + foreach (i from eg_start to (eg_len - 1)) { + assert(0 <= ((i * 4) + 3) & ((i * 4) + 3) < 'n); + let current_round_key = get_velem(vs2_val, i); + + w[31..0] = aes_subword_fwd(aes_rotword(current_round_key[127..96])) + ^ aes_decode_rcon(r) + ^ current_round_key[31..0]; + w[63..32] = w[31..0] ^ current_round_key[63..32]; + w[95..64] = w[63..32] ^ current_round_key[95..64]; + w[127..96] = w[95..64] ^ current_round_key[127..96]; + + write_single_element(128, i, vd, w); + }; + + set_vstart(zeros()); + RETIRE_SUCCESS + } +} + +/* VAESKF2.VI */ + +union clause ast = RISCV_VAESKF2_VI : (regidx, regidx, regidx) + +mapping clause encdec = RISCV_VAESKF2_VI(vs2, rnd, vd) if extensionEnabled(Ext_Zvkned) + <-> 0b1010101 @ vs2 @ rnd @ 0b010 @ vd @ 0b1110111 if extensionEnabled(Ext_Zvkned) + +mapping clause assembly = RISCV_VAESKF2_VI(vs2, rnd, vd) + <-> "vaeskf2.vi" ^ sep() ^ vreg_name(vd) + ^ sep() ^ vreg_name(vs2) + ^ sep() ^ reg_name(rnd) + +function clause execute (RISCV_VAESKF2_VI(vs2, rnd, vd)) = { + let SEW = get_sew(); + let LMUL_pow = get_lmul_pow(); + let LMUL = if LMUL_pow < 0 then 0 else LMUL_pow; + let num_elem = get_num_elem(LMUL_pow, SEW); + + if (not(zvk_check_elements(VLEN, num_elem, LMUL, SEW))) + then { + handle_illegal(); + RETIRE_FAIL + } else { + let 'n = num_elem; + let 'm = SEW; + assert('m == 32); + + var rnd_val : bits(4) = rnd[3..0]; + let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); + let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); + + if (unsigned(rnd_val) < 2) | (unsigned(rnd_val) > 14) + then rnd_val[3] = not_bit(rnd_val[3]); + + var w : bits(128) = zeros(); + + let eg_len = (unsigned(vl) / 'n); + let eg_start = (unsigned(vstart) / 'n); + + foreach (i from eg_start to (eg_len - 1)) { + assert(0 <= ((i * 4) + 3) & ((i * 4) + 3) < 'n); + + let current_round_key = get_velem(vs2_val, i); + + let round_key_b = get_velem(vd_val, i); + + w[31..0] = if (rnd_val[0] == bitone) + then + aes_subword_fwd(current_round_key[127..96]) ^ round_key_b[31..0] + else + aes_subword_fwd(aes_rotword(current_round_key[127..96])) + ^ aes_decode_rcon((rnd_val >> 1) - 1) + ^ round_key_b[31..0]; + + w[63..32] = w[31..0] ^ round_key_b[63..32]; + w[95..64] = w[63..32] ^ round_key_b[95..64]; + w[127..96] = w[95..64] ^ round_key_b[127..96]; + + write_single_element(128, i, vd, w); + }; + + set_vstart(zeros()); + RETIRE_SUCCESS + } +} + +/* VAESZ.VS */ + +union clause ast = RISCV_VAESZ_VS : (regidx, regidx) + +mapping clause encdec = RISCV_VAESZ_VS(vs2, vd) if extensionEnabled(Ext_Zvkned) + <-> 0b1010011 @ vs2 @ 0b00111 @ 0b010 @ vd @ 0b1110111 if extensionEnabled(Ext_Zvkned) + +mapping clause assembly = RISCV_VAESZ_VS(vs2, vd) + <-> "vaesz.vs" ^ sep() ^ vreg_name(vd) + ^ sep() ^ vreg_name(vs2) + +function clause execute (RISCV_VAESZ_VS(vs2, vd)) = { + let SEW = get_sew(); + let LMUL_pow = get_lmul_pow(); + let LMUL = if LMUL_pow < 0 then 0 else LMUL_pow; + let num_elem = get_num_elem(LMUL_pow, SEW); + + if (not(zvk_check_elements(VLEN, num_elem, LMUL, SEW))) + then { + handle_illegal(); + RETIRE_FAIL + } else { + let 'n = num_elem; + let 'm = SEW; + 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); + + let eg_len = (unsigned(vl) / 'n); + let eg_start = (unsigned(vstart) / 'n); + + foreach (i from eg_start to (eg_len - 1)) { + assert(0 <= ((i * 4) + 3) & ((i * 4) + 3) < 'n); + + let vd_state = get_velem(vd_val, i); + let vs2_key = get_velem(vs2_val, 0); + let ark : bits(128) = vd_state ^ vs2_key; + + write_single_element(128, i, vd, ark); + }; + + set_vstart(zeros()); + RETIRE_SUCCESS + } +} diff --git a/model/riscv_types_zvk.sail b/model/riscv_types_zvk.sail new file mode 100644 index 000000000..7f832c134 --- /dev/null +++ b/model/riscv_types_zvk.sail @@ -0,0 +1,16 @@ +/*=======================================================================================*/ +/* This Sail RISC-V architecture model, comprising all files and */ +/* directories except where otherwise noted is subject the BSD */ +/* two-clause license in the LICENSE file. */ +/* */ +/* SPDX-License-Identifier: BSD-2-Clause */ +/*=======================================================================================*/ + +/* + * Types used in supporting extensions for page-table walks. + */ + +enum suffix_kind = { + Vector_Vector, + Vector_Scalar, +}