diff options
Diffstat (limited to 'riscv')
| -rw-r--r-- | riscv/prelude.sail | 17 | ||||
| -rw-r--r-- | riscv/riscv.sail | 435 | ||||
| -rw-r--r-- | riscv/riscv_types.sail | 18 |
3 files changed, 235 insertions, 235 deletions
diff --git a/riscv/prelude.sail b/riscv/prelude.sail index b4e36507..ff11cf7e 100644 --- a/riscv/prelude.sail +++ b/riscv/prelude.sail @@ -276,9 +276,11 @@ val cast ex_int : int -> {'n, true. atom('n)} function ex_int 'n = n +/* val cast ex_range : forall 'n 'm. range('n, 'm) -> {'o, 'n <= 'o <= 'm. atom('o)} function ex_range (n as 'N) = n +*/ val coerce_int_nat : int -> nat effect {escape} @@ -297,6 +299,7 @@ val print_int = "print_int" : (string, int) -> unit union exception = { Error_not_implemented : string, Error_misaligned_access, + Error_EBREAK, } val EXTS : forall 'n 'm , 'm >= 'n . bits('n) -> bits('m) @@ -313,4 +316,16 @@ function operator <_u (x : bits('n), y : bits('n)) -> forall 'n. bool = unsigne function operator >=_u (x : bits('n), y : bits('n)) -> forall 'n. bool = unsigned(x) >= unsigned(y) val cast bool_to_bits : bool -> bits(1) -function bool_to_bits x = if x then 0b1 else 0b0
\ No newline at end of file +function bool_to_bits x = if x then 0b1 else 0b0 + +val cast bit_to_bool : bit -> bool +function bit_to_bool bitone = true +and bit_to_bool bitzero = false + +infix 7 >> +infix 7 << + +val operator >> : forall 'n 'm. (bits('n), bits('m)) -> bits('n) +val operator << : forall 'n 'm. (bits('n), bits('m)) -> bits('n) + +val vector64 : int -> bits(64)
\ No newline at end of file diff --git a/riscv/riscv.sail b/riscv/riscv.sail index 00dbb190..f05bb2be 100644 --- a/riscv/riscv.sail +++ b/riscv/riscv.sail @@ -3,10 +3,10 @@ scattered union ast val decode : bits(32) -> option(ast) effect pure scattered function decode -val execute : ast -> unit effect {escape, wreg, rreg} +val execute : ast -> unit effect {escape, wreg, rreg, wmv, eamem, rmem, barr, exmem} scattered function execute -/* *******************************************************************/ +/* ****************************************************************** */ union clause ast = UTYPE : (bits(20), regbits, uop) @@ -21,7 +21,7 @@ function clause execute UTYPE(imm, rd, op) = } in wGPR(rd, ret) -/* *******************************************************************/ +/* ****************************************************************** */ union clause ast = RISCV_JAL : (bits(21), regbits) @@ -34,7 +34,7 @@ function clause execute (RISCV_JAL(imm, rd)) = { nextPC = pc + offset; } -/* *******************************************************************/ +/* ****************************************************************** */ union clause ast = RISCV_JALR : (bits(12), regbits, regbits) function clause decode imm : bits(12) @ rs1 : regbits @ 0b000 @ rd : regbits @ 0b1100111 = @@ -47,7 +47,7 @@ function clause execute (RISCV_JALR(imm, rs1, rd)) = { nextPC = newPC[63..1] @ 0b0; } -/* *******************************************************************/ +/* ****************************************************************** */ union clause ast = BTYPE : (bits(13), regbits, regbits, bop) function clause decode imm7 : bits(7) @ rs2 : regbits @ rs1 : regbits @ 0b000 @ imm5 : bits(5) @ 0b1100011 = Some(BTYPE(imm7[6] @ imm5[0] @ imm7[5..0] @ imm5[4..1] @ 0b0, rs2, rs1, RISCV_BEQ)) @@ -71,7 +71,7 @@ function clause execute (BTYPE(imm, rs2, rs1, op)) = if taken then nextPC = PC + EXTS(imm) -/* *******************************************************************/ +/* ****************************************************************** */ union clause ast = ITYPE : (bits(12), regbits, regbits, iop) function clause decode imm : bits(12) @ rs1 : regbits @ 0b000 @ rd : regbits @ 0b0010011 = Some(ITYPE(imm, rs1, rd, RISCV_ADDI)) @@ -93,312 +93,299 @@ function clause execute (ITYPE (imm, rs1, rd, op)) = RISCV_ANDI => rs1_val & imm64 } in wGPR(rd, result) -/* -(********************************************************************) -union ast member ((bits(6)), regbits, regbits, sop) SHIFTIOP -function clause decode (0b000000 @ (bits(6)) shamt @ (regbits) rs1 @ 0b001 @ (regbits) rd @ 0b0010011) = Some(SHIFTIOP(shamt, rs1, rd, RISCV_SLLI)) -function clause decode (0b000000 @ (bits(6)) shamt @ (regbits) rs1 @ 0b101 @ (regbits) rd @ 0b0010011) = Some(SHIFTIOP(shamt, rs1, rd, RISCV_SRLI)) -function clause decode (0b010000 @ (bits(6)) shamt @ (regbits) rs1 @ 0b101 @ (regbits) rd @ 0b0010011) = Some(SHIFTIOP(shamt, rs1, rd, RISCV_SRAI)) +/* ****************************************************************** */ +union clause ast = SHIFTIOP : (bits(6), regbits, regbits, sop) + +function clause decode 0b000000 @ shamt : bits(6) @ rs1 : regbits @ 0b001 @ rd : regbits @ 0b0010011 = Some(SHIFTIOP(shamt, rs1, rd, RISCV_SLLI)) +function clause decode 0b000000 @ shamt : bits(6) @ rs1 : regbits @ 0b101 @ rd : regbits @ 0b0010011 = Some(SHIFTIOP(shamt, rs1, rd, RISCV_SRLI)) +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 = switch(op) { - case RISCV_SLLI -> rs1_val >> shamt - case RISCV_SRLI -> rs1_val << shamt - case RISCV_SRAI -> shift_right_arith64(rs1_val, shamt) + let result : bits(64) = match op { + RISCV_SLLI => rs1_val >> shamt, + RISCV_SRLI => rs1_val << shamt, + RISCV_SRAI => shift_right_arith64(rs1_val, shamt) } in wGPR(rd, result) -(********************************************************************) -union ast member (regbits, regbits, regbits, rop) RTYPE -function clause decode (0b0000000 @ (regbits) rs2 @ (regbits) rs1 @ 0b000 @ (regbits) rd @ 0b0110011) = Some(RTYPE(rs2, rs1, rd, RISCV_ADD)) -function clause decode (0b0100000 @ (regbits) rs2 @ (regbits) rs1 @ 0b000 @ (regbits) rd @ 0b0110011) = Some(RTYPE(rs2, rs1, rd, RISCV_SUB)) -function clause decode (0b0000000 @ (regbits) rs2 @ (regbits) rs1 @ 0b001 @ (regbits) rd @ 0b0110011) = Some(RTYPE(rs2, rs1, rd, RISCV_SLL)) -function clause decode (0b0000000 @ (regbits) rs2 @ (regbits) rs1 @ 0b010 @ (regbits) rd @ 0b0110011) = Some(RTYPE(rs2, rs1, rd, RISCV_SLT)) -function clause decode (0b0000000 @ (regbits) rs2 @ (regbits) rs1 @ 0b011 @ (regbits) rd @ 0b0110011) = Some(RTYPE(rs2, rs1, rd, RISCV_SLTU)) -function clause decode (0b0000000 @ (regbits) rs2 @ (regbits) rs1 @ 0b100 @ (regbits) rd @ 0b0110011) = Some(RTYPE(rs2, rs1, rd, RISCV_XOR)) -function clause decode (0b0000000 @ (regbits) rs2 @ (regbits) rs1 @ 0b101 @ (regbits) rd @ 0b0110011) = Some(RTYPE(rs2, rs1, rd, RISCV_SRL)) -function clause decode (0b0100000 @ (regbits) rs2 @ (regbits) rs1 @ 0b101 @ (regbits) rd @ 0b0110011) = Some(RTYPE(rs2, rs1, rd, RISCV_SRA)) -function clause decode (0b0000000 @ (regbits) rs2 @ (regbits) rs1 @ 0b110 @ (regbits) rd @ 0b0110011) = Some(RTYPE(rs2, rs1, rd, RISCV_OR)) -function clause decode (0b0000000 @ (regbits) rs2 @ (regbits) rs1 @ 0b111 @ (regbits) rd @ 0b0110011) = Some(RTYPE(rs2, rs1, rd, RISCV_AND)) +/* ****************************************************************** */ +union clause ast = RTYPE : (regbits, regbits, regbits, rop) + +function clause decode 0b0000000 @ rs2 : regbits @ rs1 : regbits @ 0b000 @ rd : regbits @ 0b0110011 = Some(RTYPE(rs2, rs1, rd, RISCV_ADD)) +function clause decode 0b0100000 @ rs2 : regbits @ rs1 : regbits @ 0b000 @ rd : regbits @ 0b0110011 = Some(RTYPE(rs2, rs1, rd, RISCV_SUB)) +function clause decode 0b0000000 @ rs2 : regbits @ rs1 : regbits @ 0b001 @ rd : regbits @ 0b0110011 = Some(RTYPE(rs2, rs1, rd, RISCV_SLL)) +function clause decode 0b0000000 @ rs2 : regbits @ rs1 : regbits @ 0b010 @ rd : regbits @ 0b0110011 = Some(RTYPE(rs2, rs1, rd, RISCV_SLT)) +function clause decode 0b0000000 @ rs2 : regbits @ rs1 : regbits @ 0b011 @ rd : regbits @ 0b0110011 = Some(RTYPE(rs2, rs1, rd, RISCV_SLTU)) +function clause decode 0b0000000 @ rs2 : regbits @ rs1 : regbits @ 0b100 @ rd : regbits @ 0b0110011 = Some(RTYPE(rs2, rs1, rd, RISCV_XOR)) +function clause decode 0b0000000 @ rs2 : regbits @ rs1 : regbits @ 0b101 @ rd : regbits @ 0b0110011 = Some(RTYPE(rs2, rs1, rd, RISCV_SRL)) +function clause decode 0b0100000 @ rs2 : regbits @ rs1 : regbits @ 0b101 @ rd : regbits @ 0b0110011 = Some(RTYPE(rs2, rs1, rd, RISCV_SRA)) +function clause decode 0b0000000 @ rs2 : regbits @ rs1 : regbits @ 0b110 @ rd : regbits @ 0b0110011 = Some(RTYPE(rs2, rs1, rd, RISCV_OR)) +function clause decode 0b0000000 @ rs2 : regbits @ rs1 : regbits @ 0b111 @ rd : regbits @ 0b0110011 = Some(RTYPE(rs2, rs1, rd, RISCV_AND)) + function clause execute (RTYPE(rs2, rs1, rd, op)) = let rs1_val = rGPR(rs1) in let rs2_val = rGPR(rs2) in - let (bits(64)) result = switch(op) { - case RISCV_ADD -> rs1_val + rs2_val - case RISCV_SUB -> rs1_val - rs2_val - case RISCV_SLL -> rs1_val << (rs2_val[5..0]) - case RISCV_SLT -> EXTZ(rs1_val <_s rs2_val) - case RISCV_SLTU -> EXTZ(rs1_val <_u rs2_val) - case RISCV_XOR -> rs1_val ^ rs2_val - case RISCV_SRL -> rs1_val >> (rs2_val[5..0]) - case RISCV_SRA -> shift_right_arith64(rs1_val, rs2_val[5..0]) - case RISCV_OR -> rs1_val | rs2_val - case RISCV_AND -> rs1_val & rs2_val + let result : bits(64) = match op { + RISCV_ADD => rs1_val + rs2_val, + RISCV_SUB => rs1_val - rs2_val, + RISCV_SLL => rs1_val << (rs2_val[5..0]), + RISCV_SLT => EXTZ(rs1_val <_s rs2_val), + RISCV_SLTU => EXTZ(rs1_val <_u rs2_val), + RISCV_XOR => rs1_val ^ rs2_val, + RISCV_SRL => rs1_val >> (rs2_val[5..0]), + RISCV_SRA => shift_right_arith64(rs1_val, rs2_val[5..0]), + RISCV_OR => rs1_val | rs2_val, + RISCV_AND => rs1_val & rs2_val } in wGPR(rd, result) -(********************************************************************) -union ast member ((bits(12)), regbits, regbits, bool, word_width, bool, bool) LOAD +/* ****************************************************************** */ +union clause ast = LOAD : (bits(12), regbits, regbits, bool, word_width, bool, bool) + +function clause decode imm : bits(12) @ rs1 : regbits @ 0b000 @ rd : regbits @ 0b0000011 = Some(LOAD(imm, rs1, rd, false, BYTE, false, false)) +function clause decode imm : bits(12) @ rs1 : regbits @ 0b001 @ rd : regbits @ 0b0000011 = Some(LOAD(imm, rs1, rd, false, HALF, false, false)) +function clause decode imm : bits(12) @ rs1 : regbits @ 0b010 @ rd : regbits @ 0b0000011 = Some(LOAD(imm, rs1, rd, false, WORD, false, false)) +function clause decode imm : bits(12) @ rs1 : regbits @ 0b011 @ rd : regbits @ 0b0000011 = Some(LOAD(imm, rs1, rd, false, DOUBLE, false, false)) +function clause decode imm : bits(12) @ rs1 : regbits @ 0b100 @ rd : regbits @ 0b0000011 = Some(LOAD(imm, rs1, rd, true, BYTE, false, false)) +function clause decode imm : bits(12) @ rs1 : regbits @ 0b101 @ rd : regbits @ 0b0000011 = Some(LOAD(imm, rs1, rd, true, HALF, false, false)) +function clause decode imm : bits(12) @ rs1 : regbits @ 0b110 @ rd : regbits @ 0b0000011 = Some(LOAD(imm, rs1, rd, true, WORD, false, false)) -function clause decode ((bits(12)) imm @ (regbits) rs1 @ 0b000 @ (regbits) rd @ 0b0000011) = Some(LOAD(imm, rs1, rd, false, BYTE, false, false)) -function clause decode ((bits(12)) imm @ (regbits) rs1 @ 0b001 @ (regbits) rd @ 0b0000011) = Some(LOAD(imm, rs1, rd, false, HALF, false, false)) -function clause decode ((bits(12)) imm @ (regbits) rs1 @ 0b010 @ (regbits) rd @ 0b0000011) = Some(LOAD(imm, rs1, rd, false, WORD, false, false)) -function clause decode ((bits(12)) imm @ (regbits) rs1 @ 0b011 @ (regbits) rd @ 0b0000011) = Some(LOAD(imm, rs1, rd, false, DOUBLE, false, false)) -function clause decode ((bits(12)) imm @ (regbits) rs1 @ 0b100 @ (regbits) rd @ 0b0000011) = Some(LOAD(imm, rs1, rd, true, BYTE, false, false)) -function clause decode ((bits(12)) imm @ (regbits) rs1 @ 0b101 @ (regbits) rd @ 0b0000011) = Some(LOAD(imm, rs1, rd, true, HALF, false, false)) -function clause decode ((bits(12)) imm @ (regbits) rs1 @ 0b110 @ (regbits) rd @ 0b0000011) = Some(LOAD(imm, rs1, rd, true, WORD, false, false)) function clause execute(LOAD(imm, rs1, rd, unsigned, width, aq, rl)) = - let (bits(64)) addr = rGPR(rs1) + EXTS(imm) in - let (bits(64)) result = if unsigned then - switch (width) { - case BYTE -> EXTZ(mem_read(addr, 1, aq, rl, false)) - case HALF -> EXTZ(mem_read(addr, 2, aq, rl, false)) - case WORD -> EXTZ(mem_read(addr, 4, aq, rl, false)) - case DOUBLE -> mem_read(addr, 8, aq, rl, false) + let addr : bits(64) = rGPR(rs1) + EXTS(imm) in + let result : bits(64) = if unsigned then + match width { + BYTE => EXTZ(mem_read(addr, 1, aq, rl, false)), + HALF => EXTZ(mem_read(addr, 2, aq, rl, false)), + WORD => EXTZ(mem_read(addr, 4, aq, rl, false)), + DOUBLE => mem_read(addr, 8, aq, rl, false) } else - switch (width) { - case BYTE -> EXTS(mem_read(addr, 1, aq, rl, false)) - case HALF -> EXTS(mem_read(addr, 2, aq, rl, false)) - case WORD -> EXTS(mem_read(addr, 4, aq, rl, false)) - case DOUBLE -> mem_read(addr, 8, aq, rl, false) + match width { + BYTE => EXTS(mem_read(addr, 1, aq, rl, false)), + HALF => EXTS(mem_read(addr, 2, aq, rl, false)), + WORD => EXTS(mem_read(addr, 4, aq, rl, false)), + DOUBLE => mem_read(addr, 8, aq, rl, false) } in wGPR(rd, result) -(********************************************************************) -union ast member ((bits(12)), regbits, regbits, word_width, bool, bool) STORE +/* ****************************************************************** */ +union clause ast = STORE : (bits(12), regbits, regbits, word_width, bool, bool) -function clause decode ((bits(7)) imm7 @ (regbits) rs2 @ (regbits) rs1 @ 0b000 @ (bits(5)) imm5 @ 0b0100011) = - Some(STORE(imm7 @ imm5, rs2, rs1, BYTE, false, false)) -function clause decode ((bits(7)) imm7 @ (regbits) rs2 @ (regbits) rs1 @ 0b001 @ (bits(5)) imm5 @ 0b0100011) = - Some(STORE(imm7 @ imm5, rs2, rs1, HALF, false, false)) -function clause decode ((bits(7)) imm7 @ (regbits) rs2 @ (regbits) rs1 @ 0b010 @ (bits(5)) imm5 @ 0b0100011) = - Some(STORE(imm7 @ imm5, rs2, rs1, WORD, false, false)) -function clause decode ((bits(7)) imm7 @ (regbits) rs2 @ (regbits) rs1 @ 0b011 @ (bits(5)) imm5 @ 0b0100011) = - Some(STORE(imm7 @ imm5, rs2, rs1, DOUBLE, false, false)) +function clause decode imm7 : bits(7) @ rs2 : regbits @ rs1 : regbits @ 0b000 @ imm5 : bits(5) @ 0b0100011 = Some(STORE(imm7 @ imm5, rs2, rs1, BYTE, false, false)) +function clause decode imm7 : bits(7) @ rs2 : regbits @ rs1 : regbits @ 0b001 @ imm5 : bits(5) @ 0b0100011 = Some(STORE(imm7 @ imm5, rs2, rs1, HALF, false, false)) +function clause decode imm7 : bits(7) @ rs2 : regbits @ rs1 : regbits @ 0b010 @ imm5 : bits(5) @ 0b0100011 = Some(STORE(imm7 @ imm5, rs2, rs1, WORD, false, false)) +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 (bits(64)) addr = rGPR(rs1) + EXTS(imm) in { - switch (width) { - case BYTE -> mem_write_ea(addr, 1, aq, rl, false) - case HALF -> mem_write_ea(addr, 2, aq, rl, false) - case WORD -> mem_write_ea(addr, 4, aq, rl, false) - case DOUBLE -> mem_write_ea(addr, 8, aq, rl, false) + let addr : bits(64) = rGPR(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 - switch (width) { - case BYTE -> mem_write_value(addr, 1, rs2_val[7..0], aq, rl, false) - case HALF -> mem_write_value(addr, 2, rs2_val[15..0], aq, rl, false) - case WORD -> mem_write_value(addr, 4, rs2_val[31..0], aq, rl, false) - case DOUBLE -> mem_write_value(addr, 8, rs2_val, aq, rl, false) + 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), + WORD => mem_write_value(addr, 4, rs2_val[31..0], aq, rl, false), + DOUBLE => mem_write_value(addr, 8, rs2_val, aq, rl, false) } } -(********************************************************************) -union ast member ((bits(12)), regbits, regbits) ADDIW -function clause decode ((bits(12)) imm @ (regbits) rs1 @ 0b000 @ (regbits) rd @ 0b0011011) = - Some(ADDIW(imm, rs1, rd)) +/* ****************************************************************** */ +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 (bits(64)) imm64 = EXTS(imm) in - let (bits(64)) result64 = imm64 + rGPR(rs1) in - let (bits(64)) result32 = EXTS(result64[31..0]) in + 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) -(********************************************************************) -union ast member ((bits(5)), regbits, regbits, sop) SHIFTW +/* ****************************************************************** */ +union clause ast = SHIFTW : (bits(5), regbits, regbits, sop) -function clause decode (0b0000000 @ (bits(5)) shamt @ (regbits) rs1 @ 0b001 @ (regbits) rd @ 0b0011011) = Some(SHIFTW(shamt, rs1, rd, RISCV_SLLI)) -function clause decode (0b0000000 @ (bits(5)) shamt @ (regbits) rs1 @ 0b101 @ (regbits) rd @ 0b0011011) = Some(SHIFTW(shamt, rs1, rd, RISCV_SRLI)) -function clause decode (0b0100000 @ (bits(5)) shamt @ (regbits) rs1 @ 0b101 @ (regbits) rd @ 0b0011011) = Some(SHIFTW(shamt, rs1, rd, RISCV_SRAI)) +function clause decode 0b0000000 @ shamt : bits(5) @ rs1 : regbits @ 0b001 @ rd : regbits @ 0b0011011 = Some(SHIFTW(shamt, rs1, rd, RISCV_SLLI)) +function clause decode 0b0000000 @ shamt : bits(5) @ rs1 : regbits @ 0b101 @ rd : regbits @ 0b0011011 = Some(SHIFTW(shamt, rs1, rd, RISCV_SRLI)) +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)) = +function clause execute (SHIFTW(shamt, rs1, rd, op)) = let rs1_val = (rGPR(rs1))[31..0] in - let result = switch(op) { - case RISCV_SLLI -> rs1_val >> shamt - case RISCV_SRLI -> rs1_val << shamt - case RISCV_SRAI -> shift_right_arith32(rs1_val, shamt) + 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)) -(********************************************************************) -union ast member (regbits, regbits, regbits, ropw) RTYPEW +/* ****************************************************************** */ +union clause ast = RTYPEW : (regbits, regbits, regbits, ropw) -function clause decode (0b0000000 @ (regbits) rs2 @ (regbits) rs1 @ 0b000 @ (regbits) rd @ 0b0111011) = Some(RTYPEW(rs2, rs1, rd, RISCV_ADDW)) -function clause decode (0b0100000 @ (regbits) rs2 @ (regbits) rs1 @ 0b000 @ (regbits) rd @ 0b0111011) = Some(RTYPEW(rs2, rs1, rd, RISCV_SUBW)) -function clause decode (0b0000000 @ (regbits) rs2 @ (regbits) rs1 @ 0b001 @ (regbits) rd @ 0b0111011) = Some(RTYPEW(rs2, rs1, rd, RISCV_SLLW)) -function clause decode (0b0000000 @ (regbits) rs2 @ (regbits) rs1 @ 0b101 @ (regbits) rd @ 0b0111011) = Some(RTYPEW(rs2, rs1, rd, RISCV_SRLW)) -function clause decode (0b0100000 @ (regbits) rs2 @ (regbits) rs1 @ 0b101 @ (regbits) rd @ 0b0111011) = Some(RTYPEW(rs2, rs1, rd, RISCV_SRAW)) +function clause decode 0b0000000 @ rs2 : regbits @ rs1 : regbits @ 0b000 @ rd : regbits @ 0b0111011 = Some(RTYPEW(rs2, rs1, rd, RISCV_ADDW)) +function clause decode 0b0100000 @ rs2 : regbits @ rs1 : regbits @ 0b000 @ rd : regbits @ 0b0111011 = Some(RTYPEW(rs2, rs1, rd, RISCV_SUBW)) +function clause decode 0b0000000 @ rs2 : regbits @ rs1 : regbits @ 0b001 @ rd : regbits @ 0b0111011 = Some(RTYPEW(rs2, rs1, rd, RISCV_SLLW)) +function clause decode 0b0000000 @ rs2 : regbits @ rs1 : regbits @ 0b101 @ rd : regbits @ 0b0111011 = Some(RTYPEW(rs2, rs1, rd, RISCV_SRLW)) +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 (bits(32)) result = switch(op) { - case RISCV_ADDW -> rs1_val + rs2_val - case RISCV_SUBW -> rs1_val - rs2_val - case RISCV_SLLW -> rs1_val << (rs2_val[4..0]) - case RISCV_SRLW -> rs1_val >> (rs2_val[4..0]) - case RISCV_SRAW -> shift_right_arith32(rs1_val, rs2_val[4..0]) + let result : bits(32) = match op { + RISCV_ADDW => rs1_val + rs2_val, + RISCV_SUBW => rs1_val - rs2_val, + RISCV_SLLW => rs1_val << (rs2_val[4..0]), + RISCV_SRLW => rs1_val >> (rs2_val[4..0]), + RISCV_SRAW => shift_right_arith32(rs1_val, rs2_val[4..0]) } in wGPR(rd, EXTS(result)) -(********************************************************************) -union ast member (bits(4), bits(4)) FENCE +/* ****************************************************************** */ +union clause ast = FENCE : (bits(4), bits(4)) -function clause decode (0b0000 @ (bits(4)) pred @ (bits(4)) succ @ 0b00000 @ 0b000 @ 0b00000 @ 0b0001111) = Some(FENCE (pred, succ)) +function clause decode 0b0000 @ pred : bits(4) @ succ : bits(4) @ 0b00000 @ 0b000 @ 0b00000 @ 0b0001111 = Some(FENCE(pred, succ)) function clause execute (FENCE(pred, succ)) = { - switch(pred, succ) { - case (0b0011, 0b0011) -> MEM_fence_rw_rw() - case (0b0010, 0b0011) -> MEM_fence_r_rw() - case (0b0010, 0b0010) -> MEM_fence_r_r() - case (0b0011, 0b0001) -> MEM_fence_rw_w() - case (0b0001, 0b0001) -> MEM_fence_w_w() - case _ -> not_implemented("unsupported fence") + match (pred, succ) { + (0b0011, 0b0011) => MEM_fence_rw_rw(), + (0b0010, 0b0011) => MEM_fence_r_rw(), + (0b0010, 0b0010) => MEM_fence_r_r(), + (0b0011, 0b0001) => MEM_fence_rw_w(), + (0b0001, 0b0001) => MEM_fence_w_w(), + _ => not_implemented("unsupported fence") } } -(********************************************************************) -union ast member unit FENCEI -function clause decode (0b000000000000 @ 0b00000 @ 0b001 @ 0b00000 @ 0b0001111) = Some(FENCEI) +/* ****************************************************************** */ +union clause ast = FENCEI + +function clause decode 0b000000000000 @ 0b00000 @ 0b001 @ 0b00000 @ 0b0001111 = Some(FENCEI) + function clause execute FENCEI = MEM_fence_i() -(********************************************************************) -union ast member unit ECALL -function clause decode (0b000000000000 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011) = Some(ECALL ()) +/* ****************************************************************** */ +union clause ast = ECALL + +function clause decode 0b000000000000 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011 = Some(ECALL) + function clause execute ECALL = not_implemented("ECALL is not implemented") -(********************************************************************) -union ast member unit EBREAK -function clause decode (0b000000000001 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011) = Some(EBREAK ()) -function clause execute EBREAK = { exit () } +/* ****************************************************************** */ +union clause ast = EBREAK + +function clause decode 0b000000000001 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011 = Some(EBREAK) -(********************************************************************) -union ast member (bool, bool, regbits, word_width, regbits) LOADRES +function clause execute EBREAK = { throw(Error_EBREAK) } + +/* ****************************************************************** */ +union clause ast = LOADRES : (bool, bool, regbits, word_width, regbits) + +function clause decode 0b00010 @ [aq] @ [rl] @ 0b00000 @ rs1 : regbits @ 0b010 @ rd : regbits @ 0b0101111 = Some(LOADRES(aq, rl, rs1, WORD, rd)) +function clause decode 0b00010 @ [aq] @ [rl] @ 0b00000 @ rs1 : regbits @ 0b011 @ rd : regbits @ 0b0101111 = Some(LOADRES(aq, rl, rs1, DOUBLE, rd)) -function clause decode (0b00010 @ [aq] @ [rl] @ 0b00000 @ (regbits) rs1 @ 0b010 @ (regbits) rd @ 0b0101111) = Some(LOADRES(aq, rl, rs1, WORD, rd)) -function clause decode (0b00010 @ [aq] @ [rl] @ 0b00000 @ (regbits) rs1 @ 0b011 @ (regbits) rd @ 0b0101111) = Some(LOADRES(aq, rl, rs1, DOUBLE, rd)) function clause execute(LOADRES(aq, rl, rs1, width, rd)) = - let (bits(64)) addr = rGPR(rs1) in - let (bits(64)) result = - switch width { - case WORD -> EXTS(mem_read(addr, 4, aq, rl, true)) - case DOUBLE -> mem_read(addr, 8, aq, rl, true) + let addr : bits(64) = rGPR(rs1) in + let result : bits(64) = + match width { + WORD => EXTS(mem_read(addr, 4, aq, rl, true)), + DOUBLE => mem_read(addr, 8, aq, rl, true) } in wGPR(rd, result) -(********************************************************************) -union ast member (bool, bool, regbits, regbits, word_width, regbits) STORECON +/* ****************************************************************** */ +union clause ast = STORECON : (bool, bool, regbits, regbits, word_width, regbits) -function clause decode (0b00011 @ [aq] @ [rl] @ (regbits) rs2 @ (regbits) rs1 @ 0b010 @ (regbits) rd @ 0b0101111) = - Some(STORECON(aq, rl, rs2, rs1, WORD, rd)) -function clause decode (0b00011 @ [aq] @ [rl] @ (regbits) rs2 @ (regbits) rs1 @ 0b011 @ (regbits) rd @ 0b0101111) = - Some(STORECON(aq, rl, rs2, rs1, DOUBLE, rd)) +function clause decode 0b00011 @ [aq] @ [rl] @ rs2 : regbits @ rs1 : regbits @ 0b010 @ rd : regbits @ 0b0101111 = Some(STORECON(aq, rl, rs2, rs1, WORD, rd)) +function clause decode 0b00011 @ [aq] @ [rl] @ rs2 : regbits @ rs1 : regbits @ 0b011 @ rd : regbits @ 0b0101111 = Some(STORECON(aq, rl, rs2, rs1, DOUBLE, rd)) function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = { - (*(bit)*) status = if speculate_conditional_success() then 0 else 1; - wGPR(rd) = (bits(64)) (EXTZ([status])); - - if status == 1 then () else { - (bits(64)) addr = rGPR(rs1); - switch width { - case WORD -> mem_write_ea(addr, 4, aq, rl, true) - case DOUBLE -> mem_write_ea(addr, 8, aq, rl, true) + status : bits(1) = if speculate_conditional_success() then 0b0 else 0b1; + wGPR(rd) = EXTZ(status); + + if status == 0b1 then () else { + addr : bits(64) = rGPR(rs1); + match width { + WORD => mem_write_ea(addr, 4, aq, rl, true), + DOUBLE => mem_write_ea(addr, 8, aq, rl, true) }; rs2_val = rGPR(rs2); - switch width { - case WORD -> mem_write_value(addr, 4, rs2_val[31..0], aq, rl, true) - case DOUBLE -> mem_write_value(addr, 8, rs2_val, aq, rl, true) + 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) }; }; } -(********************************************************************) -union ast member (amoop, bool, bool, regbits, regbits, word_width, regbits) AMO - -function clause decode (0b00001 @ [aq] @ [rl] @ (regbits) rs2 @ (regbits) rs1 @ 0b010 @ (regbits) rd @ 0b0101111) = - Some(AMO(AMOSWAP, aq, rl, rs2, rs1, WORD, rd)) -function clause decode (0b00001 @ [aq] @ [rl] @ (regbits) rs2 @ (regbits) rs1 @ 0b011 @ (regbits) rd @ 0b0101111) = - Some(AMO(AMOSWAP, aq, rl, rs2, rs1, DOUBLE, rd)) -function clause decode (0b00000 @ [aq] @ [rl] @ (regbits) rs2 @ (regbits) rs1 @ 0b010 @ (regbits) rd @ 0b0101111) = - Some(AMO(AMOADD , aq, rl, rs2, rs1, WORD, rd)) -function clause decode (0b00000 @ [aq] @ [rl] @ (regbits) rs2 @ (regbits) rs1 @ 0b011 @ (regbits) rd @ 0b0101111) = - Some(AMO(AMOADD , aq, rl, rs2, rs1, DOUBLE, rd)) -function clause decode (0b00100 @ [aq] @ [rl] @ (regbits) rs2 @ (regbits) rs1 @ 0b010 @ (regbits) rd @ 0b0101111) = - Some(AMO(AMOXOR , aq, rl, rs2, rs1, WORD, rd)) -function clause decode (0b00100 @ [aq] @ [rl] @ (regbits) rs2 @ (regbits) rs1 @ 0b011 @ (regbits) rd @ 0b0101111) = - Some(AMO(AMOXOR , aq, rl, rs2, rs1, DOUBLE, rd)) -function clause decode (0b01100 @ [aq] @ [rl] @ (regbits) rs2 @ (regbits) rs1 @ 0b010 @ (regbits) rd @ 0b0101111) = - Some(AMO(AMOAND , aq, rl, rs2, rs1, WORD, rd)) -function clause decode (0b01100 @ [aq] @ [rl] @ (regbits) rs2 @ (regbits) rs1 @ 0b011 @ (regbits) rd @ 0b0101111) = - Some(AMO(AMOAND , aq, rl, rs2, rs1, DOUBLE, rd)) -function clause decode (0b01000 @ [aq] @ [rl] @ (regbits) rs2 @ (regbits) rs1 @ 0b010 @ (regbits) rd @ 0b0101111) = - Some(AMO(AMOOR , aq, rl, rs2, rs1, WORD, rd)) -function clause decode (0b01000 @ [aq] @ [rl] @ (regbits) rs2 @ (regbits) rs1 @ 0b011 @ (regbits) rd @ 0b0101111) = - Some(AMO(AMOOR , aq, rl, rs2, rs1, DOUBLE, rd)) -function clause decode (0b10000 @ [aq] @ [rl] @ (regbits) rs2 @ (regbits) rs1 @ 0b010 @ (regbits) rd @ 0b0101111) = - Some(AMO(AMOMIN , aq, rl, rs2, rs1, WORD, rd)) -function clause decode (0b10000 @ [aq] @ [rl] @ (regbits) rs2 @ (regbits) rs1 @ 0b011 @ (regbits) rd @ 0b0101111) = - Some(AMO(AMOMIN , aq, rl, rs2, rs1, DOUBLE, rd)) -function clause decode (0b10100 @ [aq] @ [rl] @ (regbits) rs2 @ (regbits) rs1 @ 0b010 @ (regbits) rd @ 0b0101111) = - Some(AMO(AMOMAX , aq, rl, rs2, rs1, WORD, rd)) -function clause decode (0b10100 @ [aq] @ [rl] @ (regbits) rs2 @ (regbits) rs1 @ 0b011 @ (regbits) rd @ 0b0101111) = - Some(AMO(AMOMAX , aq, rl, rs2, rs1, DOUBLE, rd)) -function clause decode (0b11000 @ [aq] @ [rl] @ (regbits) rs2 @ (regbits) rs1 @ 0b010 @ (regbits) rd @ 0b0101111) = - Some(AMO(AMOMINU, aq, rl, rs2, rs1, WORD, rd)) -function clause decode (0b11000 @ [aq] @ [rl] @ (regbits) rs2 @ (regbits) rs1 @ 0b011 @ (regbits) rd @ 0b0101111) = - Some(AMO(AMOMINU, aq, rl, rs2, rs1, DOUBLE, rd)) -function clause decode (0b11100 @ [aq] @ [rl] @ (regbits) rs2 @ (regbits) rs1 @ 0b010 @ (regbits) rd @ 0b0101111) = - Some(AMO(AMOMAXU, aq, rl, rs2, rs1, WORD, rd)) -function clause decode (0b11100 @ [aq] @ [rl] @ (regbits) rs2 @ (regbits) rs1 @ 0b011 @ (regbits) rd @ 0b0101111) = - Some(AMO(AMOMAXU, aq, rl, rs2, rs1, DOUBLE, rd)) +/* ****************************************************************** */ +union clause ast = AMO : (amoop, bool, bool, regbits, regbits, word_width, regbits) + +function clause decode 0b00001 @ [aq] @ [rl] @ rs2 : regbits @ rs1 : regbits @ 0b010 @ rd : regbits @ 0b0101111 = Some(AMO(AMOSWAP, aq, rl, rs2, rs1, WORD, rd)) +function clause decode 0b00001 @ [aq] @ [rl] @ rs2 : regbits @ rs1 : regbits @ 0b011 @ rd : regbits @ 0b0101111 = Some(AMO(AMOSWAP, aq, rl, rs2, rs1, DOUBLE, rd)) +function clause decode 0b00000 @ [aq] @ [rl] @ rs2 : regbits @ rs1 : regbits @ 0b010 @ rd : regbits @ 0b0101111 = Some(AMO(AMOADD , aq, rl, rs2, rs1, WORD, rd)) +function clause decode 0b00000 @ [aq] @ [rl] @ rs2 : regbits @ rs1 : regbits @ 0b011 @ rd : regbits @ 0b0101111 = Some(AMO(AMOADD , aq, rl, rs2, rs1, DOUBLE, rd)) +function clause decode 0b00100 @ [aq] @ [rl] @ rs2 : regbits @ rs1 : regbits @ 0b010 @ rd : regbits @ 0b0101111 = Some(AMO(AMOXOR , aq, rl, rs2, rs1, WORD, rd)) +function clause decode 0b00100 @ [aq] @ [rl] @ rs2 : regbits @ rs1 : regbits @ 0b011 @ rd : regbits @ 0b0101111 = Some(AMO(AMOXOR , aq, rl, rs2, rs1, DOUBLE, rd)) +function clause decode 0b01100 @ [aq] @ [rl] @ rs2 : regbits @ rs1 : regbits @ 0b010 @ rd : regbits @ 0b0101111 = Some(AMO(AMOAND , aq, rl, rs2, rs1, WORD, rd)) +function clause decode 0b01100 @ [aq] @ [rl] @ rs2 : regbits @ rs1 : regbits @ 0b011 @ rd : regbits @ 0b0101111 = Some(AMO(AMOAND , aq, rl, rs2, rs1, DOUBLE, rd)) +function clause decode 0b01000 @ [aq] @ [rl] @ rs2 : regbits @ rs1 : regbits @ 0b010 @ rd : regbits @ 0b0101111 = Some(AMO(AMOOR , aq, rl, rs2, rs1, WORD, rd)) +function clause decode 0b01000 @ [aq] @ [rl] @ rs2 : regbits @ rs1 : regbits @ 0b011 @ rd : regbits @ 0b0101111 = Some(AMO(AMOOR , aq, rl, rs2, rs1, DOUBLE, rd)) +function clause decode 0b10000 @ [aq] @ [rl] @ rs2 : regbits @ rs1 : regbits @ 0b010 @ rd : regbits @ 0b0101111 = Some(AMO(AMOMIN , aq, rl, rs2, rs1, WORD, rd)) +function clause decode 0b10000 @ [aq] @ [rl] @ rs2 : regbits @ rs1 : regbits @ 0b011 @ rd : regbits @ 0b0101111 = Some(AMO(AMOMIN , aq, rl, rs2, rs1, DOUBLE, rd)) +function clause decode 0b10100 @ [aq] @ [rl] @ rs2 : regbits @ rs1 : regbits @ 0b010 @ rd : regbits @ 0b0101111 = Some(AMO(AMOMAX , aq, rl, rs2, rs1, WORD, rd)) +function clause decode 0b10100 @ [aq] @ [rl] @ rs2 : regbits @ rs1 : regbits @ 0b011 @ rd : regbits @ 0b0101111 = Some(AMO(AMOMAX , aq, rl, rs2, rs1, DOUBLE, rd)) +function clause decode 0b11000 @ [aq] @ [rl] @ rs2 : regbits @ rs1 : regbits @ 0b010 @ rd : regbits @ 0b0101111 = Some(AMO(AMOMINU, aq, rl, rs2, rs1, WORD, rd)) +function clause decode 0b11000 @ [aq] @ [rl] @ rs2 : regbits @ rs1 : regbits @ 0b011 @ rd : regbits @ 0b0101111 = Some(AMO(AMOMINU, aq, rl, rs2, rs1, DOUBLE, rd)) +function clause decode 0b11100 @ [aq] @ [rl] @ rs2 : regbits @ rs1 : regbits @ 0b010 @ rd : regbits @ 0b0101111 = Some(AMO(AMOMAXU, aq, rl, rs2, rs1, WORD, rd)) +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)) = { - (bits(64)) addr = rGPR(rs1); + addr : bits(64) = rGPR(rs1); - switch (width) { - case WORD -> mem_write_ea(addr, 4, aq & rl, rl, true) - case DOUBLE -> mem_write_ea(addr, 8, aq & rl, rl, true) + match width { + WORD => mem_write_ea(addr, 4, aq & rl, rl, true), + DOUBLE => mem_write_ea(addr, 8, aq & rl, rl, true) }; - (bits(64)) loaded = - switch (width) { - case WORD -> EXTS(mem_read(addr, 4, aq, aq & rl, true)) - case DOUBLE -> mem_read(addr, 8, aq, aq & rl, true) + loaded : bits(64) = + match width { + WORD => EXTS(mem_read(addr, 4, aq, aq & rl, true)), + DOUBLE => mem_read(addr, 8, aq, aq & rl, true) }; - wGPR(rd, loaded); - - (bits(64)) rs2_val = rGPR(rs2); - (bits(64)) result = - switch(op) { - case AMOSWAP -> rs2_val - case AMOADD -> rs2_val + loaded - case AMOXOR -> rs2_val ^ loaded - case AMOAND -> rs2_val & loaded - case AMOOR -> rs2_val | loaded - - case AMOMIN -> (bits(64)) (min(signed(rs2_val), signed(loaded))) - case AMOMAX -> (bits(64)) (max(signed(rs2_val), signed(loaded))) - case AMOMINU -> (bits(64)) (min(unsigned(rs2_val), unsigned(loaded))) - case AMOMAXU -> (bits(64)) (max(unsigned(rs2_val), unsigned(loaded))) + wGPR(rd) = loaded; + + rs2_val : bits(64) = rGPR(rs2); + result : bits(64) = + match op { + AMOSWAP => rs2_val, + AMOADD => rs2_val + loaded, + AMOXOR => rs2_val ^ loaded, + AMOAND => rs2_val & loaded, + AMOOR => rs2_val | loaded, + + /* Have to convert number to vector here. Check this */ + AMOMIN => vector64(min(signed(rs2_val), signed(loaded))), + AMOMAX => vector64(max(signed(rs2_val), signed(loaded))), + AMOMINU => vector64(min(unsigned(rs2_val), unsigned(loaded))), + AMOMAXU => vector64(max(unsigned(rs2_val), unsigned(loaded))) }; - switch (width) { - case WORD -> mem_write_value(addr, 4, result[31..0], aq & rl, rl, true) - case DOUBLE -> mem_write_value(addr, 8, result, aq & rl, rl, true) + match width { + WORD => mem_write_value(addr, 4, result[31..0], aq & rl, rl, true), + DOUBLE => mem_write_value(addr, 8, result, aq & rl, rl, true) }; } -(********************************************************************) +/* ****************************************************************** */ function clause decode _ = None -*/ + end ast end decode end execute diff --git a/riscv/riscv_types.sail b/riscv/riscv_types.sail index a593792d..b1b070bb 100644 --- a/riscv/riscv_types.sail +++ b/riscv/riscv_types.sail @@ -6,8 +6,9 @@ type regval = bits(64) type regno ('n : Int), 0 <= 'n < 32 = atom('n) type regbits = bits(5) -val cast regbits_to_regno : bits(5) -> {'n, 0 <= 'n < 32. atom('n)} -function regbits_to_regno n = unsigned(n) + +val cast regbits_to_regno : bits(5) -> {'n, 0 <= 'n < 32. regno('n)} +function regbits_to_regno n = let 'N = unsigned(n) in N /* register x0 : regval is hard-wired zero */ register x1 : regval @@ -166,13 +167,10 @@ enum word_width = {BYTE, HALF, WORD, DOUBLE} /* Ideally these would be sail builtin */ -/* -function (bit[64]) shift_right_arith64 ((bit[64]) v, (bit[6]) shift) = - let (bit[128]) v128 = EXTS(v) in +function shift_right_arith64 (v : bits(64), shift : bits(6)) -> bits(64) = + let v128 : bits(128) = EXTS(v) in (v128 >> shift)[63..0] -function (bit[32]) shift_right_arith32 ((bit[32]) v, (bit[5]) shift) = - let (bit[64]) v64 = EXTS(v) in - (v64 >> shift)[31..0] - -*/ +function shift_right_arith32 (v : bits(32), shift : bits(5)) -> bits(32) = + let v64 : bits(64) = EXTS(v) in + (v64 >> shift)[31..0]
\ No newline at end of file |