Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Adding Zcb implementation #322

Closed
wants to merge 5 commits into from
Closed

Adding Zcb implementation #322

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
f4317ad
Adding Zcb implementation for pull request
junambi Oct 18, 2023
bde4caf
Changed the implementations as per suggestions in PR#322
junambi Oct 24, 2023
29280ad
Fixed syntax error
junambi Oct 24, 2023
e19a6b2
Fixed issues with the Makefile and Zcb sail code
junambi Oct 25, 2023
c35a554
Fixed Makefile as per comments on PR
junambi Nov 10, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 4 additions & 0 deletions Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -29,7 +29,11 @@ SAIL_DEFAULT_INST += riscv_insts_zbb.sail
SAIL_DEFAULT_INST += riscv_insts_zbc.sail
SAIL_DEFAULT_INST += riscv_insts_zbs.sail

SAIL_DEFAULT_INST += riscv_insts_zcb.sail

SAIL_DEFAULT_INST += riscv_insts_zfh.sail


# Zfa needs to be added after fext, dext and Zfh (as it needs
# definitions from those)
SAIL_DEFAULT_INST += riscv_insts_zfa.sail
Expand Down
288 changes: 288 additions & 0 deletions model/riscv_insts_zcb.sail
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,288 @@
/*=======================================================================================*/
/* 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 */
/* Nambi JU */
/* */
/* 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 'Zcb' extension. */
/* ****************************************************************** */

/* ------------------------------------------------------------------ */
/* Sail Model for the c.l and c.s encoding group */
/* ------------------------------------------------------------------ */

/* ****************************************************************** */
union clause ast = C_LBU : (bits(2), cregidx, cregidx)

mapping clause encdec_compressed = C_LBU(ui01, rs1, rd)
<-> 0b100 @ 0b000 @ rs1 : cregidx @ ui01 : bits(2) @ rd : cregidx @ 0b00

function clause execute (C_LBU(uimm, rsc, rdc)) = {
let imm : bits(12) = zero_extend(uimm);
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think this is wrong. The ui65 should be called ui01 and then

let imm : bits(12) = zero_extend(ui01[0] @ ui01[1]);

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Swizzle the bits in decode not execute


let rd = creg2reg_idx(rdc);
let rs = creg2reg_idx(rsc);
execute(LOAD(imm, rs, rd, true, BYTE, false, false))
}

mapping clause assembly = C_LBU(uimm, rsc, rdc)
<-> "c.lbu" ^ spc() ^ creg_name(rdc) ^ sep() ^ creg_name(rsc) ^ sep() ^ hex_bits_5(uimm @ 0b000)
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

uimm wrong here too.

/* ****************************************************************** */
union clause ast = C_LHU : (bits(1), cregidx, cregidx)

mapping clause encdec_compressed = C_LHU(ui1, rs1, rd)
Copy link
Collaborator

@arichardson arichardson Oct 25, 2023 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
mapping clause encdec_compressed = C_LHU(ui1, rs1, rd)
mapping clause encdec_compressed = C_LHU(ui1 @ 0b0, rs1, rd)

Immediate is not scaled in current code. I assume this means there are no tests?

<-> 0b100 @ 0b001 @ rs1 : cregidx @ 0b0 @ ui1 : bits(1) @ rd : cregidx @ 0b00

function clause execute (C_LHU(uimm, rsc, rdc)) = {
let imm : bits(12) = zero_extend(uimm);
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Also wrong - should be zero_extend(ui1 @ 0b0);

Please check the other instructions too.


let rd = creg2reg_idx(rdc);
let rs = creg2reg_idx(rsc);

execute(LOAD(imm, rs, rd, true, HALF, false, false))
}

mapping clause assembly = C_LHU(uimm, rsc, rdc)
<-> "c.lhu" ^ spc() ^ creg_name(rdc) ^ sep() ^ creg_name(rsc) ^ sep() ^ hex_bits_4(uimm @ 0b000)
/* ****************************************************************** */
union clause ast = C_LH : (bits(1), cregidx, cregidx)

mapping clause encdec_compressed = C_LH(ui1, rs1, rd)
<-> 0b100 @ 0b001 @ rs1 : cregidx @ 0b1 @ ui1 : bits(1) @ rd : cregidx @ 0b00

function clause execute (C_LH(uimm, rsc, rdc)) = {
let immext : xlenbits = zero_extend(uimm);
let imm : bits(12) = zero_extend(uimm);

let rd = creg2reg_idx(rdc);
let rs = creg2reg_idx(rsc);

let rsext = X(rs) + immext;
X(rs) = rsext;
execute(LOAD(imm, rs, rd, false, HALF, false, false))
}

mapping clause assembly = C_LH(uimm, rsc, rdc)
<-> "c.lh" ^ spc() ^ creg_name(rdc) ^ sep() ^ creg_name(rsc) ^ sep() ^ hex_bits_4(uimm @ 0b000)
/* ****************************************************************** */

union clause ast = C_SB : (bits(2), cregidx, cregidx)

mapping clause encdec_compressed = C_SB(ui01, rs1, rs2)
<-> 0b100 @ 0b010 @ rs1 : cregidx @ ui01 : bits(2) @ rs2 : cregidx @ 0b00

function clause execute (C_SB(uimm, rs1c, rs2c)) = {
let imm : bits(12) = zero_extend(uimm);

let rs1c = creg2reg_idx(rs1c);
let rs2c = creg2reg_idx(rs2c);
execute(STORE(imm, rs2c, rs1c, BYTE, false, false))
}

mapping clause assembly = C_SB(uimm, rs1, rs2)
<-> "c.sb" ^ spc() ^ creg_name(rs2) ^ sep() ^ creg_name(rs1) ^ sep() ^ hex_bits_5(uimm @ 0b000)
/* ****************************************************************** */
union clause ast = C_SH : (bits(1), cregidx, cregidx)

mapping clause encdec_compressed = C_SH(ui1, rs1, rs2)
<-> 0b100 @ 0b011 @ rs1 : cregidx @ 0b0 @ ui1 : bits(1) @ rs2 : cregidx @ 0b00

function clause execute (C_SH(uimm, rs1c, rs2c)) = {
let imm : bits(12) = zero_extend(uimm);

let rs2c = creg2reg_idx(rs2c);
let rs1c = creg2reg_idx(rs1c);
execute(STORE(imm, rs2c, rs1c, HALF, false, false))
}

mapping clause assembly = C_SH(uimm, rs1, rs2)
<-> "c.sh" ^ spc() ^ creg_name(rs2) ^ sep() ^ creg_name(rs1) ^ sep() ^ hex_bits_4(uimm @ 0b000)
/* ****************************************************************** */

/* ------------------------------------------------------------------ */
/* Sail Model for the c.zext and c.sext encoding group */
/* ------------------------------------------------------------------ */
/* ****************************************************************** */
union clause ast = C_ZEXT_B : (cregidx)

mapping clause encdec_compressed = C_ZEXT_B(rsd)
<-> 0b100 @ 0b111 @ rsd : cregidx @ 0b11 @ 0b000 @ 0b01

function clause execute (C_ZEXT_B(rsd)) = {
let rsdc = creg2reg_idx(rsd);

X(rsdc) = zero_extend(X(rsdc)[7..0]);
RETIRE_SUCCESS
}

mapping clause assembly = C_ZEXT_B(rsd)
<-> "c.zext.b" ^ spc() ^ creg_name(rsd)

/* ****************************************************************** */
union clause ast = C_SEXT_B : (cregidx)

mapping clause encdec_compressed = C_SEXT_B(rsd)
<-> 0b100 @ 0b111 @ rsd : cregidx @ 0b11 @ 0b001 @ 0b01

function clause execute (C_SEXT_B(rsd)) = {
let rsdc = creg2reg_idx(rsd);

execute(ZBB_EXTOP(rsdc, rsdc, RISCV_SEXTB))
}

mapping clause assembly = C_SEXT_B(rsd)
<-> "c.sext.b" ^ spc() ^ creg_name(rsd)
/* ****************************************************************** */
union clause ast = C_ZEXT_H : (cregidx)

mapping clause encdec_compressed = C_ZEXT_H(rsd)
<-> 0b100 @ 0b111 @ rsd : cregidx @ 0b11 @ 0b010 @ 0b01

function clause execute (C_ZEXT_H(rsd)) = {
let rsdc = creg2reg_idx(rsd);

execute(ZBB_EXTOP(rsdc, rsdc, RISCV_ZEXTH))
}

mapping clause assembly = C_ZEXT_H(rsd)
<-> "c.zext.h" ^ spc() ^ creg_name(rsd)

/* ****************************************************************** */
union clause ast = C_SEXT_H : (cregidx)

mapping clause encdec_compressed = C_SEXT_H(rsd)
<-> 0b100 @ 0b111 @ rsd : cregidx @ 0b11 @ 0b011 @ 0b01

function clause execute (C_SEXT_H(rsd)) = {
let rsdc = creg2reg_idx(rsd);

execute(ZBB_EXTOP(rsdc, rsdc, RISCV_SEXTH))
}

mapping clause assembly = C_SEXT_H(rsd)
<-> "c.sext.h" ^ spc() ^ creg_name(rsd)
/* ****************************************************************** */
union clause ast = C_ZEXT_W : (cregidx)

mapping clause encdec_compressed = C_ZEXT_W(rsd)
<-> 0b100 @ 0b111 @ rsd : cregidx @ 0b11 @ 0b100 @ 0b01

function clause execute (C_ZEXT_W(rsd)) = {
let rsdc = creg2reg_idx(rsd);

X(rsdc) = zero_extend(X(rsdc)[31..0]);
RETIRE_SUCCESS
}

mapping clause assembly = C_ZEXT_W(rsd)
<-> "c.zext.w" ^ spc() ^ creg_name(rsd)

/* ****************************************************************** */

/* ------------------------------------------------------------------ */
/* Sail Model for the c.mul encoding group */
/* ------------------------------------------------------------------ */

/* the assembly abstract syntax tree (AST) clause for the CMUL instructions */
union clause ast = C_MUL : (cregidx,cregidx)

/* the encode/decode mapping between AST elements and 16-bit half words */

mapping clause encdec_compressed = C_MUL(rsd, rs2)
<-> 0b100 @ 0b111 @ rsd : cregidx @ 0b10 @ rs2 : cregidx @ 0b01

function clause execute (C_MUL(rsd,rs2)) = {
let rd = creg2reg_idx(rsd);
let rs = creg2reg_idx(rs2);

execute(MUL(rs, rd, rd, false, true, true))
}

mapping clause assembly = C_MUL(rsd, rs2) <->
"c.mul" ^ spc() ^ creg_name(rsd) ^ spc() ^ creg_name(rs2)

/* ------------------------------------------------------------------ */
/* Sail Model for the c.not encoding group */
/* ------------------------------------------------------------------ */

/* the assembly abstract syntax tree (AST) clause for the CNOT instructions */

union clause ast = C_NOT : (cregidx)

/* the encode/decode mapping between AST elements and 16-bit half words */

mapping clause encdec_compressed = C_NOT(rsd)
<-> 0b100 @ 0b111 @ rsd : cregidx @ 0b11 @ 0b101 @ 0b01

function clause execute (C_NOT(rsd)) = {
let rsd = creg2reg_idx(rsd);
X(rsd) = ~(X(rsd));
RETIRE_SUCCESS
}

mapping clause assembly = C_NOT(rsd) <->
"c.not" ^ spc() ^ creg_name(rsd)
Loading