diff options
| -rw-r--r-- | riscv/riscv.sail | 159 | ||||
| -rw-r--r-- | riscv/riscv_sys.sail | 20 | ||||
| -rw-r--r-- | riscv/riscv_types.sail | 119 |
3 files changed, 129 insertions, 169 deletions
diff --git a/riscv/riscv.sail b/riscv/riscv.sail index f7cb702c..f79c3c4f 100644 --- a/riscv/riscv.sail +++ b/riscv/riscv.sail @@ -18,12 +18,12 @@ function clause decode imm : bits(20) @ rd : regbits @ 0b0110111 = Some(UTYPE(im function clause decode imm : bits(20) @ rd : regbits @ 0b0010111 = Some(UTYPE(imm, rd, RISCV_AUIPC)) function clause execute UTYPE(imm, rd, op) = - let off : bits(64) = EXTS(imm @ 0x000) in - let ret : regval = match op { + let off : xlenbits = EXTS(imm @ 0x000) in + let ret : xlenbits = match op { RISCV_LUI => off, RISCV_AUIPC => PC + off } in - wGPR(rd, ret) + X(rd) = ret /* ****************************************************************** */ @@ -32,9 +32,9 @@ union clause ast = RISCV_JAL : (bits(21), regbits) function clause decode imm : bits(20) @ rd : regbits @ 0b1101111 = Some (RISCV_JAL(imm[19] @ imm[7..0] @ imm[8] @ imm[18..13] @ imm[12..9] @ 0b0, rd)) function clause execute (RISCV_JAL(imm, rd)) = { - let pc : bits(64) = PC; - wGPR(rd, nextPC); /* compatible with JAL and C.JAL */ - let offset : bits(64) = EXTS(imm); + let pc : xlenbits = PC; + X(rd) = nextPC; /* compatible with JAL and C.JAL */ + let offset : xlenbits = EXTS(imm); nextPC = pc + offset; } @@ -46,8 +46,8 @@ function clause decode imm : bits(12) @ rs1 : regbits @ 0b000 @ rd : regbits @ 0 function clause execute (RISCV_JALR(imm, rs1, rd)) = { /* write rd before anything else to prevent unintended strength */ - wGPR(rd, nextPC); /* compatible with JALR, C.JR and C.JALR */ - let newPC : bits(64) = rGPR(rs1) + EXTS(imm); + X(rd) = nextPC; /* compatible with JALR, C.JR and C.JALR */ + let newPC : xlenbits = X(rs1) + EXTS(imm); nextPC = newPC[63..1] @ 0b0; } @@ -62,8 +62,8 @@ function clause decode imm7 : bits(7) @ rs2 : regbits @ rs1 : regbits @ 0b110 @ function clause decode imm7 : bits(7) @ rs2 : regbits @ rs1 : regbits @ 0b111 @ imm5 : bits(5) @ 0b1100011 = Some(BTYPE(imm7[6] @ imm5[0] @ imm7[5..0] @ imm5[4..1] @ 0b0, rs2, rs1, RISCV_BGEU)) function clause execute (BTYPE(imm, rs2, rs1, op)) = - let rs1_val = rGPR(rs1) in - let rs2_val = rGPR(rs2) in + let rs1_val = X(rs1) in + let rs2_val = X(rs2) in let taken : bool = match op { RISCV_BEQ => rs1_val == rs2_val, RISCV_BNE => rs1_val != rs2_val, @@ -86,17 +86,17 @@ function clause decode imm : bits(12) @ rs1 : regbits @ 0b110 @ rd : regbits @ 0 function clause decode imm : bits(12) @ rs1 : regbits @ 0b111 @ rd : regbits @ 0b0010011 = Some(ITYPE(imm, rs1, rd, RISCV_ANDI)) function clause execute (ITYPE (imm, rs1, rd, op)) = - let rs1_val = rGPR(rs1) in - let imm64 : bits(64) = EXTS(imm) in - let result : bits(64) = match op { - RISCV_ADDI => rs1_val + imm64, - RISCV_SLTI => EXTZ(rs1_val <_s imm64), - RISCV_SLTIU => EXTZ(rs1_val <_u imm64), - RISCV_XORI => rs1_val ^ imm64, - RISCV_ORI => rs1_val | imm64, - RISCV_ANDI => rs1_val & imm64 + let rs1_val = X(rs1) in + let immext : xlenbits = EXTS(imm) in + let result : xlenbits = match op { + RISCV_ADDI => rs1_val + immext, + RISCV_SLTI => EXTZ(rs1_val <_s immext), + RISCV_SLTIU => EXTZ(rs1_val <_u immext), + RISCV_XORI => rs1_val ^ immext, + RISCV_ORI => rs1_val | immext, + RISCV_ANDI => rs1_val & immext } in - wGPR(rd, result) + X(rd) = result /* ****************************************************************** */ union clause ast = SHIFTIOP : (bits(6), regbits, regbits, sop) @@ -106,13 +106,13 @@ function clause decode 0b000000 @ shamt : bits(6) @ rs1 : regbits @ 0b101 @ rd : function clause decode 0b010000 @ shamt : bits(6) @ rs1 : regbits @ 0b101 @ rd : regbits @ 0b0010011 = Some(SHIFTIOP(shamt, rs1, rd, RISCV_SRAI)) function clause execute (SHIFTIOP(shamt, rs1, rd, op)) = - let rs1_val = rGPR(rs1) in - let result : bits(64) = match op { + let rs1_val = X(rs1) in + let result : xlenbits = match op { RISCV_SLLI => rs1_val << shamt, RISCV_SRLI => rs1_val >> shamt, RISCV_SRAI => shift_right_arith64(rs1_val, shamt) } in - wGPR(rd, result) + X(rd) = result /* ****************************************************************** */ @@ -131,9 +131,9 @@ function clause decode 0b0000000 @ rs2 : regbits @ rs1 : regbits @ 0b111 @ rd : function clause execute (RTYPE(rs2, rs1, rd, op)) = - let rs1_val = rGPR(rs1) in - let rs2_val = rGPR(rs2) in - let result : bits(64) = match op { + let rs1_val = X(rs1) in + let rs2_val = X(rs2) in + let result : xlenbits = match op { RISCV_ADD => rs1_val + rs2_val, RISCV_SUB => rs1_val - rs2_val, RISCV_SLL => rs1_val << (rs2_val[5..0]), @@ -145,7 +145,7 @@ function clause execute (RTYPE(rs2, rs1, rd, op)) = RISCV_OR => rs1_val | rs2_val, RISCV_AND => rs1_val & rs2_val } in - wGPR(rd, result) + X(rd) = result /* ****************************************************************** */ union clause ast = LOAD : (bits(12), regbits, regbits, bool, word_width, bool, bool) @@ -160,8 +160,8 @@ function clause decode imm : bits(12) @ rs1 : regbits @ 0b110 @ rd : regbits @ 0 function clause execute(LOAD(imm, rs1, rd, is_unsigned, width, aq, rl)) = - let addr : bits(64) = rGPR(rs1) + EXTS(imm) in - let result : bits(64) = if is_unsigned then + let addr : xlenbits = X(rs1) + EXTS(imm) in + let result : xlenbits = if is_unsigned then match width { BYTE => EXTZ(mem_read(addr, 1, aq, rl, false)), HALF => EXTZ(mem_read(addr, 2, aq, rl, false)), @@ -175,7 +175,7 @@ function clause execute(LOAD(imm, rs1, rd, is_unsigned, width, aq, rl)) = WORD => EXTS(mem_read(addr, 4, aq, rl, false)), DOUBLE => mem_read(addr, 8, aq, rl, false) } in - wGPR(rd, result) + X(rd) = result /* ****************************************************************** */ union clause ast = STORE : (bits(12), regbits, regbits, word_width, bool, bool) @@ -186,14 +186,14 @@ function clause decode imm7 : bits(7) @ rs2 : regbits @ rs1 : regbits @ 0b010 @ function clause decode imm7 : bits(7) @ rs2 : regbits @ rs1 : regbits @ 0b011 @ imm5 : bits(5) @ 0b0100011 = Some(STORE(imm7 @ imm5, rs2, rs1, DOUBLE, false, false)) function clause execute (STORE(imm, rs2, rs1, width, aq, rl)) = - let addr : bits(64) = rGPR(rs1) + EXTS(imm) in { + let addr : xlenbits = X(rs1) + EXTS(imm) in { match width { BYTE => mem_write_ea(addr, 1, aq, rl, false), HALF => mem_write_ea(addr, 2, aq, rl, false), WORD => mem_write_ea(addr, 4, aq, rl, false), DOUBLE => mem_write_ea(addr, 8, aq, rl, false) }; - let rs2_val = rGPR(rs2) in + let rs2_val = X(rs2) in match width { BYTE => mem_write_value(addr, 1, rs2_val[7..0], aq, rl, false), HALF => mem_write_value(addr, 2, rs2_val[15..0], aq, rl, false), @@ -209,10 +209,8 @@ union clause ast = ADDIW : (bits(12), regbits, regbits) function clause decode imm : bits(12) @ rs1 : regbits @ 0b000 @ rd : regbits @ 0b0011011 = Some(ADDIW(imm, rs1, rd)) function clause execute (ADDIW(imm, rs1, rd)) = - let imm64 : bits(64) = EXTS(imm) in - let result64 : bits(64) = imm64 + rGPR(rs1) in - let result32 : bits(64) = EXTS(result64[31..0]) in - wGPR(rd, result32) + let result : xlenbits = EXTS(imm) + X(rs1) in + X(rd) = EXTS(result[31..0]) /* ****************************************************************** */ union clause ast = SHIFTW : (bits(5), regbits, regbits, sop) @@ -222,13 +220,13 @@ function clause decode 0b0000000 @ shamt : bits(5) @ rs1 : regbits @ 0b101 @ rd function clause decode 0b0100000 @ shamt : bits(5) @ rs1 : regbits @ 0b101 @ rd : regbits @ 0b0011011 = Some(SHIFTW(shamt, rs1, rd, RISCV_SRAI)) function clause execute (SHIFTW(shamt, rs1, rd, op)) = - let rs1_val = (rGPR(rs1))[31..0] in + let rs1_val = (X(rs1))[31..0] in let result : bits(32) = match op { RISCV_SLLI => rs1_val << shamt, RISCV_SRLI => rs1_val >> shamt, RISCV_SRAI => shift_right_arith32(rs1_val, shamt) } in - wGPR(rd, EXTS(result)) + X(rd) = EXTS(result) /* ****************************************************************** */ union clause ast = RTYPEW : (regbits, regbits, regbits, ropw) @@ -240,8 +238,8 @@ function clause decode 0b0000000 @ rs2 : regbits @ rs1 : regbits @ 0b101 @ rd : function clause decode 0b0100000 @ rs2 : regbits @ rs1 : regbits @ 0b101 @ rd : regbits @ 0b0111011 = Some(RTYPEW(rs2, rs1, rd, RISCV_SRAW)) function clause execute (RTYPEW(rs2, rs1, rd, op)) = - let rs1_val = (rGPR(rs1))[31..0] in - let rs2_val = (rGPR(rs2))[31..0] in + let rs1_val = (X(rs1))[31..0] in + let rs2_val = (X(rs2))[31..0] in let result : bits(32) = match op { RISCV_ADDW => rs1_val + rs2_val, RISCV_SUBW => rs1_val - rs2_val, @@ -249,7 +247,7 @@ function clause execute (RTYPEW(rs2, rs1, rd, op)) = RISCV_SRLW => rs1_val >> (rs2_val[4..0]), RISCV_SRAW => shift_right_arith32(rs1_val, rs2_val[4..0]) } in - wGPR(rd, EXTS(result)) + X(rd) = EXTS(result) /* ****************************************************************** */ @@ -260,13 +258,13 @@ function clause decode 0b0000001 @ rs2 : regbits @ rs1 : regbits @ 0b001 @ rd : function clause decode 0b0000001 @ rs2 : regbits @ rs1 : regbits @ 0b010 @ rd : regbits @ 0b0110011 = Some(MUL(rs2, rs1, rd, true, true, false)) /* MULHSU */ function clause decode 0b0000001 @ rs2 : regbits @ rs1 : regbits @ 0b011 @ rd : regbits @ 0b0110011 = Some(MUL(rs2, rs1, rd, true, false, false)) /* MULHU */ function clause execute (MUL(rs2, rs1, rd, high, signed1, signed2)) = - let rs1_val = rGPR(rs1) in - let rs2_val = rGPR(rs2) in + let rs1_val = X(rs1) in + let rs2_val = X(rs2) in let rs1_int : int = if signed1 then signed(rs1_val) else unsigned(rs1_val) in let rs2_int : int = if signed2 then signed(rs2_val) else unsigned(rs2_val) in let result128 = to_bits(128, rs1_int * rs2_int) in let result = if high then result128[127..64] else result128[63..0] in - wGPR(rd, result) + X(rd) = result /* ****************************************************************** */ @@ -274,13 +272,12 @@ union clause ast = DIV : (regbits, regbits, regbits, bool) function clause decode 0b0000001 @ rs2 : regbits @ rs1 : regbits @ 0b100 @ rd : regbits @ 0b0110011 = Some(DIV(rs2, rs1, rd, true)) /* DIV */ function clause decode 0b0000001 @ rs2 : regbits @ rs1 : regbits @ 0b101 @ rd : regbits @ 0b0110011 = Some(DIV(rs2, rs1, rd, false)) /* DIVU */ function clause execute (DIV(rs2, rs1, rd, s)) = - let rs1_val = rGPR(rs1) in - let rs2_val = rGPR(rs2) in + let rs1_val = X(rs1) in + let rs2_val = X(rs2) in let rs1_int : int = if s then signed(rs1_val) else unsigned(rs1_val) in let rs2_int : int = if s then signed(rs2_val) else unsigned(rs2_val) in let q : int = if rs2_int == 0 then -1 else quot_round_zero(rs1_int, rs2_int) in - let q': int = if s & q > (2 ^ 63 - 1) then (0 - 2^63) else q in /* check for signed overflow */ - wGPR(rd, to_bits(64, q')) + let q': int = if s & q > xlen_max_signed then xlen_min_signed else q in /* check for signed overflow */ X(rd) = to_bits(xlen, q') /* ****************************************************************** */ @@ -288,26 +285,26 @@ union clause ast = REM : (regbits, regbits, regbits, bool) function clause decode 0b0000001 @ rs2 : regbits @ rs1 : regbits @ 0b110 @ rd : regbits @ 0b0110011 = Some(REM(rs2, rs1, rd, true)) /* REM */ function clause decode 0b0000001 @ rs2 : regbits @ rs1 : regbits @ 0b111 @ rd : regbits @ 0b0110011 = Some(REM(rs2, rs1, rd, false)) /* REMU */ function clause execute (REM(rs2, rs1, rd, s)) = - let rs1_val = rGPR(rs1) in - let rs2_val = rGPR(rs2) in + let rs1_val = X(rs1) in + let rs2_val = X(rs2) in let rs1_int : int = if s then signed(rs1_val) else unsigned(rs1_val) in let rs2_int : int = if s then signed(rs2_val) else unsigned(rs2_val) in let r : int = if rs2_int == 0 then rs1_int else rem_round_zero(rs1_int, rs2_int) in /* signed overflow case returns zero naturally as required due to -1 divisor */ - wGPR(rd, to_bits(64, r)) + X(rd) = to_bits(xlen, r) /* ****************************************************************** */ union clause ast = MULW : (regbits, regbits, regbits) function clause decode 0b0000001 @ rs2 : regbits @ rs1 : regbits @ 0b000 @ rd : regbits @ 0b0111011 = Some(MULW(rs2, rs1, rd)) /* MULW */ function clause execute (MULW(rs2, rs1, rd)) = - let rs1_val = rGPR(rs1)[31..0] in - let rs2_val = rGPR(rs2)[31..0] in + let rs1_val = X(rs1)[31..0] in + let rs2_val = X(rs2)[31..0] in let rs1_int : int = signed(rs1_val) in let rs2_int : int = signed(rs2_val) in let result32 = to_bits(64, rs1_int * rs2_int)[31..0] in /* XXX surprising behaviour of to_bits requires exapnsion to 64 bits followed by truncation... */ - let result64 : regval = EXTS(result32) in - wGPR(rd, result64) + let result : xlenbits = EXTS(result32) in + X(rd) = result /* ****************************************************************** */ @@ -315,13 +312,13 @@ union clause ast = DIVW : (regbits, regbits, regbits, bool) function clause decode 0b0000001 @ rs2 : regbits @ rs1 : regbits @ 0b100 @ rd : regbits @ 0b0111011 = Some(DIVW(rs2, rs1, rd, true)) /* DIVW */ function clause decode 0b0000001 @ rs2 : regbits @ rs1 : regbits @ 0b101 @ rd : regbits @ 0b0111011 = Some(DIVW(rs2, rs1, rd, false)) /* DIVUW */ function clause execute (DIVW(rs2, rs1, rd, s)) = - let rs1_val = rGPR(rs1)[31..0] in - let rs2_val = rGPR(rs2)[31..0] in + let rs1_val = X(rs1)[31..0] in + let rs2_val = X(rs2)[31..0] in let rs1_int : int = if s then signed(rs1_val) else unsigned(rs1_val) in let rs2_int : int = if s then signed(rs2_val) else unsigned(rs2_val) in let q : int = if rs2_int == 0 then -1 else quot_round_zero(rs1_int, rs2_int) in let q': int = if s & q > (2 ^ 31 - 1) then (0 - 2^31) else q in /* check for signed overflow */ - wGPR(rd, EXTS(to_bits(32, q'))) + X(rd) = EXTS(to_bits(32, q')) /* ****************************************************************** */ @@ -329,13 +326,13 @@ union clause ast = REMW : (regbits, regbits, regbits, bool) function clause decode 0b0000001 @ rs2 : regbits @ rs1 : regbits @ 0b110 @ rd : regbits @ 0b0111011 = Some(REMW(rs2, rs1, rd, true)) /* REMW */ function clause decode 0b0000001 @ rs2 : regbits @ rs1 : regbits @ 0b111 @ rd : regbits @ 0b0111011 = Some(REMW(rs2, rs1, rd, false)) /* REMUW */ function clause execute (REMW(rs2, rs1, rd, s)) = - let rs1_val = rGPR(rs1)[31..0] in - let rs2_val = rGPR(rs2)[31..0] in + let rs1_val = X(rs1)[31..0] in + let rs2_val = X(rs2)[31..0] in let rs1_int : int = if s then signed(rs1_val) else unsigned(rs1_val) in let rs2_int : int = if s then signed(rs2_val) else unsigned(rs2_val) in let r : int = if rs2_int == 0 then rs1_int else rem_round_zero(rs1_int, rs2_int) in /* signed overflow case returns zero naturally as required due to -1 divisor */ - wGPR(rd, EXTS(to_bits(32, r))) + X(rd) = EXTS(to_bits(32, r)) /* ****************************************************************** */ @@ -373,7 +370,7 @@ function clause execute ECALL = USER => User_ECall, MACHINE => Machine_ECall }, - excinfo = (None : option(regval)) } in + excinfo = (None : option(xlenbits)) } in nextPC = handle_exception_ctl(cur_privilege, CTL_TRAP(t), PC) /* ****************************************************************** */ @@ -398,14 +395,14 @@ function clause decode 0b00010 @ [aq] @ [rl] @ 0b00000 @ rs1 : regbits @ 0b010 @ function clause decode 0b00010 @ [aq] @ [rl] @ 0b00000 @ rs1 : regbits @ 0b011 @ rd : regbits @ 0b0101111 = Some(LOADRES(aq, rl, rs1, DOUBLE, rd)) function clause execute(LOADRES(aq, rl, rs1, width, rd)) = - let addr : bits(64) = rGPR(rs1) in - let result : bits(64) = + let addr : xlenbits = X(rs1) in + let result : xlenbits = match width { WORD => EXTS(mem_read(addr, 4, aq, rl, true)), DOUBLE => mem_read(addr, 8, aq, rl, true), _ => internal_error("LOADRES expected WORD or DOUBLE") } in - wGPR(rd, result) + X(rd) = result /* ****************************************************************** */ union clause ast = STORECON : (bool, bool, regbits, regbits, word_width, regbits) @@ -415,16 +412,16 @@ function clause decode 0b00011 @ [aq] @ [rl] @ rs2 : regbits @ rs1 : regbits @ 0 function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = { status : bits(1) = if speculate_conditional_success() then 0b0 else 0b1; - wGPR(rd) = EXTZ(status); + X(rd) = EXTZ(status); if status == 0b1 then () else { - addr : bits(64) = rGPR(rs1); + addr : xlenbits = X(rs1); match width { WORD => mem_write_ea(addr, 4, aq, rl, true), DOUBLE => mem_write_ea(addr, 8, aq, rl, true), _ => internal_error("STORECON expected word or double") }; - rs2_val = rGPR(rs2); + rs2_val = X(rs2); match width { WORD => mem_write_value(addr, 4, rs2_val[31..0], aq, rl, true), DOUBLE => mem_write_value(addr, 8, rs2_val, aq, rl, true), @@ -456,7 +453,7 @@ function clause decode 0b11100 @ [aq] @ [rl] @ rs2 : regbits @ rs1 : regbits @ 0 function clause decode 0b11100 @ [aq] @ [rl] @ rs2 : regbits @ rs1 : regbits @ 0b011 @ rd : regbits @ 0b0101111 = Some(AMO(AMOMAXU, aq, rl, rs2, rs1, DOUBLE, rd)) function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = { - addr : bits(64) = rGPR(rs1); + addr : xlenbits = X(rs1); match width { WORD => mem_write_ea(addr, 4, aq & rl, rl, true), @@ -464,16 +461,16 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = { _ => internal_error ("AMO expected WORD or DOUBLE") }; - loaded : bits(64) = + loaded : xlenbits = match width { WORD => EXTS(mem_read(addr, 4, aq, aq & rl, true)), DOUBLE => mem_read(addr, 8, aq, aq & rl, true), _ => internal_error ("AMO expected WORD or DOUBLE") }; - wGPR(rd) = loaded; + X(rd) = loaded; - rs2_val : bits(64) = rGPR(rs2); - result : bits(64) = + rs2_val : xlenbits = X(rs2); + result : xlenbits = match op { AMOSWAP => rs2_val, AMOADD => rs2_val + loaded, @@ -529,7 +526,7 @@ function isCSRImplemented csr : bits(12) -> bool = _ => false } -function readCSR csr: bits(12) -> regval = +function readCSR csr: bits(12) -> xlenbits = match csr { 0x300 => mstatus.bits(), 0x302 => medeleg.bits(), @@ -545,7 +542,7 @@ function readCSR csr: bits(12) -> regval = 0x0000_0000_0000_0000 } } -function writeCSR (csr : bits(12), value : bits(64)) -> unit = +function writeCSR (csr : bits(12), value : xlenbits) -> unit = match csr { 0x300 => mstatus->bits() = value, 0x302 => medeleg->bits() = value, @@ -568,13 +565,13 @@ val signalIllegalInstruction : unit -> unit effect {escape} function signalIllegalInstruction () = not_implemented ("illegal instruction") function clause execute CSR(csr, rs1, rd, is_imm, op) = - let rs1_val : bits(64) = if is_imm then EXTZ(rs1) else rGPR(rs1) in + let rs1_val : xlenbits = if is_imm then EXTZ(rs1) else X(rs1) in let isWrite : bool = match op { CSRRW => true, _ => if is_imm then unsigned(rs1_val) != 0 else unsigned(rs1) != 0 } in if ~ (isCSRImplemented(csr) & haveCSRPriv(csr, isWrite)) then { - let instr : regval = EXTZ(__RISCV_read(PC, 4)); + let instr : xlenbits = EXTZ(__RISCV_read(PC, 4)); let t : sync_exception = struct { trap = Illegal_Instr, excinfo = Some (instr) } in @@ -582,14 +579,14 @@ function clause execute CSR(csr, rs1, rd, is_imm, op) = } else { let csr_val = readCSR(csr); /* could have side-effects, so technically shouldn't perform for CSRW[I] with rd == 0 */ if isWrite then { - let new_val : bits(64) = match op { + let new_val : xlenbits = match op { CSRRW => rs1_val, CSRRS => csr_val | rs1_val, CSRRC => csr_val & ~(rs1_val) } in writeCSR(csr, new_val) }; - wGPR(rd, csr_val) + X(rd) = csr_val } /* ****************************************************************** */ @@ -712,9 +709,9 @@ function clause execute (C_JAL(imm)) = { function clause execute (C_ADDIW(imm, rsd)) = { let imm : bits(32) = EXTS(imm) in - let rs_val = rGPR(rsd) in + let rs_val = X(rsd) in let res : bits(32) = rs_val[31..0] + imm in - wGPR(rsd, EXTS(res)) + X(rsd) = EXTS(res) } /* ****************************************************************** */ diff --git a/riscv/riscv_sys.sail b/riscv/riscv_sys.sail index 68ef7a55..ccbe58fb 100644 --- a/riscv/riscv_sys.sail +++ b/riscv/riscv_sys.sail @@ -195,24 +195,24 @@ bitfield Medeleg : bits(64) = { register medeleg : Medeleg /* exception registers */ -register mepc : regval -register mtval : regval -register mtvec : regval -register mcause : regval -register mscratch : regval +register mepc : xlenbits +register mtval : xlenbits +register mtvec : xlenbits +register mcause : xlenbits +register mscratch : xlenbits /* other registers */ -register pmpaddr0 : regval -register pmpcfg0 : regval +register pmpaddr0 : xlenbits +register pmpcfg0 : xlenbits /* TODO: this should be readonly, and always 0 for now */ -register mhartid : regval +register mhartid : xlenbits /* instruction control flow */ struct sync_exception = { trap : ExceptionCode, - excinfo : option(regval) + excinfo : option(xlenbits) } union ctl_result = { @@ -246,7 +246,7 @@ function bits_to_priv(b : bits(2)) -> privilege = /* handle exceptional ctl flow by updating nextPC */ function handle_exception_ctl(cur_priv : privilege, ctl : ctl_result, - pc: regval) -> regval = + pc: xlenbits) -> xlenbits = /* TODO: check delegation */ match (cur_priv, ctl) { (_, CTL_TRAP(e)) => { diff --git a/riscv/riscv_types.sail b/riscv/riscv_types.sail index 477b4902..2e3e29f6 100644 --- a/riscv/riscv_types.sail +++ b/riscv/riscv_types.sail @@ -8,7 +8,11 @@ function internal_error(s) = { throw (Error_internal_error) } -type regval = bits(64) +let xlen = 64 +type xlenbits = bits(64) +let xlen_max_unsigned = 2 ^ xlen - 1 +let xlen_max_signed = 2 ^ (xlen - 1) - 1 +let xlen_min_signed = 0 - 2 ^ (xlen - 1) type regno ('n : Int), 0 <= 'n < 32 = atom('n) type regbits = bits(5) @@ -20,82 +24,41 @@ function regbits_to_regno b = let 'r = unsigned(b) in r val creg2reg_bits : cregbits -> regbits function creg2reg_bits(creg) = 0b10 @ creg -/* register x0 : regval is hard-wired zero */ -register x1 : regval -register x2 : regval -register x3 : regval -register x4 : regval -register x5 : regval -register x6 : regval -register x7 : regval -register x8 : regval -register x9 : regval -register x10 : regval -register x11 : regval -register x12 : regval -register x13 : regval -register x14 : regval -register x15 : regval -register x16 : regval -register x17 : regval -register x18 : regval -register x19 : regval -register x20 : regval -register x21 : regval -register x22 : regval -register x23 : regval -register x24 : regval -register x25 : regval -register x26 : regval -register x27 : regval -register x28 : regval -register x29 : regval -register x30 : regval -register x31 : regval - /* some arch and ABI relevant registers */ let zreg : regbits = 0b00000 let ra : regbits = 0b00001 /* x1 */ let sp : regbits = 0b00010 /* x2 */ -register PC : bits(64) -register nextPC : bits(64) +register PC : xlenbits +register nextPC : xlenbits -let GPRs : vector(31, dec, register(regval)) = - [ ref x31, ref x30, ref x29, ref x28, - ref x27, ref x26, ref x25, ref x24, - ref x23, ref x22, ref x21, ref x20, - ref x19, ref x18, ref x17, ref x16, - ref x15, ref x14, ref x13, ref x12, - ref x11, ref x10, ref x9, ref x8, - ref x7, ref x6, ref x5, ref x4, - ref x3, ref x2, ref x1 /* ref x0 */ - ] +register Xs : vector(32, dec, xlenbits) -/* Getters and setters for registers */ -val rGPR : forall 'n, 0 <= 'n < 32. regno('n) -> regval effect {rreg} +/* Getters and setters for X registers (special case for zeros register, x0) */ +val rX : forall 'n, 0 <= 'n < 32. regno('n) -> xlenbits effect {rreg} -function rGPR 0 = 0x0000000000000000 -and rGPR (r if r > 0) = reg_deref(GPRs[r - 1]) +function rX 0 = 0x0000000000000000 +and rX (r if r > 0) = Xs[r] -/*val wGPR : forall 'n, 0 <= 'n < 32. (regno('n), regval) -> unit effect {wreg}*/ -val wGPR : forall 'n, 0 <= 'n < 32. (regno('n), regval) -> unit effect {wreg} +val wX : forall 'n, 0 <= 'n < 32. (regno('n), xlenbits) -> unit effect {wreg} -function wGPR (r, v) = +function wX (r, v) = if (r != 0) then { - (*GPRs[r - 1]) = v; + Xs[r] = v; print_string("x", concat_str(string_of_int(r), concat_str(" <- ", BitStr(v)))); } -function check_alignment (addr : bits(64), width : atom('n)) -> forall 'n. unit = +overload X = {rX, wX} + +function check_alignment (addr : xlenbits, width : atom('n)) -> forall 'n. unit = if unsigned(addr) % width != 0 then throw(Error_misaligned_access) else () -val MEMr : forall 'n. (bits(64), atom('n)) -> bits(8 * 'n) effect {rmem} -val MEMr_acquire : forall 'n. (bits(64), atom('n)) -> bits(8 * 'n) effect {rmem} -val MEMr_strong_acquire : forall 'n. (bits(64), atom('n)) -> bits(8 * 'n) effect {rmem} -val MEMr_reserved : forall 'n. (bits(64), atom('n)) -> bits(8 * 'n) effect {rmem} -val MEMr_reserved_acquire : forall 'n. (bits(64), atom('n)) -> bits(8 * 'n) effect {rmem} -val MEMr_reserved_strong_acquire : forall 'n. (bits(64), atom('n)) -> bits(8 * 'n) effect {rmem} +val MEMr : forall 'n. (xlenbits, atom('n)) -> bits(8 * 'n) effect {rmem} +val MEMr_acquire : forall 'n. (xlenbits, atom('n)) -> bits(8 * 'n) effect {rmem} +val MEMr_strong_acquire : forall 'n. (xlenbits, atom('n)) -> bits(8 * 'n) effect {rmem} +val MEMr_reserved : forall 'n. (xlenbits, atom('n)) -> bits(8 * 'n) effect {rmem} +val MEMr_reserved_acquire : forall 'n. (xlenbits, atom('n)) -> bits(8 * 'n) effect {rmem} +val MEMr_reserved_strong_acquire : forall 'n. (xlenbits, atom('n)) -> bits(8 * 'n) effect {rmem} function MEMr (addr, width) = __RISCV_read(addr, width) function MEMr_acquire (addr, width) = __RISCV_read(addr, width) @@ -104,7 +67,7 @@ function MEMr_reserved (addr, width) = __RISCV_read(addr, width) function MEMr_reserved_acquire (addr, width) = __RISCV_read(addr, width) function MEMr_reserved_strong_acquire (addr, width) = __RISCV_read(addr, width) -val mem_read : forall 'n. (bits(64), atom('n), bool, bool, bool) -> bits(8 * 'n) effect {rmem, escape} +val mem_read : forall 'n. (xlenbits, atom('n), bool, bool, bool) -> bits(8 * 'n) effect {rmem, escape} function mem_read (addr, width, aq, rl, res) = { if aq | res then check_alignment(addr, width); @@ -122,19 +85,19 @@ function mem_read (addr, width, aq, rl, res) = { } val MEMea = {ocaml: "memea", lem: "MEMea"} : forall 'n. - (bits(64), atom('n)) -> unit effect {eamem} + (xlenbits, atom('n)) -> unit effect {eamem} val MEMea_release = {ocaml: "memea", lem: "MEMea_release"} : forall 'n. - (bits(64), atom('n)) -> unit effect {eamem} + (xlenbits, atom('n)) -> unit effect {eamem} val MEMea_strong_release = {ocaml: "memea", lem: "MEMea_strong_release"} : forall 'n. - (bits(64), atom('n)) -> unit effect {eamem} + (xlenbits, atom('n)) -> unit effect {eamem} val MEMea_conditional = {ocaml: "memea", lem: "MEMea_conditional"} : forall 'n. - (bits(64), atom('n)) -> unit effect {eamem} + (xlenbits, atom('n)) -> unit effect {eamem} val MEMea_conditional_release = {ocaml: "memea", lem: "MEMea_conditional_release"} : forall 'n. - (bits(64), atom('n)) -> unit effect {eamem} + (xlenbits, atom('n)) -> unit effect {eamem} val MEMea_conditional_strong_release = {ocaml: "memea", lem: "MEMea_conditional_strong_release"} : forall 'n. - (bits(64), atom('n)) -> unit effect {eamem} + (xlenbits, atom('n)) -> unit effect {eamem} -val mem_write_ea : forall 'n. (bits(64), atom('n), bool, bool, bool) -> unit effect {eamem, escape} +val mem_write_ea : forall 'n. (xlenbits, atom('n), bool, bool, bool) -> unit effect {eamem, escape} function mem_write_ea (addr, width, aq, rl, con) = { if rl | con then check_alignment(addr, width); @@ -151,12 +114,12 @@ function mem_write_ea (addr, width, aq, rl, con) = { } } -val MEMval : forall 'n. (bits(64), atom('n), bits(8 * 'n)) -> unit effect {wmv} -val MEMval_release : forall 'n. (bits(64), atom('n), bits(8 * 'n)) -> unit effect {wmv} -val MEMval_strong_release : forall 'n. (bits(64), atom('n), bits(8 * 'n)) -> unit effect {wmv} -val MEMval_conditional : forall 'n. (bits(64), atom('n), bits(8 * 'n)) -> unit effect {wmv} -val MEMval_conditional_release : forall 'n. (bits(64), atom('n), bits(8 * 'n)) -> unit effect {wmv} -val MEMval_conditional_strong_release : forall 'n. (bits(64), atom('n), bits(8 * 'n)) -> unit effect {wmv} +val MEMval : forall 'n. (xlenbits, atom('n), bits(8 * 'n)) -> unit effect {wmv} +val MEMval_release : forall 'n. (xlenbits, atom('n), bits(8 * 'n)) -> unit effect {wmv} +val MEMval_strong_release : forall 'n. (xlenbits, atom('n), bits(8 * 'n)) -> unit effect {wmv} +val MEMval_conditional : forall 'n. (xlenbits, atom('n), bits(8 * 'n)) -> unit effect {wmv} +val MEMval_conditional_release : forall 'n. (xlenbits, atom('n), bits(8 * 'n)) -> unit effect {wmv} +val MEMval_conditional_strong_release : forall 'n. (xlenbits, atom('n), bits(8 * 'n)) -> unit effect {wmv} function MEMval (addr, width, data) = __RISCV_write(addr, width, data) function MEMval_release (addr, width, data) = __RISCV_write(addr, width, data) @@ -165,7 +128,7 @@ function MEMval_conditional (addr, width, data) = __RISCV_write(a function MEMval_conditional_release (addr, width, data) = __RISCV_write(addr, width, data) function MEMval_conditional_strong_release (addr, width, data) = __RISCV_write(addr, width, data) -val mem_write_value : forall 'n. (bits(64), atom('n), bits(8 * 'n), bool, bool, bool) -> unit effect {wmv, escape} +val mem_write_value : forall 'n. (xlenbits, atom('n), bits(8 * 'n), bool, bool, bool) -> unit effect {wmv, escape} function mem_write_value (addr, width, value, aq, rl, con) = { if rl | con then check_alignment(addr, width); @@ -203,10 +166,10 @@ enum word_width = {BYTE, HALF, WORD, DOUBLE} /* Ideally these would be sail builtin */ -function shift_right_arith64 (v : bits(64), shift : bits(6)) -> bits(64) = +function shift_right_arith64 (v : xlenbits, shift : bits(6)) -> xlenbits = let v128 : bits(128) = EXTS(v) in (v128 >> shift)[63..0] function shift_right_arith32 (v : bits(32), shift : bits(5)) -> bits(32) = - let v64 : bits(64) = EXTS(v) in + let v64 : xlenbits = EXTS(v) in (v64 >> shift)[31..0] |