From 1e5cbd488e5ad1837632080ee1fa7e89689d3f77 Mon Sep 17 00:00:00 2001 From: Ved Shanbhogue Date: Sun, 28 Jan 2024 17:41:33 -0600 Subject: [PATCH] add Zawrs extension --- Makefile | 1 + c_emulator/riscv_platform.c | 6 ++ c_emulator/riscv_platform.h | 3 + model/riscv_insts_zawrs.sail | 118 +++++++++++++++++++++++++++++++++++ model/riscv_platform.sail | 12 ++++ model/riscv_sys_regs.sail | 3 + model/riscv_types.sail | 3 + ocaml_emulator/platform.ml | 4 ++ 8 files changed, 150 insertions(+) create mode 100644 model/riscv_insts_zawrs.sail diff --git a/Makefile b/Makefile index af355efc1..c71206e02 100644 --- a/Makefile +++ b/Makefile @@ -48,6 +48,7 @@ SAIL_DEFAULT_INST += riscv_insts_zbkb.sail SAIL_DEFAULT_INST += riscv_insts_zbkx.sail SAIL_DEFAULT_INST += riscv_insts_zicond.sail +SAIL_DEFAULT_INST += riscv_insts_zawrs.sail SAIL_DEFAULT_INST += riscv_insts_vext_utils.sail SAIL_DEFAULT_INST += riscv_insts_vext_vset.sail diff --git a/c_emulator/riscv_platform.c b/c_emulator/riscv_platform.c index 2fdb63f92..86ff6ff06 100644 --- a/c_emulator/riscv_platform.c +++ b/c_emulator/riscv_platform.c @@ -176,3 +176,9 @@ unit memea(mach_bits len, sail_int n) { return UNIT; } + +/* Zawrs : Wait-on-Reservation-Set */ +bool reservation_set_valid(unit u) +{ + return reservation_valid; +} diff --git a/c_emulator/riscv_platform.h b/c_emulator/riscv_platform.h index 341bd5964..9bf6269cf 100644 --- a/c_emulator/riscv_platform.h +++ b/c_emulator/riscv_platform.h @@ -42,3 +42,6 @@ unit plat_term_write(mach_bits); mach_bits plat_htif_tohost(unit); unit memea(mach_bits, sail_int); + +/* Zawrs : Wait-on-Reservation-Set */ +bool reservation_set_valid(unit); diff --git a/model/riscv_insts_zawrs.sail b/model/riscv_insts_zawrs.sail new file mode 100644 index 000000000..22a275222 --- /dev/null +++ b/model/riscv_insts_zawrs.sail @@ -0,0 +1,118 @@ +/*=======================================================================================*/ +/* 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-2024 */ +/* 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. */ +/*=======================================================================================*/ + +/* ****************************************************************** */ +/* This file specifies the instructions in the 'Zawrs' extension. */ + +val reservation_set_valid = { + ocaml: "Platform.reservation_set_valid", + interpreter: "Platform.reservation_set_valid", + c: "reservation_set_valid", + lem: "reservation_set_valid" + } : unit -> bool + +/* ****************************************************************** */ +union clause ast = WRS : (wrsop) + +mapping clause encdec = WRS(WRS_STO) if haveZawrs() + <-> 0b000000011101 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011 if haveZawrs() + +mapping clause encdec = WRS(WRS_NTO) if haveZawrs() + <-> 0b000000001101 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011 if haveZawrs() + +/* Hart must resume if a locally enabled interrupt becomes pending, even if delegated */ +function interrupts_pending() -> bool = ((mip.bits() & mie.bits()) != zero_extend(0b0)) + +function clause execute (WRS(op)) = { + + platform_start_wrs_timeout(if op == WRS_STO then true else false); + + while reservation_set_valid() & not(interrupts_pending()) & not(platform_is_wrs_timed_out()) do (); + + platform_stop_wrs_timeout(); + + let timed_out : bool = if not(reservation_set_valid()) | interrupts_pending() then false else true; + + match (op, timed_out) { + (_, false) => RETIRE_SUCCESS, + (WRS_STO, true) => RETIRE_SUCCESS, + (WRS_NTO, true) => match cur_privilege { + Machine => { RETIRE_SUCCESS }, + _ => if mstatus.TW() == 0b1 then { handle_illegal(); RETIRE_FAIL } else { RETIRE_SUCCESS } + } + } +} + +mapping wrs_mnemonic : wrsop <-> string = { + WRS_STO <-> "wrs.sto", + WRS_NTO <-> "wrs.nto", +} +mapping clause assembly = WRS(op) <-> wrs_mnemonic(op) diff --git a/model/riscv_platform.sail b/model/riscv_platform.sail index 19e3d30ae..42deeb423 100644 --- a/model/riscv_platform.sail +++ b/model/riscv_platform.sail @@ -454,3 +454,15 @@ function platform_wfi() -> unit = { mcycle = mtimecmp; } } + +/* Start implementation defined short timeout if short is true + * For no timeout, start a implementation defined timeout if privilege + * level is less than M. + */ +function platform_start_wrs_timeout(short : bool) -> unit = () + +/* Stop any timer started by WRS */ +function platform_stop_wrs_timeout() -> unit = () + +/* Return status of WRS timer timeout */ +function platform_is_wrs_timed_out() -> bool = true diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail index 65d141923..0ade1c77f 100644 --- a/model/riscv_sys_regs.sail +++ b/model/riscv_sys_regs.sail @@ -168,6 +168,9 @@ function haveZalrsc() -> bool = haveAtomics() /* Zicond extension support */ function haveZicond() -> bool = true +/* Zawrs extension support */ +function haveZawrs() -> bool = true + /* * Illegal values legalized to least privileged mode supported. * Note: the only valid combinations of supported modes are M, M+U, M+S+U. diff --git a/model/riscv_types.sail b/model/riscv_types.sail index 2b1c132ec..5b68237d1 100644 --- a/model/riscv_types.sail +++ b/model/riscv_types.sail @@ -357,6 +357,9 @@ enum extop_zbb = {RISCV_SEXTB, RISCV_SEXTH, RISCV_ZEXTH} enum zicondop = {RISCV_CZERO_EQZ, RISCV_CZERO_NEZ} +/* Zawrs : Wait-on-Reservation-Set */ +enum wrsop = {WRS_STO, WRS_NTO} + mapping bool_bits : bool <-> bits(1) = { true <-> 0b1, false <-> 0b0 diff --git a/ocaml_emulator/platform.ml b/ocaml_emulator/platform.ml index 69f271496..3d04c2285 100644 --- a/ocaml_emulator/platform.ml +++ b/ocaml_emulator/platform.ml @@ -181,3 +181,7 @@ let init arch elf_file = in ( write_rom 0 rom; get_slice_int (cur_arch_bitwidth (), rom_base, Big_int.zero) ) + +(* Zawrs: Wait-on-Reservation-Set *) +let reservation_set_valid () = + "none" <> !reservation