Merge pull request #206 from ptomsich/vrull/zicond

Add support for the Zicond extension

Author: ptomsich

Makefile

@@ -36,6 +36,8 @@ SAIL_DEFAULT_INST += riscv_insts_zks.sail
 SAIL_DEFAULT_INST += riscv_insts_zbkb.sail
 SAIL_DEFAULT_INST += riscv_insts_zbkx.sail
 
+SAIL_DEFAULT_INST += riscv_insts_zicond.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
 

model/riscv_insts_zicond.sail

@@ -0,0 +1,32 @@
+union clause ast = ZICOND_RTYPE : (regidx, regidx, regidx, zicondop)
+
+mapping clause encdec = ZICOND_RTYPE(rs2, rs1, rd, RISCV_CZERO_EQZ) if haveZicond()
+  <-> 0b0000111 @ rs2 @ rs1 @ 0b101 @ rd @ 0b0110011 if haveZicond()
+mapping clause encdec = ZICOND_RTYPE(rs2, rs1, rd, RISCV_CZERO_NEZ) if haveZicond()
+  <-> 0b0000111 @ rs2 @ rs1 @ 0b111 @ rd @ 0b0110011 if haveZicond()
+
+mapping zicond_mnemonic : zicondop <-> string = {
+  RISCV_CZERO_EQZ <-> "czero.eqz",
+  RISCV_CZERO_NEZ <-> "czero.nez"
+}
+
+mapping clause assembly = ZICOND_RTYPE(rs2, rs1, rd, op)
+  <-> zicond_mnemonic(op) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2)
+
+function clause execute (ZICOND_RTYPE(rs2, rs1, rd, RISCV_CZERO_EQZ)) = {
+  let value = X(rs1);
+  let condition = X(rs2);
+  let result : xlenbits = if condition == zeros() then zeros()
+						    else value;
+  X(rd) = result;
+  RETIRE_SUCCESS
+}
+
+function clause execute (ZICOND_RTYPE(rs2, rs1, rd, RISCV_CZERO_NEZ)) = {
+  let value = X(rs1);
+  let condition = X(rs2);
+  let result : xlenbits = if (condition != zeros()) then zeros()
+						    else value;
+  X(rd) = result;
+  RETIRE_SUCCESS
+}

model/riscv_sys_regs.sail

@@ -6,7 +6,7 @@
 /*  in the prover_snapshots directory (which include copies of their                     */
 /*  licences), is subject to the BSD two-clause licence below.                           */
 /*                                                                                       */
-/*  Copyright (c) 2017-2021                                                              */
+/*  Copyright (c) 2017-2023                                                              */
 /*    Prashanth Mundkur                                                                  */
 /*    Rishiyur S. Nikhil and Bluespec, Inc.                                              */
 /*    Jon French                                                                         */
@@ -23,6 +23,7 @@
 /*    Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo  */
 /*    Peter Rugg                                                                         */
 /*    Aril Computer Corp., for contributions by Scott Johnson                            */
+/*    VRULL GmbH, for contributions by Philipp Tomsich                                   */
 /*                                                                                       */
 /*  All rights reserved.                                                                 */
 /*                                                                                       */
@@ -205,6 +206,9 @@ function haveZknd()   -> bool = true
 
 function haveZmmul()  -> bool = true
 
+/* Zicond extension support */
+function haveZicond() -> bool = true
+
 bitfield Mstatush : bits(32) = {
   MBE  : 5,
   SBE  : 4

model/riscv_types.sail

@@ -6,7 +6,7 @@
 /*  in the prover_snapshots directory (which include copies of their                     */
 /*  licences), is subject to the BSD two-clause licence below.                           */
 /*                                                                                       */
-/*  Copyright (c) 2017-2021                                                              */
+/*  Copyright (c) 2017-2023                                                              */
 /*    Prashanth Mundkur                                                                  */
 /*    Rishiyur S. Nikhil and Bluespec, Inc.                                              */
 /*    Jon French                                                                         */
@@ -23,6 +23,7 @@
 /*    Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo  */
 /*    Peter Rugg                                                                         */
 /*    Aril Computer Corp., for contributions by Scott Johnson                            */
+/*    VRULL GmbH, for contributions by Philipp Tomsich                                   */
 /*                                                                                       */
 /*  All rights reserved.                                                                 */
 /*                                                                                       */
@@ -415,6 +416,8 @@ enum biop_zbs = {RISCV_BCLRI, RISCV_BEXTI, RISCV_BINVI, RISCV_BSETI}
 
 enum extop_zbb = {RISCV_SEXTB, RISCV_SEXTH, RISCV_ZEXTH}
 
+enum zicondop = {RISCV_CZERO_EQZ, RISCV_CZERO_NEZ}
+
 val sep : unit <-> string
 mapping sep : unit <-> string = {
   ()     <-> opt_spc() ^ "," ^ def_spc()