diff options
| author | Philipp Tomsich <philipp.tomsich@vrull.eu> | 2023-01-20 15:15:13 +0100 |
|---|---|---|
| committer | Philipp Tomsich <philipp.tomsich@vrull.eu> | 2023-05-29 20:54:10 +0200 |
| commit | 136be16cf30eabc9b9f34323636b881aee63be25 (patch) | |
| tree | 847aa1e4144622edcc6eebe31ee96c9294a69cb8 | |
| parent | 5a8fb7da91c35328da12d6cfb44cd7f0b64f490c (diff) | |
| download | sail-riscv-136be16cf30eabc9b9f34323636b881aee63be25.zip sail-riscv-136be16cf30eabc9b9f34323636b881aee63be25.tar.gz sail-riscv-136be16cf30eabc9b9f34323636b881aee63be25.tar.bz2 | |
Add support for the Zicond extension
This implements the Zicond (conditional integer operations) extension,
as of version 1.0-draft-20230120.
The Zicond extension acts as a building block for branchless sequences
including conditional-arithmetic, conditional-logic and
conditional-select/move.
The following instructions constitute Zicond:
- czero.eqz rd, rs1, rs2 => rd = (rs2 == 0) ? 0 : rs1
- czero.nez rd, rs1, rs2 => rd = (rs2 != 0) ? 0 : rs1
See
https://github.com/riscv/riscv-zicond/releases/download/v1.0-draft-20230120/riscv-zicond_1.0-draft-20230120.pdf
for the proposed specification and usage details.
Co-authored-by: Jessica Clarke <jrtc27@jrtc27.com>
Signed-off-by: Philipp Tomsich <philipp.tomsich@vrull.eu>
| -rw-r--r-- | Makefile | 2 | ||||
| -rw-r--r-- | model/riscv_insts_zicond.sail | 32 | ||||
| -rw-r--r-- | model/riscv_sys_regs.sail | 6 | ||||
| -rw-r--r-- | model/riscv_types.sail | 5 |
4 files changed, 43 insertions, 2 deletions
@@ -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 diff --git a/model/riscv_insts_zicond.sail b/model/riscv_insts_zicond.sail new file mode 100644 index 0000000..7ecfcb3 --- /dev/null +++ b/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 +} diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail index 85d5c73..3ee24a4 100644 --- a/model/riscv_sys_regs.sail +++ b/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 diff --git a/model/riscv_types.sail b/model/riscv_types.sail index 9b9323e..bfb176e 100644 --- a/model/riscv_types.sail +++ b/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() |