Add Zicfiss extension

Makefile

@@ -48,6 +48,9 @@ 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_zimop.sail # Zimop instructions
+SAIL_DEFAULT_INST += riscv_insts_zcmop.sail # Zcmop instructions
+SAIL_DEFAULT_INST += riscv_insts_zicfiss.sail # Zicfiss instructions
 
 SAIL_DEFAULT_INST += riscv_insts_vext_utils.sail
 SAIL_DEFAULT_INST += riscv_insts_vext_vset.sail
@@ -72,6 +75,7 @@ SAIL_SYS_SRCS += riscv_sys_exceptions.sail # default basic helpers for exceptio
 SAIL_SYS_SRCS += riscv_sync_exception.sail # define the exception structure used in the model
 SAIL_SYS_SRCS += riscv_next_control.sail # helpers for the 'N' extension
 SAIL_SYS_SRCS += riscv_softfloat_interface.sail riscv_fdext_regs.sail riscv_fdext_control.sail
+SAIL_SYS_SRCS += riscv_zicfiss_control.sail # Zicfiss CSRs
 SAIL_SYS_SRCS += riscv_csr_ext.sail # access to CSR extensions
 SAIL_SYS_SRCS += riscv_sys_control.sail # general exception handling
 
@@ -96,6 +100,7 @@ PRELUDE = prelude.sail $(SAIL_XLEN) $(SAIL_FLEN) $(SAIL_VLEN) prelude_mem_metada
 
 SAIL_REGS_SRCS = riscv_reg_type.sail riscv_freg_type.sail riscv_regs.sail riscv_pc_access.sail riscv_sys_regs.sail
 SAIL_REGS_SRCS += riscv_pmp_regs.sail riscv_pmp_control.sail
+SAIL_REGS_SRCS += riscv_zicfiss_regs.sail # Zicfiss state
 SAIL_REGS_SRCS += riscv_ext_regs.sail $(SAIL_CHECK_SRCS)
 SAIL_REGS_SRCS += riscv_vreg_type.sail riscv_vext_regs.sail
 

model/riscv_csr_map.sail

@@ -176,6 +176,8 @@ mapping clause csr_name_map = 0x00F <-> "vcsr"
 mapping clause csr_name_map = 0xC20 <-> "vl"
 mapping clause csr_name_map = 0xC21 <-> "vtype"
 mapping clause csr_name_map = 0xC22 <-> "vlenb"
+/* Zicfiss csrs */
+mapping clause csr_name_map = 0x011 <-> "ssp"
 
 val csr_name : csreg -> string
 overload to_str = {csr_name}

model/riscv_insts_zcmop.sail

@@ -0,0 +1,117 @@
+/*=======================================================================================*/
+/* 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. */
+/*=======================================================================================*/
+
+/* ********************************************************************* */
+/* This file specifies the compressed insts. in the 'Zcmop' extension. */
+
+/* These instructions are only legal if misa.C() is true and is checked in
+ * the fetch-execute logic.
+ */
+/* ****************************************************************** */
+/* Zcmops may be redefined by other extensions */
+function is_ext_defined_cmop(mop : bits(3)) -> bool = {
+ /* Zicfiss uses the following cmop codepoints:
+ * mop.rr.7 rd=x0, rs2=x1/x5, rs1=x0 => sspush rs2
+ * c.mop.1 => c.sspush x1
+ * c.mop.5 => c.sspopchk x5
+ */
+ match mop {
+ 0b000 => haveZicfiss(),
+ 0b010 => haveZicfiss(),
+ _ => false
+ }
+}
+
+union clause ast = ZCMOP : (bits(3))
+mapping clause encdec_compressed = ZCMOP(mop)
+ if haveZcmop() & not(is_ext_defined_cmop(mop))
+ <-> 0b01100 @ mop : bits(3) @ 0b100000 @ 0b01
+ if haveZcmop() & not(is_ext_defined_cmop(mop))
+
+mapping zcmop_mnemonic : bits(3) <-> string = {
+ 0b000 <-> "c.mop.1",
+ 0b001 <-> "c.mop.3",
+ 0b010 <-> "c.mop.5",
+ 0b011 <-> "c.mop.7",
+ 0b100 <-> "c.mop.9",
+ 0b101 <-> "c.mop.11",
+ 0b110 <-> "c.mop.13",
+ 0b111 <-> "c.mop.15"
+}
+
+mapping clause assembly = ZCMOP(mop)
+ if haveZcmop() & not(is_ext_defined_cmop(mop))
+ <-> zcmop_mnemonic(mop)
+ if haveZcmop() & not(is_ext_defined_cmop(mop))
+
+function clause execute ZCMOP(mop) = {
+ RETIRE_SUCCESS
+}