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

Implement format-specific encoding mechanism #546

Draft
wants to merge 5 commits into
base: master
Choose a base branch
from
Draft

Implement format-specific encoding mechanism #546

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
41a7d92
WIP: remove build of some instructions to reduce scope
ThinkOpenly Jul 19, 2024
226a28f
[DRAFT] Implement format-specific encoding mechanism
ThinkOpenly Jul 19, 2024
05ddfaa
Implement well-formatted encodings for CF extension
ThinkOpenly Jul 19, 2024
6beae1e
ruin run_tests.sh
ThinkOpenly Sep 10, 2024
738896b
Cleanly end scattered mappings
ThinkOpenly Sep 10, 2024
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
67 changes: 34 additions & 33 deletions Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,45 +23,46 @@ SAIL_VLEN := riscv_vlen.sail

# Instruction sources, depending on target
SAIL_CHECK_SRCS = riscv_addr_checks_common.sail riscv_addr_checks.sail riscv_misa_ext.sail
SAIL_DEFAULT_INST = riscv_insts_base.sail riscv_insts_aext.sail riscv_insts_zca.sail riscv_insts_mext.sail riscv_insts_zicsr.sail riscv_insts_next.sail riscv_insts_hints.sail
SAIL_DEFAULT_INST += riscv_insts_fext.sail riscv_insts_zcf.sail
SAIL_DEFAULT_INST += riscv_insts_dext.sail riscv_insts_zcd.sail
#SAIL_DEFAULT_INST = riscv_insts_base.sail riscv_insts_aext.sail riscv_insts_zca.sail riscv_insts_mext.sail riscv_insts_zicsr.sail riscv_insts_next.sail riscv_insts_hints.sail
#SAIL_DEFAULT_INST += riscv_insts_fext.sail riscv_insts_zcf.sail
#SAIL_DEFAULT_INST += riscv_insts_dext.sail riscv_insts_zcd.sail
SAIL_DEFAULT_INST = riscv_insts_base.sail riscv_insts_zicsr.sail riscv_insts_next.sail

SAIL_DEFAULT_INST += riscv_insts_svinval.sail
#SAIL_DEFAULT_INST += riscv_insts_svinval.sail

SAIL_DEFAULT_INST += riscv_insts_zba.sail
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_zba.sail
#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_zcb.sail

SAIL_DEFAULT_INST += riscv_insts_zfh.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

SAIL_DEFAULT_INST += riscv_insts_zkn.sail
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_DEFAULT_INST += riscv_insts_vext_utils.sail
SAIL_DEFAULT_INST += riscv_insts_vext_fp_utils.sail
SAIL_DEFAULT_INST += riscv_insts_vext_vset.sail
SAIL_DEFAULT_INST += riscv_insts_vext_arith.sail
SAIL_DEFAULT_INST += riscv_insts_vext_fp.sail
SAIL_DEFAULT_INST += riscv_insts_vext_mem.sail
SAIL_DEFAULT_INST += riscv_insts_vext_mask.sail
SAIL_DEFAULT_INST += riscv_insts_vext_vm.sail
SAIL_DEFAULT_INST += riscv_insts_vext_fp_vm.sail
SAIL_DEFAULT_INST += riscv_insts_vext_red.sail
SAIL_DEFAULT_INST += riscv_insts_vext_fp_red.sail
SAIL_DEFAULT_INST += riscv_insts_zicbom.sail
SAIL_DEFAULT_INST += riscv_insts_zicboz.sail
#SAIL_DEFAULT_INST += riscv_insts_zfa.sail

#SAIL_DEFAULT_INST += riscv_insts_zkn.sail
#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_DEFAULT_INST += riscv_insts_vext_utils.sail
#SAIL_DEFAULT_INST += riscv_insts_vext_fp_utils.sail
#SAIL_DEFAULT_INST += riscv_insts_vext_vset.sail
#SAIL_DEFAULT_INST += riscv_insts_vext_arith.sail
#SAIL_DEFAULT_INST += riscv_insts_vext_fp.sail
#SAIL_DEFAULT_INST += riscv_insts_vext_mem.sail
#SAIL_DEFAULT_INST += riscv_insts_vext_mask.sail
#SAIL_DEFAULT_INST += riscv_insts_vext_vm.sail
#SAIL_DEFAULT_INST += riscv_insts_vext_fp_vm.sail
#SAIL_DEFAULT_INST += riscv_insts_vext_red.sail
#SAIL_DEFAULT_INST += riscv_insts_vext_fp_red.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
Expand Down
3 changes: 3 additions & 0 deletions model/riscv_decode_ext.sail
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,4 +15,7 @@ val ext_decode_compressed : bits(16) -> ast
function ext_decode_compressed(bv) = encdec_compressed(bv)

val ext_decode : bits(32) -> ast
/*
function ext_decode(bv) = encdec(bv)
*/
function ext_decode(bv) = fmtencdec(fmt2bits(bv))
202 changes: 158 additions & 44 deletions model/riscv_insts_base.sail
View file
Open in desktop

Large diffs are not rendered by default.

42 changes: 40 additions & 2 deletions model/riscv_insts_begin.sail
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -20,12 +20,50 @@ scattered function execute
val assembly : ast <-> string
scattered mapping assembly

val encdec : ast <-> bits(32)
scattered mapping encdec
val oldencdec : ast <-> bits(32)
scattered mapping oldencdec

union instruction_input = {
RFormat: { funct7: bits(7), rs2: regidx, rs1: regidx, funct3: bits(3), rd: regidx, opcode: bits(7) },
IFormat: { imm: bits(12), rs1: regidx, funct3: bits(3), rd: regidx, opcode: bits(7) },
SFormat: { imm: bits(12), rs2: regidx, rs1: regidx, funct3: bits(3), opcode: bits(7) },
BFormat: { imm: bits(13), rs2: regidx, rs1: regidx, funct3: bits(3), opcode: bits(7) },
UFormat: { imm: bits(20), rd: regidx, opcode: bits(7) },
JFormat: { imm: bits(21), rd: regidx, opcode: bits(7) }
}

val encdec_compressed : ast <-> bits(16)
scattered mapping encdec_compressed

union instruction_input_compressed = {
CRFormat: { funct4: bits(4), rd: regidx, rs2: regidx, op: bits(2) },
// CIFormat: { funct3: bits(3), imm1: bits(1), rd: regidx, imm5: bits(5), op: bits(2) },
CIFormat: { funct3: bits(3), imm: bits(6), rd: regidx, op: bits(2) },
CSSFormat: { funct3: bits(3), imm6: bits(6), rs2: regidx, op: bits(2) },
CIWFormat: { funct3: bits(3), imm8: bits(8), rd: cregidx, op: bits(2) },
CLFormat: { funct3: bits(3), imm: bits(5), rs1: cregidx, rd: cregidx, op: bits(2) },
CSFormat: { funct3: bits(3), imm: bits(5), rs1: cregidx, rs2: cregidx, op: bits(2) },
CAFormat: { funct6: bits(6), rd: cregidx, imm2: bits(2), rs2: cregidx, op: bits(2) },
CBFormat: { funct3: bits(3), offset3: bits(3), rs1: cregidx, offset5: bits(5), op: bits(2) },
CJFormat: { funct3: bits(3), target: bits(11), op: bits(2) }
}

val fmtencdec : ast <-> instruction_input
scattered mapping fmtencdec

val fmtencdec_compressed : ast <-> instruction_input_compressed
scattered mapping fmtencdec_compressed

enum Format = { R_Format, U_Format, I_Format, J_Format, S_Format, B_Format, Unknown_Format }
val opcode2format : bits(7) -> Format
scattered function opcode2format

val fmt2bits16 : instruction_input_compressed <-> bits(16)
scattered mapping fmt2bits16

mapping clause fmt2bits16 = CIFormat(struct { imm = imm1 : bits(1) @ imm5: bits(5), rd = rd, funct3 = funct3, op = op })
<-> funct3 @ imm1 @ rd @ imm5 @ op

/*
* We declare the ILLEGAL/C_ILLEGAL ast clauses here instead of in
* riscv_insts_end, so that model extensions can make use of them.
Expand Down
29 changes: 27 additions & 2 deletions model/riscv_insts_end.sail
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,11 +6,34 @@
/* SPDX-License-Identifier: BSD-2-Clause */
/*=======================================================================================*/

function clause opcode2format _ = Unknown_Format

mapping fmt2bits : instruction_input <-> bits(32) = {

UFormat(struct { imm = imm, rd = rd, opcode = opcode }) if opcode2format(opcode) == U_Format
<-> imm @ rd @ opcode if opcode2format(opcode) == U_Format,

RFormat(struct { funct7 = funct7, rs2 = rs2, rs1 = rs1, funct3 = funct3, rd = rd, opcode = opcode }) if opcode2format(opcode) == R_Format
<-> funct7 @ rs2 @ rs1 @ funct3 @ rd @ opcode if opcode2format(opcode) == R_Format,

JFormat(struct { imm = imm_20 : bits(1) @ imm_19_12 : bits(8) @ imm_11 : bits(1) @ imm_10_1 : bits(10) @ 0b0, rd = rd, opcode = opcode }) if opcode2format(opcode) == J_Format
<-> imm_20 @ imm_10_1 @ imm_11 @ imm_19_12 @ rd @ opcode if opcode2format(opcode) == J_Format,

BFormat(struct { imm = imm_12 : bits(1) @ imm_11 : bits(1) @ imm_10_5 : bits(6) @ imm_4_1 : bits(4) @ 0b0, rs2 = rs2, rs1 = rs1, funct3 = funct3, opcode = opcode }) if opcode2format(opcode) == B_Format
<-> imm_12 @ imm_10_5 @ rs2 @ rs1 @ funct3 @ imm_4_1 @ imm_11 @ opcode if opcode2format(opcode) == B_Format,

SFormat(struct { imm = imm7 : bits(7) @ imm5 : bits(5), rs2 = rs2, rs1 = rs1, funct3 = funct3, opcode = opcode }) if opcode2format(opcode) == S_Format
<-> imm7 @ rs2 @ rs1 @ funct3 @ imm5 @ opcode if opcode2format(opcode) == S_Format,

IFormat(struct { imm = imm, rs1 = rs1, funct3 = funct3, rd = rd, opcode = opcode }) if opcode2format(opcode) == I_Format
<-> imm @ rs1 @ funct3 @ rd @ opcode if opcode2format(opcode) == I_Format,
}

/* Put the illegal instructions last to use their wildcard match. */

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

mapping clause encdec = ILLEGAL(s) <-> s
mapping clause oldencdec = ILLEGAL(s) <-> s

function clause execute (ILLEGAL(s)) = { handle_illegal(); RETIRE_FAIL }

Expand All @@ -32,8 +55,10 @@ end extensionEnabled
end ast
end execute
end assembly
end encdec
end fmtencdec_compressed
end fmtencdec
end encdec_compressed
end oldencdec

val print_insn : ast -> string
function print_insn insn = assembly(insn)
Expand Down
6 changes: 5 additions & 1 deletion model/riscv_insts_next.sail
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,9 +11,13 @@

union clause ast = URET : unit

mapping clause encdec = URET()
mapping clause oldencdec = URET()
<-> 0b0000000 @ 0b00010 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011

function clause opcode2format 0b1110011 = R_Format
mapping clause fmtencdec = URET()
<-> RFormat(struct { funct7 = 0b0000000, rs2 = 0b00000, rs1 = 0b00000, funct3 = 0b000, rd = 0b00000, opcode = 0b1110011 })

function clause execute URET() = {
if not(extensionEnabled(Ext_U)) | not(sys_enable_next())
then handle_illegal()
Expand Down
12 changes: 12 additions & 0 deletions model/riscv_insts_zcf.sail
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,6 +23,9 @@ union clause ast = C_FLWSP : (bits(6), regidx)
mapping clause encdec_compressed = C_FLWSP(ui76 @ ui5 @ ui42, rd) if extensionEnabled(Ext_Zcf)
<-> 0b011 @ ui5 : bits(1) @ rd : regidx @ ui42 : bits(3) @ ui76 : bits(2) @ 0b10 if extensionEnabled(Ext_Zcf)

mapping clause fmtencdec_compressed = C_FLWSP(imm, rd)
<-> CIFormat(struct { funct3 = 0b011, imm = imm, rd = rd, op = 0b10 })

function clause execute (C_FLWSP(imm, rd)) = {
let imm : bits(12) = zero_extend(imm @ 0b00);
execute(LOAD_FP(imm, sp, rd, WORD))
Expand All @@ -39,6 +42,9 @@ union clause ast = C_FSWSP : (bits(6), regidx)
mapping clause encdec_compressed = C_FSWSP(ui76 @ ui52, rs2) if extensionEnabled(Ext_Zcf)
<-> 0b111 @ ui52 : bits(4) @ ui76 : bits(2) @ rs2 : regidx @ 0b10 if extensionEnabled(Ext_Zcf)

mapping clause fmtencdec_compressed = C_FSWSP(imm, rs2)
<-> CIFormat(struct { funct3 = 0b111, imm = imm, rd = rs2, op = 0b10 })

function clause execute (C_FSWSP(uimm, rs2)) = {
let imm : bits(12) = zero_extend(uimm @ 0b00);
execute(STORE_FP(imm, rs2, sp, WORD))
Expand All @@ -55,6 +61,9 @@ union clause ast = C_FLW : (bits(5), cregidx, cregidx)
mapping clause encdec_compressed = C_FLW(ui6 @ ui53 @ ui2, rs1, rd) if extensionEnabled(Ext_Zcf)
<-> 0b011 @ ui53 : bits(3) @ rs1 : cregidx @ ui2 : bits(1) @ ui6 : bits(1) @ rd : cregidx @ 0b00 if extensionEnabled(Ext_Zcf)

mapping clause fmtencdec_compressed = C_FLW(imm, rs1, rd)
<-> CLFormat(struct { funct3 = 0b011, imm = imm, rs1 = rs1, rd = rd, op = 0b00 })

function clause execute (C_FLW(uimm, rsc, rdc)) = {
let imm : bits(12) = zero_extend(uimm @ 0b00);
let rd = creg2reg_idx(rdc);
Expand All @@ -73,6 +82,9 @@ union clause ast = C_FSW : (bits(5), cregidx, cregidx)
mapping clause encdec_compressed = C_FSW(ui6 @ ui53 @ ui2, rs1, rs2) if extensionEnabled(Ext_Zcf)
<-> 0b111 @ ui53 : bits(3) @ rs1 : cregidx @ ui2 : bits(1) @ ui6 : bits(1) @ rs2 : cregidx @ 0b00 if extensionEnabled(Ext_Zcf)

mapping clause fmtencdec_compressed = C_FSW(imm, rs1, rs2)
<-> CSFormat(struct { funct3 = 0b111, imm = imm, rs1 = rs1, rs2 = rs2, op = 0b00 })

function clause execute (C_FSW(uimm, rsc1, rsc2)) = {
let imm : bits(12) = zero_extend(uimm @ 0b00);
let rs1 = creg2reg_idx(rsc1);
Expand Down
5 changes: 4 additions & 1 deletion model/riscv_insts_zicsr.sail
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -18,9 +18,12 @@ mapping encdec_csrop : csrop <-> bits(2) = {
CSRRC <-> 0b11
}

mapping clause encdec = CSR(csr, rs1, rd, is_imm, op)
mapping clause oldencdec = CSR(csr, rs1, rd, is_imm, op)
<-> csr @ rs1 @ bool_bits(is_imm) @ encdec_csrop(op) @ rd @ 0b1110011

mapping clause fmtencdec = CSR(csr, rs1, rd, is_imm, op)
<-> IFormat(struct { imm = csr, rs1 = rs1, funct3 = bool_bits(is_imm) @ encdec_csrop(op), rd = rd, opcode = 0b1110011 })

function readCSR csr : csreg -> xlenbits = {
let res : xlenbits =
match (csr, sizeof(xlen)) {
Expand Down
Loading
Loading