diff --git a/Makefile b/Makefile index 255224125..a8277b9dc 100644 --- a/Makefile +++ b/Makefile @@ -45,6 +45,9 @@ SAIL_DEFAULT_INST += riscv_insts_zbkx.sail SAIL_DEFAULT_INST += riscv_insts_zicond.sail +SAIL_DEFAULT_INST += riscv_zicfilp_regs.sail # Zicfilp state +SAIL_DEFAULT_INST += riscv_insts_zicfilp.sail # Zicfilp instructions + SAIL_DEFAULT_INST += riscv_insts_vext_utils.sail SAIL_DEFAULT_INST += riscv_insts_vext_vset.sail SAIL_DEFAULT_INST += riscv_insts_vext_arith.sail diff --git a/model/riscv_insts_base.sail b/model/riscv_insts_base.sail index caea73a4b..198be6d79 100644 --- a/model/riscv_insts_base.sail +++ b/model/riscv_insts_base.sail @@ -12,14 +12,22 @@ /* ****************************************************************** */ union clause ast = UTYPE : (bits(20), regidx, uop) +union clause ast = zicfilp_lpad : (bits(20)) mapping encdec_uop : uop <-> bits(7) = { RISCV_LUI <-> 0b0110111, RISCV_AUIPC <-> 0b0010111 } +/* Zicfilp landing pad lpad is auipc x0, imm */ +function is_lpad(op : uop, rd : regidx) -> bool = + haveZicfilp() & rd == zreg & op == RISCV_AUIPC + mapping clause encdec = UTYPE(imm, rd, op) - <-> imm @ rd @ encdec_uop(op) + <-> imm @ rd @ encdec_uop(op) if not(is_lpad(op, rd)) + +mapping clause encdec = zicfilp_lpad(imm) + <-> imm @ 0b00000 @ 0b0010111 function clause execute UTYPE(imm, rd, op) = { let off : xlenbits = sign_extend(imm @ 0x000); @@ -39,6 +47,9 @@ mapping utype_mnemonic : uop <-> string = { mapping clause assembly = UTYPE(imm, rd, op) <-> utype_mnemonic(op) ^ spc() ^ reg_name(rd) ^ sep() ^ hex_bits_20(imm) +mapping clause assembly = zicfilp_lpad(imm) + <-> "lpad" ^ spc() ^ hex_bits_20(imm) + /* ****************************************************************** */ union clause ast = RISCV_JAL : (bits(21), regidx) diff --git a/model/riscv_insts_zicfilp.sail b/model/riscv_insts_zicfilp.sail new file mode 100644 index 000000000..59b9fb2e1 --- /dev/null +++ b/model/riscv_insts_zicfilp.sail @@ -0,0 +1,215 @@ +/*=======================================================================================*/ +/* RISCV Sail Model */ +/* */ +/* This Sail RISC-V architecture model, comprising all files and */ +/* 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 */ +/* Ved Shanbhogue */ +/* */ +/* 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. */ +/* */ +/* 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. */ +/*=======================================================================================*/ + +/* ****************************************************************** */ +/* This file specifies the instructions in the 'Zicfilp' extension. */ +/* ****************************************************************** */ +/* Forward-edge CFI: Landing pads */ +val get_MPELP : (unit) -> elp_state +/* Sail does not yet support H extension - this needs to be updated to + support henvcfg for VS when H extension support is included */ +function zicfilp_xLPE() -> bool = { + /* When S-mode is implemented + * Priv xLPE + * M mseccfg.MLPE + * S/HS menvcfg.LPE + * VS henvcfg.LPE + * U/VU senvcfg.LPE + * When S-mode is not implemented + * Priv xLPE + * M mseccfg.MLPE + * U menvcfg.LPE + */ + if not(haveZicfilp()) + then false + else if cur_privilege == Machine + then mseccfg[MLPE] == 0b1 + else if cur_privilege == Supervisor + then menvcfg[LPE] == 0b1 + else if not(haveSupMode()) + then menvcfg[LPE] == 0b1 + else senvcfg[LPE] == 0b1 +} +/* extension to jalr */ +function zicfilp_update_elp(rs1_reg : regidx) -> unit = { + /* + * An indirect branch using JALR, C.JALR, or C.JR with rs1 as x7 is termed + * a software guarded branch. Such branches do not need to land on a LPAD + * instruction and thus do not set ELP to LP_EXPECTED. JALR/C.JR/C.JALR + * using x1/x5 as source are returns; they do not set ELP to LP_EXPECTED. + * + * is_lp_expected = ( (JALR || C.JR || C.JALR) && + * (rs1 != x1) && (rs1 != x5) && (rs1 != x7) ) ? 1 : 0; + */ + let is_lp_expected : bool = ((rs1_reg != 0b00001) & (rs1_reg != 0b00101) & + (rs1_reg != 0b00111)); + if is_lp_expected == true & zicfilp_xLPE() + then elp = ElpState_to_bits(LP_EXPECTED); + + print("jalr: elp= " ^ BitStr(elp) ^ " is_lp_expected=" ^ BitStr(bool_to_bits(is_lp_expected))); +} +/* AUIPC with rd=x0 is a lpad instruction when zicfilp is active else a no-op */ +function clause execute zicfilp_lpad( lpl ) = { + /* expected label is in x7 bits 31:12 */ + let exp_lbl : bits(20) = x7[31..12]; + + print("lpad:elp= " ^ BitStr(elp) ^ " lpl= " ^ BitStr(lpl) ^ " x7_31_12= " ^ BitStr(exp_lbl)); + + if zicfilp_xLPE() & (elp == ElpState_to_bits(LP_EXPECTED)) then { + if ( (lpl != exp_lbl) & (lpl != 0b00000000000000000000) ) + then { handle_sw_check_exception(LANDING_PAD_FAULT); RETIRE_FAIL } + else { elp = ElpState_to_bits(NO_LP_EXPECTED); RETIRE_SUCCESS }; + } else { + RETIRE_SUCCESS + } +} +/* trap delivery extension */ +function zicfilp_preserve_elp(del_priv : Privilege) -> unit = { + /* When a trap is taken into privilege mode x, the xPELP is set + to ELP and ELP is set to NO_LP_EXPECTED. */ + /* Sail does not have support for Debug mode - this needs to be + updated when Debug mode support is added */ + if haveZicfilp() then { + match (del_priv, sizeof(xlen)) { + (Machine, 32 ) => {mstatush = update_MPELP(mstatush, elp)}, + (Machine, _ ) => {mstatus = update_mstatus_MPELP(mstatus, elp)}, + ( _, _ ) => {mstatus = update_SPELP(mstatus, elp)}, + }; + elp = ElpState_to_bits(NO_LP_EXPECTED); + } +} +/* extension to MRET */ +function zicfilp_set_elp_to_mpelp() -> unit = { + /* An MRET or SRET instruction is used to return from a trap in M-mode + * or S-mode, respectively. When executing an xRET instruction, if xPP + * holds the value y, then ELP is set to the value of xPELP if yLPE is + * 1; otherwise, it is set to NO_LP_EXPECTED; xPELP is set to + * NO_LP_EXPECTED. + */ + if haveZicfilp() then { + match zicfilp_xLPE() { + true => { elp = get_MPELP() }, + false => { elp = ElpState_to_bits(NO_LP_EXPECTED) } + }; + match (sizeof(xlen)) { + 32 => {mstatush = update_MPELP(mstatush, ElpState_to_bits(NO_LP_EXPECTED))}, + _ => {mstatus = update_mstatus_MPELP(mstatus, ElpState_to_bits(NO_LP_EXPECTED))} + }; + } +} +/* extension to SRET */ +function zicfilp_set_elp_to_spelp() -> unit = { + /* An MRET or SRET instruction is used to return from a trap in M-mode + * or S-mode, respectively. When executing an xRET instruction, if xPP + * holds the value y, then ELP is set to the value of xPELP if yLPE is + * 1; otherwise, it is set to NO_LP_EXPECTED; xPELP is set to + * NO_LP_EXPECTED. + */ + if haveZicfilp() then { + match zicfilp_xLPE() { + true => { elp = mstatus.SPELP() }, + false => { elp = ElpState_to_bits(NO_LP_EXPECTED) } + }; + mstatus = update_SPELP(mstatus, ElpState_to_bits(NO_LP_EXPECTED)); + } +} +/* Check if fetch violates ELP */ +function zicfilp_is_elp_violated() -> bool = { + /* landing pad is a AUIPC with rd=x0 */ + /* When ELP is set to LP_EXPECTED, if the next instruction in + * the instruction stream is not 4-byte aligned, or is not LPAD, or + * if the landing pad label encoded in LPAD is not zero and does not + * match the expected landing pad label in bits 31:12 of the x7 + * register, then a software-check exception (cause=18) with xtval + * set to "landing pad fault (code=2)" is raised else the ELP is + * updated to NO_LP_EXPECTED. The label check is performed in + * riscv_insts_zicfilp:zicfilp_lpad + */ + if not(zicfilp_xLPE()) + then false + else if elp != ElpState_to_bits(LP_EXPECTED) + then false + else if ( (PC[1 .. 0] != 0b00) | (instbits[6..0] != 0b0010111) | (instbits[11..7] != 0b00000) ) + then true + else false +} + +/* helper to update MPELP in mstatus */ +function update_mstatus_MPELP(o : Mstatus, e : elp_state) -> Mstatus = + if sizeof(xlen) == 64 + then Mk_Mstatus([o.bits() with 41 .. 41 = e]) + else o + +/* helpers to get MPELP from mstatus/mstatush */ +function get_MPELP() -> elp_state = + if sizeof(xlen) == 64 + then mstatus.bits()[41..41] + else mstatush.MPELP() diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail index 78983a742..48089a946 100644 --- a/model/riscv_sys_control.sail +++ b/model/riscv_sys_control.sail @@ -496,6 +496,7 @@ function handle_exception(e: ExceptionType) -> unit = { function handle_interrupt(i : InterruptType, del_priv : Privilege) -> unit = set_next_pc(trap_handler(del_priv, true, interruptType_to_bits(i), PC, None(), None())) +val init_zicfilp_regs : unit -> unit /* state state initialization */ function init_sys() -> unit = { @@ -574,6 +575,8 @@ function init_sys() -> unit = { // PMP's L and A fields are set to 0 on reset. init_pmp(); + init_zicfilp_regs(); + // log compatibility with spike if get_config_print_reg() then print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits) ^ " (input: " ^ BitStr(zero_extend(0b0) : xlenbits) ^ ")") diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail index fb46456ba..12fe1f65d 100644 --- a/model/riscv_sys_regs.sail +++ b/model/riscv_sys_regs.sail @@ -160,6 +160,9 @@ function haveZmmul() -> bool = true /* Zicond extension support */ function haveZicond() -> bool = true +/* Zicfilp extension support */ +function haveZicfilp() -> bool = true + bitfield Mstatush : bits(32) = { MPELP: 9, MBE : 5, diff --git a/model/riscv_zicfilp_regs.sail b/model/riscv_zicfilp_regs.sail new file mode 100644 index 000000000..f71317c36 --- /dev/null +++ b/model/riscv_zicfilp_regs.sail @@ -0,0 +1,103 @@ +/*=======================================================================================*/ +/* RISCV Sail Model */ +/* */ +/* This Sail RISC-V architecture model, comprising all files and */ +/* 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 */ +/* Ved Shanbhogue */ +/* 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. */ +/* */ +/* 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. */ +/*=======================================================================================*/ + +/* Architectural state for the Zicfilp extension. */ +type elp_state = bits(1) + +enum ElpState = {NO_LP_EXPECTED, LP_EXPECTED} + +function ElpState_to_bits (e : ElpState) -> elp_state = + match (e) { + NO_LP_EXPECTED => 0b0, + LP_EXPECTED => 0b1 + } + +function ElpState_of_bits (e : elp_state) -> ElpState = + match (e) { + 0b0 => NO_LP_EXPECTED, + 0b1 => LP_EXPECTED + } + +function ElpState_to_str (e : ElpState) -> string = + match (e) { + NO_LP_EXPECTED => "NO_LP_EXPECTED", + LP_EXPECTED => "LP_EXPECTED" + } + +overload to_str = {ElpState_to_str} + +register elp : elp_state + +val init_zicfilp_regs : unit -> unit +function init_zicfilp_regs () = { + elp = ElpState_to_bits(NO_LP_EXPECTED); +} +