From bb87f5a0a7a910ae2712174c51f8d8b046019a38 Mon Sep 17 00:00:00 2001 From: Linda Njau Date: Tue, 2 Jul 2024 12:48:27 +0300 Subject: [PATCH] Add names for AES instructions --- model/riscv_insts_zkn.sail | 129 +++++++++++++++++++++++++++++-------- 1 file changed, 101 insertions(+), 28 deletions(-) diff --git a/model/riscv_insts_zkn.sail b/model/riscv_insts_zkn.sail index 12623430d..8593c939d 100644 --- a/model/riscv_insts_zkn.sail +++ b/model/riscv_insts_zkn.sail @@ -1,9 +1,71 @@ /*=======================================================================================*/ +/* RISCV Sail Model */ +/* */ /* 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. */ +/* directories except for the snapshots of the Lem and Sail libraries */ +/* in the prover_snapshots directory (which include copies of their */ +/* licences), is subject to the BSD two-clause licence below. */ +/* */ +/* Copyright (c) 2017-2023 */ +/* Prashanth Mundkur */ +/* Rishiyur S. Nikhil and Bluespec, Inc. */ +/* Jon French */ +/* Brian Campbell */ +/* Robert Norton-Wright */ +/* Alasdair Armstrong */ +/* Thomas Bauereiss */ +/* Shaked Flur */ +/* Christopher Pulte */ +/* Peter Sewell */ +/* Alexander Richardson */ +/* Hesham Almatary */ +/* Jessica Clarke */ +/* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ +/* Peter Rugg */ +/* Aril Computer Corp., for contributions by Scott Johnson */ +/* Philipp Tomsich */ +/* VRULL GmbH, for contributions by its employees */ +/* */ +/* All rights reserved. */ +/* */ +/* This software was developed by the above within the Rigorous */ +/* Engineering of Mainstream Systems (REMS) project, partly funded by */ +/* EPSRC grant EP/K008528/1, at the Universities of Cambridge and */ +/* Edinburgh. */ +/* */ +/* This software was developed by SRI International and the University of */ +/* Cambridge Computer Laboratory (Department of Computer Science and */ +/* Technology) under DARPA/AFRL contract FA8650-18-C-7809 ("CIFV"), and */ +/* under DARPA contract HR0011-18-C-0016 ("ECATS") as part of the DARPA */ +/* SSITH research programme. */ +/* */ +/* This project has received funding from the European Research Council */ +/* (ERC) under the European Union’s Horizon 2020 research and innovation */ +/* programme (grant agreement 789108, ELVER). */ +/* */ +/* */ +/* Redistribution and use in source and binary forms, with or without */ +/* modification, are permitted provided that the following conditions */ +/* are met: */ +/* 1. Redistributions of source code must retain the above copyright */ +/* notice, this list of conditions and the following disclaimer. */ +/* 2. Redistributions in binary form must reproduce the above copyright */ +/* notice, this list of conditions and the following disclaimer in */ +/* the documentation and/or other materials provided with the */ +/* distribution. */ /* */ -/* SPDX-License-Identifier: BSD-2-Clause */ +/* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' */ +/* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED */ +/* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A */ +/* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR */ +/* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, */ +/* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT */ +/* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF */ +/* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND */ +/* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, */ +/* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT */ +/* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF */ +/* SUCH DAMAGE. */ /*=======================================================================================*/ /* @@ -21,16 +83,16 @@ $[name "SHA2-256 Sum1"] union clause ast = SHA256SUM1 : (regidx, regidx) mapping clause encdec = SHA256SUM0 (rs1, rd) if extension("Zknh") - <-> 0b00 @ 0b01000 @ 0b00000 @ rs1 @ 0b001 @ rd @ 0b0010011 if extension("Zknh") + <-> 0b00 @ 0b01000 @ 0b00000 @ rs1 @ 0b001 @ rd @ 0b0010011 mapping clause encdec = SHA256SUM1 (rs1, rd) if extension("Zknh") - <-> 0b00 @ 0b01000 @ 0b00001 @ rs1 @ 0b001 @ rd @ 0b0010011 if extension("Zknh") + <-> 0b00 @ 0b01000 @ 0b00001 @ rs1 @ 0b001 @ rd @ 0b0010011 mapping clause encdec = SHA256SIG0 (rs1, rd) if extension("Zknh") - <-> 0b00 @ 0b01000 @ 0b00010 @ rs1 @ 0b001 @ rd @ 0b0010011 if extension("Zknh") + <-> 0b00 @ 0b01000 @ 0b00010 @ rs1 @ 0b001 @ rd @ 0b0010011 mapping clause encdec = SHA256SIG1 (rs1, rd) if extension("Zknh") - <-> 0b00 @ 0b01000 @ 0b00011 @ rs1 @ 0b001 @ rd @ 0b0010011 if extension("Zknh") + <-> 0b00 @ 0b01000 @ 0b00011 @ rs1 @ 0b001 @ rd @ 0b0010011 mapping clause assembly = SHA256SIG0 (rs1, rd) <-> "sha256sig0" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) @@ -77,10 +139,11 @@ function clause execute (SHA256SUM1(rs1, rd)) = { * ---------------------------------------------------------------------- */ +$[name "AES middle round encrypt (RV32)"] union clause ast = AES32ESMI : (bits(2), regidx, regidx, regidx) mapping clause encdec = AES32ESMI (bs, rs2, rs1, rd) if extension("Zkne") & sizeof(xlen) == 32 - <-> bs @ 0b10011 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if extension("Zkne") & sizeof(xlen) == 32 + <-> bs @ 0b10011 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 mapping clause assembly = AES32ESMI (bs, rs2, rs1, rd) <-> "aes32esmi" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2) ^ sep() ^ hex_bits_2(bs) @@ -95,10 +158,11 @@ function clause execute (AES32ESMI (bs, rs2, rs1, rd)) = { RETIRE_SUCCESS } +$[name "AES final round encrypt (RV32)"] union clause ast = AES32ESI : (bits(2), regidx, regidx, regidx) mapping clause encdec = AES32ESI (bs, rs2, rs1, rd) if extension("Zkne") & sizeof(xlen) == 32 - <-> bs @ 0b10001 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if extension("Zkne") & sizeof(xlen) == 32 + <-> bs @ 0b10001 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 mapping clause assembly = AES32ESI (bs, rs2, rs1, rd) <-> "aes32esi" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2) ^ sep() ^ hex_bits_2(bs) @@ -117,10 +181,11 @@ function clause execute (AES32ESI (bs, rs2, rs1, rd)) = { * ---------------------------------------------------------------------- */ +$[name "AES middle round decrypt (RV32)"] union clause ast = AES32DSMI : (bits(2), regidx, regidx, regidx) mapping clause encdec = AES32DSMI (bs, rs2, rs1, rd) if extension("Zknd") & sizeof(xlen) == 32 - <-> bs @ 0b10111 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if extension("Zknd") & sizeof(xlen) == 32 + <-> bs @ 0b10111 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 mapping clause assembly = AES32DSMI (bs, rs2, rs1, rd) <-> "aes32dsmi" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2) ^ sep() ^ hex_bits_2(bs) @@ -135,10 +200,11 @@ function clause execute (AES32DSMI (bs, rs2, rs1, rd)) = { RETIRE_SUCCESS } +$[name " AES final round decrypt (RV32)"] union clause ast = AES32DSI : (bits(2), regidx, regidx, regidx) mapping clause encdec = AES32DSI (bs, rs2, rs1, rd) if extension("Zknd") & sizeof(xlen) == 32 - <-> bs @ 0b10101 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if extension("Zknd") & sizeof(xlen) == 32 + <-> bs @ 0b10101 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 mapping clause assembly = AES32DSI (bs, rs2, rs1, rd) <-> "aes32dsi" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2) ^ sep() ^ hex_bits_2(bs) @@ -171,22 +237,22 @@ $[name "SHA2-512 Sum1 (RV32)"] union clause ast = SHA512SUM1R : (regidx, regidx, regidx) mapping clause encdec = SHA512SUM0R (rs2, rs1, rd) if extension("Zknh") & sizeof(xlen) == 32 - <-> 0b01 @ 0b01000 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if extension("Zknh") & sizeof(xlen) == 32 + <-> 0b01 @ 0b01000 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 mapping clause encdec = SHA512SUM1R (rs2, rs1, rd) if extension("Zknh") & sizeof(xlen) == 32 - <-> 0b01 @ 0b01001 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if extension("Zknh") & sizeof(xlen) == 32 + <-> 0b01 @ 0b01001 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 mapping clause encdec = SHA512SIG0L (rs2, rs1, rd) if extension("Zknh") & sizeof(xlen) == 32 - <-> 0b01 @ 0b01010 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if extension("Zknh") & sizeof(xlen) == 32 + <-> 0b01 @ 0b01010 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 mapping clause encdec = SHA512SIG0H (rs2, rs1, rd) if extension("Zknh") & sizeof(xlen) == 32 - <-> 0b01 @ 0b01110 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if extension("Zknh") & sizeof(xlen) == 32 + <-> 0b01 @ 0b01110 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 mapping clause encdec = SHA512SIG1L (rs2, rs1, rd) if extension("Zknh") & sizeof(xlen) == 32 - <-> 0b01 @ 0b01011 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if extension("Zknh") & sizeof(xlen) == 32 + <-> 0b01 @ 0b01011 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 mapping clause encdec = SHA512SIG1H (rs2, rs1, rd) if extension("Zknh") & sizeof(xlen) == 32 - <-> 0b01 @ 0b01111 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if extension("Zknh") & sizeof(xlen) == 32 + <-> 0b01 @ 0b01111 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 mapping clause assembly = SHA512SIG0L (rs2, rs1, rd) <-> "sha512sig0l" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2) @@ -247,34 +313,41 @@ function clause execute (SHA512SUM1R(rs2, rs1, rd)) = { * ---------------------------------------------------------------------- */ +$[name "AES Key Schedule Instruction 1 (RV64)"] union clause ast = AES64KS1I : (bits(4), regidx, regidx) +$[name "AES Key Schedule Instruction 2 (RV64)"] union clause ast = AES64KS2 : (regidx, regidx, regidx) +$[name "AES Decrypt KeySchedule MixColumns (RV64)"] union clause ast = AES64IM : (regidx, regidx) +$[name "AES encrypt middle round instruction (RV64)"] union clause ast = AES64ESM : (regidx, regidx, regidx) +$[name "AES encrypt final round instruction (RV64)"] union clause ast = AES64ES : (regidx, regidx, regidx) +$[name "AES decrypt middle round (RV64)"] union clause ast = AES64DSM : (regidx, regidx, regidx) +$[name "AES decrypt final round (RV64)"] union clause ast = AES64DS : (regidx, regidx, regidx) mapping clause encdec = AES64KS1I (rnum, rs1, rd) if (extension("Zkne") | extension("Zknd")) & (sizeof(xlen) == 64) & (rnum <_u 0xB) - <-> 0b00 @ 0b11000 @ 0b1 @ rnum @ rs1 @ 0b001 @ rd @ 0b0010011 if (extension("Zkne") | extension("Zknd")) & (sizeof(xlen) == 64) & (rnum <_u 0xB) + <-> 0b00 @ 0b11000 @ 0b1 @ rnum @ rs1 @ 0b001 @ rd @ 0b0010011 mapping clause encdec = AES64IM (rs1, rd) if extension("Zknd") & sizeof(xlen) == 64 - <-> 0b00 @ 0b11000 @ 0b00000 @ rs1 @ 0b001 @ rd @ 0b0010011 if extension("Zknd") & sizeof(xlen) == 64 + <-> 0b00 @ 0b11000 @ 0b00000 @ rs1 @ 0b001 @ rd @ 0b0010011 mapping clause encdec = AES64KS2 (rs2, rs1, rd) if (extension("Zkne") | extension("Zknd")) & sizeof(xlen) == 64 - <-> 0b01 @ 0b11111 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if (extension("Zkne") | extension("Zknd")) & sizeof(xlen) == 64 + <-> 0b01 @ 0b11111 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 mapping clause encdec = AES64ESM (rs2, rs1, rd) if extension("Zkne") & sizeof(xlen) == 64 - <-> 0b00 @ 0b11011 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if extension("Zkne") & sizeof(xlen) == 64 + <-> 0b00 @ 0b11011 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 mapping clause encdec = AES64ES (rs2, rs1, rd) if extension("Zkne") & sizeof(xlen) == 64 - <-> 0b00 @ 0b11001 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if extension("Zkne") & sizeof(xlen) == 64 + <-> 0b00 @ 0b11001 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 mapping clause encdec = AES64DSM (rs2, rs1, rd) if extension("Zknd") & sizeof(xlen) == 64 - <-> 0b00 @ 0b11111 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if extension("Zknd") & sizeof(xlen) == 64 + <-> 0b00 @ 0b11111 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 mapping clause encdec = AES64DS (rs2, rs1, rd) if extension("Zknd") & sizeof(xlen) == 64 - <-> 0b00 @ 0b11101 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if extension("Zknd") & sizeof(xlen) == 64 + <-> 0b00 @ 0b11101 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 mapping clause assembly = AES64KS1I (rnum, rs1, rd) <-> "aes64ks1i" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ hex_bits_4(rnum) @@ -375,16 +448,16 @@ $[name "SHA2-512 Sum1 (RV64)"] union clause ast = SHA512SUM1 : (regidx, regidx) mapping clause encdec = SHA512SUM0 (rs1, rd) if extension("Zknh") & sizeof(xlen) == 64 - <-> 0b00 @ 0b01000 @ 0b00100 @ rs1 @ 0b001 @ rd @ 0b0010011 if extension("Zknh") & sizeof(xlen) == 64 + <-> 0b00 @ 0b01000 @ 0b00100 @ rs1 @ 0b001 @ rd @ 0b0010011 mapping clause encdec = SHA512SUM1 (rs1, rd) if extension("Zknh") & sizeof(xlen) == 64 - <-> 0b00 @ 0b01000 @ 0b00101 @ rs1 @ 0b001 @ rd @ 0b0010011 if extension("Zknh") & sizeof(xlen) == 64 + <-> 0b00 @ 0b01000 @ 0b00101 @ rs1 @ 0b001 @ rd @ 0b0010011 mapping clause encdec = SHA512SIG0 (rs1, rd) if extension("Zknh") & sizeof(xlen) == 64 - <-> 0b00 @ 0b01000 @ 0b00110 @ rs1 @ 0b001 @ rd @ 0b0010011 if extension("Zknh") & sizeof(xlen) == 64 + <-> 0b00 @ 0b01000 @ 0b00110 @ rs1 @ 0b001 @ rd @ 0b0010011 mapping clause encdec = SHA512SIG1 (rs1, rd) if extension("Zknh") & sizeof(xlen) == 64 - <-> 0b00 @ 0b01000 @ 0b00111 @ rs1 @ 0b001 @ rd @ 0b0010011 if extension("Zknh") & sizeof(xlen) == 64 + <-> 0b00 @ 0b01000 @ 0b00111 @ rs1 @ 0b001 @ rd @ 0b0010011 mapping clause assembly = SHA512SIG0 (rs1, rd) <-> "sha512sig0" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1)