diff --git a/Makefile b/Makefile index 3198db7ee..c49f9f04c 100644 --- a/Makefile +++ b/Makefile @@ -41,6 +41,9 @@ SAIL_DEFAULT_INST += riscv_insts_zbkx.sail SAIL_DEFAULT_INST += riscv_insts_zicond.sail +SAIL_DEFAULT_INST += riscv_insts_zicbom.sail +SAIL_DEFAULT_INST += riscv_insts_zicboz.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/c_emulator/riscv_platform.c b/c_emulator/riscv_platform.c index 917a36a95..c90863d32 100644 --- a/c_emulator/riscv_platform.c +++ b/c_emulator/riscv_platform.c @@ -82,6 +82,11 @@ mach_bits plat_rom_size(unit u) return rv_rom_size; } +mach_bits plat_cache_block_size() +{ + return rv_cache_block_size; +} + // Provides entropy for the scalar cryptography extension. mach_bits plat_get_16_random_bits() { diff --git a/c_emulator/riscv_platform.h b/c_emulator/riscv_platform.h index aec59d017..972933c62 100644 --- a/c_emulator/riscv_platform.h +++ b/c_emulator/riscv_platform.h @@ -19,6 +19,8 @@ bool within_phys_mem(mach_bits, sail_int); mach_bits plat_rom_base(unit); mach_bits plat_rom_size(unit); +mach_bits plat_cache_block_size(unit); + // Provides entropy for the scalar cryptography extension. mach_bits plat_get_16_random_bits(); diff --git a/c_emulator/riscv_platform_impl.c b/c_emulator/riscv_platform_impl.c index 148c72bd4..de1b2eec5 100644 --- a/c_emulator/riscv_platform_impl.c +++ b/c_emulator/riscv_platform_impl.c @@ -20,6 +20,8 @@ uint64_t rv_ram_size = UINT64_C(0x4000000); uint64_t rv_rom_base = UINT64_C(0x1000); uint64_t rv_rom_size = UINT64_C(0x100); +uint64_t rv_cache_block_size = UINT64_C(0x40); + // Provides entropy for the scalar cryptography extension. uint64_t rv_16_random_bits(void) { diff --git a/c_emulator/riscv_platform_impl.h b/c_emulator/riscv_platform_impl.h index d24ecc8fb..2882436a7 100644 --- a/c_emulator/riscv_platform_impl.h +++ b/c_emulator/riscv_platform_impl.h @@ -23,6 +23,8 @@ extern uint64_t rv_ram_size; extern uint64_t rv_rom_base; extern uint64_t rv_rom_size; +extern uint64_t rv_cache_block_size; + // Provides entropy for the scalar cryptography extension. extern uint64_t rv_16_random_bits(void); diff --git a/c_emulator/riscv_sim.c b/c_emulator/riscv_sim.c index fdb9ce01d..5e3b730d2 100644 --- a/c_emulator/riscv_sim.c +++ b/c_emulator/riscv_sim.c @@ -137,6 +137,7 @@ static struct option options[] = { #ifdef SAILCOV {"sailcov-file", required_argument, 0, 'c'}, #endif + {"cache-block-size", required_argument, 0, 'B'}, {0, 0, 0, 0 } }; @@ -221,6 +222,7 @@ char *process_args(int argc, char **argv) { int c; uint64_t ram_size = 0; + uint64_t block_size = 0; while (true) { c = getopt_long(argc, argv, "a" @@ -249,6 +251,7 @@ char *process_args(int argc, char **argv) "V::" "v::" "l:" + "B:" "x", options, NULL); if (c == -1) @@ -352,6 +355,17 @@ char *process_args(int argc, char **argv) sailcov_file = strdup(optarg); break; #endif + case 'B': + block_size = atol(optarg); + if ((block_size & (block_size - 1)) == 0) { + fprintf(stderr, "setting cache-block-size to %" PRIu64 " B\n", + block_size); + rv_cache_block_size = block_size; + } else { + fprintf(stderr, "invalid cache-block-size '%s' provided.\n", optarg); + exit(1); + } + break; case '?': print_usage(argv[0], 1); break; diff --git a/handwritten_support/0.11/riscv_extras.lem b/handwritten_support/0.11/riscv_extras.lem index 2509057e6..3e038115a 100644 --- a/handwritten_support/0.11/riscv_extras.lem +++ b/handwritten_support/0.11/riscv_extras.lem @@ -107,6 +107,10 @@ val plat_rom_size : forall 'a. Size 'a => unit -> bitvector 'a let plat_rom_size () = wordFromInteger 0 declare ocaml target_rep function plat_rom_size = `Platform.rom_size` +val plat_cache_block_size : forall 'a. Size 'a => unit -> bitvector 'a +let plat_cache_block_size () = wordFromInteger 0 +declare ocaml target_rep function plat_cache_block_size = `Platform.cache_block_size` + val plat_clint_base : forall 'a. Size 'a => unit -> bitvector 'a let plat_clint_base () = wordFromInteger 0 declare ocaml target_rep function plat_clint_base = `Platform.clint_base` diff --git a/handwritten_support/0.11/riscv_extras_sequential.lem b/handwritten_support/0.11/riscv_extras_sequential.lem index 0c236515f..d841f615d 100644 --- a/handwritten_support/0.11/riscv_extras_sequential.lem +++ b/handwritten_support/0.11/riscv_extras_sequential.lem @@ -99,6 +99,10 @@ val plat_rom_size : forall 'a. Size 'a => unit -> bitvector 'a let plat_rom_size () = wordFromInteger 0 declare ocaml target_rep function plat_rom_size = `Platform.rom_size` +val plat_cache_block_size : forall 'a. Size 'a => unit -> bitvector 'a +let plat_cache_block_size () = wordFromInteger 0 +declare ocaml target_rep function plat_cache_block_size = `Platform.cache_block_size` + val plat_clint_base : forall 'a. Size 'a => unit -> bitvector 'a let plat_clint_base () = wordFromInteger 0 declare ocaml target_rep function plat_clint_base = `Platform.clint_base` diff --git a/handwritten_support/riscv_extras.lem b/handwritten_support/riscv_extras.lem index a476136f7..4a89a5884 100644 --- a/handwritten_support/riscv_extras.lem +++ b/handwritten_support/riscv_extras.lem @@ -177,6 +177,10 @@ val plat_rom_size : forall 'a. Size 'a => unit -> bitvector 'a let plat_rom_size () = wordFromInteger 0 declare ocaml target_rep function plat_rom_size = `Platform.rom_size` +val plat_cache_block_size : forall 'a. Size 'a => unit -> bitvector 'a +let plat_cache_block_size () = wordFromInteger 0 +declare ocaml target_rep function plat_cache_block_size = `Platform.cache_block_size` + val plat_clint_base : forall 'a. Size 'a => unit -> bitvector 'a let plat_clint_base () = wordFromInteger 0 declare ocaml target_rep function plat_clint_base = `Platform.clint_base` diff --git a/handwritten_support/riscv_extras_sequential.lem b/handwritten_support/riscv_extras_sequential.lem index 41ca9c6f8..238c49246 100644 --- a/handwritten_support/riscv_extras_sequential.lem +++ b/handwritten_support/riscv_extras_sequential.lem @@ -169,6 +169,10 @@ val plat_rom_size : forall 'a. Size 'a => unit -> bitvector 'a let plat_rom_size () = wordFromInteger 0 declare ocaml target_rep function plat_rom_size = `Platform.rom_size` +val plat_cache_block_size : forall 'a. Size 'a => unit -> bitvector 'a +let plat_cache_block_size () = wordFromInteger 0 +declare ocaml target_rep function plat_cache_block_size = `Platform.cache_block_size` + val plat_clint_base : forall 'a. Size 'a => unit -> bitvector 'a let plat_clint_base () = wordFromInteger 0 declare ocaml target_rep function plat_clint_base = `Platform.clint_base` diff --git a/model/riscv_addr_checks.sail b/model/riscv_addr_checks.sail index 33091d93e..def2f431b 100644 --- a/model/riscv_addr_checks.sail +++ b/model/riscv_addr_checks.sail @@ -116,7 +116,7 @@ type ext_data_addr_error = unit /* Default data addr is just base register + immediate offset (may be zero). Extensions might override and add additional checks. */ -function ext_data_get_addr(base : regidx, offset : xlenbits, acc : AccessType(ext_access_type), width : word_width) +function ext_data_get_addr(base : regidx, offset : xlenbits, acc : AccessType(ext_access_type), width : xlenbits) -> Ext_DataAddr_Check(ext_data_addr_error) = let addr = X(base) + offset in Ext_DataAddr_OK(addr) diff --git a/model/riscv_csr_map.sail b/model/riscv_csr_map.sail index e3f8f5bb8..974bd761e 100644 --- a/model/riscv_csr_map.sail +++ b/model/riscv_csr_map.sail @@ -113,6 +113,8 @@ mapping clause csr_name_map = 0x143 <-> "stval" mapping clause csr_name_map = 0x144 <-> "sip" /* supervisor protection and translation */ mapping clause csr_name_map = 0x180 <-> "satp" +/* supervisor envcfg */ +mapping clause csr_name_map = 0x10A <-> "senvcfg" /* machine information registers */ mapping clause csr_name_map = 0xF11 <-> "mvendorid" mapping clause csr_name_map = 0xF12 <-> "marchid" @@ -159,6 +161,8 @@ mapping clause csr_name_map = 0xB00 <-> "mcycle" mapping clause csr_name_map = 0xB02 <-> "minstret" mapping clause csr_name_map = 0xB80 <-> "mcycleh" mapping clause csr_name_map = 0xB82 <-> "minstreth" +/* machine envcfg */ +mapping clause csr_name_map = 0x30A <-> "menvcfg" /* TODO: other hpm counters and events */ /* trigger/debug */ mapping clause csr_name_map = 0x7a0 <-> "tselect" diff --git a/model/riscv_insts_aext.sail b/model/riscv_insts_aext.sail index 6e64101d1..927a6da29 100644 --- a/model/riscv_insts_aext.sail +++ b/model/riscv_insts_aext.sail @@ -127,7 +127,7 @@ function clause execute(LOADRES(aq, rl, rs1, width, rd)) = { /* Get the address, X(rs1) (no offset). * Extensions might perform additional checks on address validity. */ - match ext_data_get_addr(rs1, zeros(), Read(Data), width) { + match ext_data_get_addr(rs1, zeros(), Read(Data), EXTZ(size_bits(width))) { Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL }, Ext_DataAddr_OK(vaddr) => { let aligned : bool = @@ -188,7 +188,7 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = { /* Get the address, X(rs1) (no offset). * Extensions might perform additional checks on address validity. */ - match ext_data_get_addr(rs1, zeros(), Write(Data), width) { + match ext_data_get_addr(rs1, zeros(), Write(Data), EXTZ(size_bits(width))) { Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL }, Ext_DataAddr_OK(vaddr) => { let aligned : bool = @@ -278,7 +278,7 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = { /* Get the address, X(rs1) (no offset). * Some extensions perform additional checks on address validity. */ - match ext_data_get_addr(rs1, zeros(), ReadWrite(Data, Data), width) { + match ext_data_get_addr(rs1, zeros(), ReadWrite(Data, Data), EXTZ(size_bits(width))) { Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL }, Ext_DataAddr_OK(vaddr) => { match translateAddr(vaddr, ReadWrite(Data, Data)) { diff --git a/model/riscv_insts_base.sail b/model/riscv_insts_base.sail index eccaac4f5..430646c88 100644 --- a/model/riscv_insts_base.sail +++ b/model/riscv_insts_base.sail @@ -388,7 +388,7 @@ function clause execute(LOAD(imm, rs1, rd, is_unsigned, width, aq, rl)) = { let offset : xlenbits = EXTS(imm); /* Get the address, X(rs1) + offset. Some extensions perform additional checks on address validity. */ - match ext_data_get_addr(rs1, offset, Read(Data), width) { + match ext_data_get_addr(rs1, offset, Read(Data), EXTZ(size_bits(width))) { Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL }, Ext_DataAddr_OK(vaddr) => if check_misaligned(vaddr, width) @@ -444,7 +444,7 @@ function clause execute (STORE(imm, rs2, rs1, width, aq, rl)) = { let offset : xlenbits = EXTS(imm); /* Get the address, X(rs1) + offset. Some extensions perform additional checks on address validity. */ - match ext_data_get_addr(rs1, offset, Write(Data), width) { + match ext_data_get_addr(rs1, offset, Write(Data), EXTZ(size_bits(width))) { Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL }, Ext_DataAddr_OK(vaddr) => if check_misaligned(vaddr, width) diff --git a/model/riscv_insts_fext.sail b/model/riscv_insts_fext.sail index c7e1541f3..bb97b5a76 100644 --- a/model/riscv_insts_fext.sail +++ b/model/riscv_insts_fext.sail @@ -377,7 +377,7 @@ function clause execute(LOAD_FP(imm, rs1, rd, width)) = { let offset : xlenbits = EXTS(imm); /* Get the address, X(rs1) + offset. Some extensions perform additional checks on address validity. */ - match ext_data_get_addr(rs1, offset, Read(Data), width) { + match ext_data_get_addr(rs1, offset, Read(Data), EXTZ(size_bits(width))) { Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL }, Ext_DataAddr_OK(vaddr) => if check_misaligned(vaddr, width) @@ -443,7 +443,7 @@ function clause execute (STORE_FP(imm, rs2, rs1, width)) = { let (aq, rl, con) = (false, false, false); /* Get the address, X(rs1) + offset. Some extensions perform additional checks on address validity. */ - match ext_data_get_addr(rs1, offset, Write(Data), width) { + match ext_data_get_addr(rs1, offset, Write(Data), EXTZ(size_bits(width))) { Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL }, Ext_DataAddr_OK(vaddr) => if check_misaligned(vaddr, width) diff --git a/model/riscv_insts_zicbom.sail b/model/riscv_insts_zicbom.sail new file mode 100644 index 000000000..67db5f382 --- /dev/null +++ b/model/riscv_insts_zicbom.sail @@ -0,0 +1,150 @@ +/*=======================================================================================*/ +/* 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 */ +/* PLCT, 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. */ +/*=======================================================================================*/ + +/* ****************************************************************** */ +union clause ast = RISCV_ZICBOM : (cbop_zicbom, regidx) + +mapping encdec_cbop : cbop_zicbom <-> bits(12) = { + CBO_CLEAN <-> 0b000000000001, + CBO_FLUSH <-> 0b000000000010, + CBO_INVAL <-> 0b000000000000 +} + +mapping clause encdec = RISCV_ZICBOM(cbop, rs1) if haveZicbom() + <-> encdec_cbop(cbop) @ rs1 @ 0b010 @ 0b00000 @ 0b0001111 if haveZicbom() + +mapping cbop_mnemonic : cbop_zicbom <-> string = { + CBO_CLEAN <-> "cbo.clean", + CBO_FLUSH <-> "cbo.flush", + CBO_INVAL <-> "cbo.inval" +} + +mapping clause assembly = RISCV_ZICBOM(cbop, rs1) + <-> cbop_mnemonic(cbop) ^ spc() ^ "(" ^ reg_name(rs1) ^ ")" + +val process_clean_inval : (regidx, cbop_zicbom) -> Retired effect {escape, rmem, rmemt, rreg, wmv, wmvt, wreg} +function process_clean_inval(rs1, cbop) = { + let rs1_val = X(rs1); + let cache_block_size = plat_cache_block_size(); + let begin_addr = rs1_val & ~(cache_block_size - EXTZ(0b1)); + let offset = begin_addr - rs1_val; + match ext_data_get_addr(rs1, offset, Read(Data), cache_block_size) { + Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL }, + Ext_DataAddr_OK(vaddr) => { + let res: option(ExceptionType) = match translateAddr(vaddr, Read(Data)) { + TR_Address(paddr, _) => { + match mem_read(Read(Data), paddr, 1, false, false, false) { + MemValue(_) => None(), + MemException(e) => Some(e) + } + }, + TR_Failure(e, _) => Some(e) + }; + match res { + None() => RETIRE_SUCCESS, // do nothing for cbop currently + Some(e) => { + match (e) { + E_Load_Access_Fault() => { handle_mem_exception(vaddr, E_SAMO_Access_Fault()); RETIRE_FAIL }, + E_Load_Page_Fault() => { handle_mem_exception(vaddr, E_SAMO_Page_Fault()); RETIRE_FAIL } + } + } + } + } + } +} + +function cbo_clean_flush_enable(p : Privilege) -> bool = + ~((p != Machine & menvcfg.CBCFE() == 0b0) | (p == User & senvcfg.CBCFE() == 0b0)) + +function cbop_for_cbo_inval(p : Privilege) -> option(cbop_zicbom) = { + let illegal = ((p != Machine) & (menvcfg.CBIE() == 0b00)) | + ((p == User) & (senvcfg.CBIE() == 0b00)); + let flush = ((p != Machine) & (menvcfg.CBIE() == 0b01)) | + ((p == User) & (senvcfg.CBIE() == 0b01)); + if illegal then None() + else if flush then Some(CBO_FLUSH) + else Some(CBO_INVAL) +} + +function clause execute(RISCV_ZICBOM(cbop, rs1)) = { + let cbcfe = cbo_clean_flush_enable(cur_privilege); + let final_op : option(cbop_zicbom) = match (cbop, cbcfe) { + (CBO_CLEAN, true) => Some(CBO_CLEAN), + (CBO_CLEAN, false) => None(), + (CBO_FLUSH, true) => Some(CBO_FLUSH), + (CBO_FLUSH, false) => None(), + (CBO_INVAL, _) => cbop_for_cbo_inval(cur_privilege) + }; + match final_op { + None() => { handle_illegal(); RETIRE_FAIL }, + Some(cbop) => process_clean_inval(rs1, cbop) + } +} diff --git a/model/riscv_insts_zicboz.sail b/model/riscv_insts_zicboz.sail new file mode 100644 index 000000000..b73c1b76a --- /dev/null +++ b/model/riscv_insts_zicboz.sail @@ -0,0 +1,127 @@ +/*=======================================================================================*/ +/* 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 */ +/* PLCT, 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. */ +/*=======================================================================================*/ + +/* ****************************************************************** */ +union clause ast = RISCV_ZICBOZ : (regidx) + +mapping clause encdec = RISCV_ZICBOZ(rs1) if haveZicboz() + <-> 0b000000000100 @ rs1 @ 0b010 @ 0b00000 @ 0b0001111 if haveZicboz() + +mapping clause assembly = RISCV_ZICBOZ(rs1) + <-> "cbo.zero" ^ spc() ^ "(" ^ reg_name(rs1) ^ ")" + +function get_envcfg_cbze(p : Privilege) -> bool = + ~((p != Machine & menvcfg.CBZE() == 0b0) | (p == User & senvcfg.CBZE() == 0b0)) + +val process_cbo_zero : (regidx) -> Retired effect {eamem, escape, rmem, rmemt, rreg, wmv, wmvt, wreg} +function process_cbo_zero(rs1) = { + let rs1_val = X(rs1); + let cache_block_size = plat_cache_block_size(); + let begin_addr = rs1_val & ~(cache_block_size - EXTZ(0b1)); + let offset = begin_addr - rs1_val; + index : xlenbits = zeros(); + failed : bool = false; + match ext_data_get_addr(rs1, offset, Write(Data), cache_block_size) { + Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); failed = true }, + Ext_DataAddr_OK(vaddr) => + while (index <_u cache_block_size) & (failed == false) do { + let addr = vaddr + index; + match translateAddr(addr, Write(Data)) { + TR_Failure(e, _) => { handle_mem_exception(vaddr, e); failed = true }, + TR_Address(paddr, _) => { + let eares : MemoryOpResult(unit) = mem_write_ea(paddr, 1, false, false, false); + match (eares) { + MemException(e) => { handle_mem_exception(vaddr, e); failed = true }, + MemValue(_) => { + let res : MemoryOpResult(bool) = mem_write_value(paddr, 1, zeros(), false, false, false); + match (res) { + MemValue(true) => index = index + EXTZ(0b1), + MemValue(false) => internal_error(__FILE__, __LINE__, "store got false from mem_write_value"), + MemException(e) => { handle_mem_exception(vaddr, e); failed = true } + } + } + } + } + } + } + }; + if failed then RETIRE_FAIL + else RETIRE_SUCCESS +} + +function clause execute(RISCV_ZICBOZ(rs1)) = { + if get_envcfg_cbze(cur_privilege) then + process_cbo_zero(rs1) + else { + handle_illegal(); + RETIRE_FAIL + } +} diff --git a/model/riscv_insts_zicsr.sail b/model/riscv_insts_zicsr.sail index b93283483..09e0d50aa 100644 --- a/model/riscv_insts_zicsr.sail +++ b/model/riscv_insts_zicsr.sail @@ -98,6 +98,7 @@ function readCSR csr : csreg -> xlenbits = { (0x304, _) => mie.bits(), (0x305, _) => get_mtvec(), (0x306, _) => EXTZ(mcounteren.bits()), + (0x30A, _) => menvcfg.bits(), (0x310, 32) => mstatush.bits(), (0x320, _) => EXTZ(mcountinhibit.bits()), @@ -145,6 +146,7 @@ function readCSR csr : csreg -> xlenbits = { (0x104, _) => lower_mie(mie, mideleg).bits(), (0x105, _) => get_stvec(), (0x106, _) => EXTZ(scounteren.bits()), + (0x10A, _) => senvcfg.bits(), (0x140, _) => sscratch, (0x141, _) => get_xret_target(Supervisor) & pc_alignment_mask(), (0x142, _) => scause.bits(), @@ -186,6 +188,7 @@ function writeCSR (csr : csreg, value : xlenbits) -> unit = { (0x304, _) => { mie = legalize_mie(mie, value); Some(mie.bits()) }, (0x305, _) => { Some(set_mtvec(value)) }, (0x306, _) => { mcounteren = legalize_mcounteren(mcounteren, value); Some(EXTZ(mcounteren.bits())) }, + (0x30A, _) => { menvcfg = legalize_envcfg(menvcfg, value); Some(menvcfg.bits()) }, (0x310, 32) => { Some(mstatush.bits()) }, // ignore writes for now (0x320, _) => { mcountinhibit = legalize_mcountinhibit(mcountinhibit, value); Some(EXTZ(mcountinhibit.bits())) }, (0x340, _) => { mscratch = value; Some(mscratch) }, @@ -233,6 +236,7 @@ function writeCSR (csr : csreg, value : xlenbits) -> unit = { (0x104, _) => { mie = legalize_sie(mie, mideleg, value); Some(mie.bits()) }, (0x105, _) => { Some(set_stvec(value)) }, (0x106, _) => { scounteren = legalize_scounteren(scounteren, value); Some(EXTZ(scounteren.bits())) }, + (0x10A, _) => { senvcfg = legalize_envcfg(senvcfg, value); Some(senvcfg.bits()) }, (0x140, _) => { sscratch = value; Some(sscratch) }, (0x141, _) => { Some(set_xret_target(Supervisor, value)) }, (0x142, _) => { scause->bits() = value; Some(scause.bits()) }, diff --git a/model/riscv_platform.sail b/model/riscv_platform.sail index aed996626..83982df26 100644 --- a/model/riscv_platform.sail +++ b/model/riscv_platform.sail @@ -88,6 +88,8 @@ val elf_entry = { c: "elf_entry" } : unit -> int +val plat_cache_block_size = {c: "plat_cache_block_size", ocaml: "Platform.cache_block_size", interpreter: "Platform.cache_block_size", lem: "plat_cache_block_size"} : unit -> xlenbits + /* Main memory */ val plat_ram_base = {c: "plat_ram_base", ocaml: "Platform.dram_base", interpreter: "Platform.dram_base", lem: "plat_ram_base"} : unit -> xlenbits val plat_ram_size = {c: "plat_ram_size", ocaml: "Platform.dram_size", interpreter: "Platform.dram_size", lem: "plat_ram_size"} : unit -> xlenbits diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail index c2d968095..3362d3ee6 100644 --- a/model/riscv_sys_control.sail +++ b/model/riscv_sys_control.sail @@ -91,6 +91,7 @@ function is_CSR_defined (csr : csreg, p : Privilege) -> bool = 0x304 => p == Machine, // mie 0x305 => p == Machine, // mtvec 0x306 => p == Machine & haveUsrMode(), // mcounteren + 0x30a => p == Machine, // menvcfg 0x310 => p == Machine & (sizeof(xlen) == 32), // mstatush 0x320 => p == Machine, // mcountinhibit /* machine mode: trap handling */ @@ -140,6 +141,8 @@ function is_CSR_defined (csr : csreg, p : Privilege) -> bool = 0x105 => haveSupMode() & (p == Machine | p == Supervisor), // stvec 0x106 => haveSupMode() & (p == Machine | p == Supervisor), // scounteren + 0x10a => haveSupMode() & (p == Machine | p == Supervisor), // senvcfg + /* supervisor mode: trap handling */ 0x140 => haveSupMode() & (p == Machine | p == Supervisor), // sscratch 0x141 => haveSupMode() & (p == Machine | p == Supervisor), // sepc @@ -598,6 +601,8 @@ function init_sys() -> unit = { minstret = EXTZ(0b0); minstret_increment = true; + menvcfg->bits() = EXTZ(0b0); + init_pmp(); // log compatibility with spike diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail index ecc7735b7..22ae057f2 100644 --- a/model/riscv_sys_regs.sail +++ b/model/riscv_sys_regs.sail @@ -213,6 +213,10 @@ function haveZmmul() -> bool = true /* Zicond extension support */ function haveZicond() -> bool = true +/* Cache Management Operations extension support. */ +function haveZicbom() -> bool = true +function haveZicboz() -> bool = true + bitfield Mstatush : bits(32) = { MBE : 5, SBE : 4 @@ -830,3 +834,27 @@ function read_seed_csr() -> xlenbits = { /* Writes to the seed CSR are ignored */ function write_seed_csr () -> option(xlenbits) = None() + +bitfield Envcfg : xlenbits = { + CBZE : 7, + CBCFE : 6, + CBIE : 5 .. 4 +} +register senvcfg : Envcfg +register menvcfg : Envcfg + +/* treat 0b10 as 0b00: Partially, the encoding was set up so that bit [4] was an + * "enable" bit, and bit [5] was an "operation" bit. So if bit [4] was zero, + * bit [5] is a don't care. + */ +function legalize_envcfg_cbie(o : bits(2), v : bits(2)) -> bits(2) = match (v) { + 0b10 => 0b00, + _ => v +} + +function legalize_envcfg(o : Envcfg, v : xlenbits) -> Envcfg = { + let c = update_CBZE(o, [v[7]]); + let c = update_CBCFE(c, [v[6]]); + let c = update_CBIE(c, legalize_envcfg_cbie(o.CBIE(), v[5 .. 4])); + c +} diff --git a/model/riscv_types.sail b/model/riscv_types.sail index 728c1d26c..6ac623f67 100644 --- a/model/riscv_types.sail +++ b/model/riscv_types.sail @@ -398,6 +398,8 @@ enum amoop = {AMOSWAP, AMOADD, AMOXOR, AMOAND, AMOOR, AMOMIN, AMOMAX, AMOMINU, AMOMAXU} /* AMO ops */ enum csrop = {CSRRW, CSRRS, CSRRC} /* CSR ops */ +enum cbop_zicbom = {CBO_CLEAN, CBO_FLUSH, CBO_INVAL} /* Zicbom ops */ + enum brop_zba = {RISCV_SH1ADD, RISCV_SH2ADD, RISCV_SH3ADD} enum brop_zbb = {RISCV_ANDN, RISCV_ORN, RISCV_XNOR, RISCV_MAX, diff --git a/ocaml_emulator/platform.ml b/ocaml_emulator/platform.ml index ccf487589..8ffff87fd 100644 --- a/ocaml_emulator/platform.ml +++ b/ocaml_emulator/platform.ml @@ -90,6 +90,8 @@ let rom_size () = arch_bits_of_int !rom_size_ref let dram_base () = arch_bits_of_int64 P.dram_base let dram_size () = arch_bits_of_int64 !P.dram_size_ref +let cache_block_size () = arch_bits_of_int64 !P.cache_block_size_ref + let clint_base () = arch_bits_of_int64 P.clint_base let clint_size () = arch_bits_of_int64 P.clint_size diff --git a/ocaml_emulator/platform_impl.ml b/ocaml_emulator/platform_impl.ml index 39de43776..b55edfbb1 100644 --- a/ocaml_emulator/platform_impl.ml +++ b/ocaml_emulator/platform_impl.ml @@ -57,6 +57,8 @@ let rom_base = 0x00001000L;; (* Spike::DEFAULT_RSTVEC *) let dram_size_ref = ref (Int64.(shift_left 64L 20)) +let cache_block_size_ref = ref (Int64.(64L)) + type mem_region = { addr : Int64.t; size : Int64.t @@ -144,6 +146,9 @@ let set_dtc path = let set_dram_size mb = dram_size_ref := Int64.(shift_left (Int64.of_int mb) 20) +let set_cache_block_size b = + cache_block_size_ref := Int64.(Int64.of_int b) + let make_dtb dts = (* Call the dtc compiler, assumed to be at /usr/bin/dtc *) try let cmd = Printf.sprintf "%s -I dts" !dtc_path in diff --git a/ocaml_emulator/riscv_ocaml_sim.ml b/ocaml_emulator/riscv_ocaml_sim.ml index 6e612ad26..6b828445c 100644 --- a/ocaml_emulator/riscv_ocaml_sim.ml +++ b/ocaml_emulator/riscv_ocaml_sim.ml @@ -59,6 +59,9 @@ let options = Arg.align ([("-dump-dts", ("-ram-size", Arg.Int PI.set_dram_size, " size of physical ram memory to use (in MB)"); + ("-cache-block-size", + Arg.Int PI.set_cache_block_size, + " size of cache block size to use (in bytes)"); ("-report-arch", Arg.Unit report_arch, " report model architecture (RV32 or RV64)");