path: root/risc-v/riscv.sail

default Order dec

typedef regval = bit[64]
typedef regno = bit[5]

register (regval) x0
register (regval) x1
register (regval) x2
register (regval) x3
register (regval) x4
register (regval) x5
register (regval) x6
register (regval) x7
register (regval) x8
register (regval) x9
register (regval) x10
register (regval) x11
register (regval) x12
register (regval) x13
register (regval) x14
register (regval) x15
register (regval) x16
register (regval) x17
register (regval) x18
register (regval) x19
register (regval) x20
register (regval) x21
register (regval) x22
register (regval) x23
register (regval) x24
register (regval) x25
register (regval) x26
register (regval) x27
register (regval) x28
register (regval) x29
register (regval) x30
register (regval) x31

register (bit[64]) PC
register (bit[64]) nextPC

let (vector <0, 32, inc, (register<(regval)>)>) GPRs =
  [ x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14,
    x15, x16, x17, x18, x19, x20, x21, x22, x23, x24, x25, x26, x27,
    x28, x29, x30, x31
  ]

function (regval) rGPR ((regno) r) = 
    if (r == 0) then 
        0
    else 
        GPRs[r]

function unit wGPR((regno) r, (regval) v) =
    if (r != 0) then
        GPRs[r] := v

function forall 'a. 'a effect { escape } not_implemented((string) message) =
{
  exit message;
}

val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bit[8 * 'n]) effect { rmem } MEMr
val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bit[8 * 'n]) effect { rmem } MEMr_acquire
val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bit[8 * 'n]) effect { rmem } MEMr_reserved
val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bit[8 * 'n]) effect { rmem } MEMr_reserved_acquire
function forall Nat 'n. (bit[8 * 'n]) effect { rmem } mem_read( (bit[64]) addr, ([|'n|]) width, (bool) aq, (bool) res) =
  switch (aq, res) {
    case (false, false) -> MEMr(addr, width)
    case (true,  false) -> MEMr_acquire(addr, width)
    case (false, true)  -> MEMr_reserved(addr, width)
    case (true,  true)  -> MEMr_reserved_acquire(addr, width)
  }

val extern forall Nat 'n. ( bit[64] , [|'n|]) -> unit effect { eamem } MEMea
val extern forall Nat 'n. ( bit[64] , [|'n|]) -> unit effect { eamem } MEMea_release
val extern forall Nat 'n. ( bit[64] , [|'n|]) -> unit effect { eamem } MEMea_conditional
val extern forall Nat 'n. ( bit[64] , [|'n|]) -> unit effect { eamem } MEMea_conditional_release
function forall Nat 'n. unit effect { eamem } mem_write_ea( (bit[64]) addr , ([|'n|]) width, (bool) rl, (bool) con) =
  switch (rl, con) {
    case (false, false) -> MEMea(addr, width)
    case (true,  false) -> MEMea_release(addr, width)
    case (false, true)  -> MEMea_conditional(addr, width)
    case (true , true)  -> MEMea_conditional_release(addr, width)
  }

val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8*'n]) -> unit effect { wmv } MEMval
val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8*'n]) -> unit effect { wmv } MEMval_release
val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8*'n]) -> unit effect { wmv } MEMval_conditional
val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8*'n]) -> unit effect { wmv } MEMval_conditional_release
function forall Nat 'n. unit effect { wmv } mem_write_value( (bit[64]) addr , ([|'n|]) width , (bit[8*'n]) value, (bool) rl, (bool) con) =
  switch (rl, con) {
    case (false, false) -> MEMval(addr, width, value)
    case (true,  false) -> MEMval_release(addr, width, value)
    case (false, true)  -> MEMval_conditional(addr, width, value)
    case (true,  true)  -> MEMval_conditional_release(addr, width, value)
  }

val extern unit -> bool effect {exmem} speculate_conditional_success

val extern unit -> unit effect { barr } MEM_fence_rw_rw
val extern unit -> unit effect { barr } MEM_fence_r_rw
val extern unit -> unit effect { barr } MEM_fence_rw_w
val extern unit -> unit effect { barr } MEM_fence_w_w
val extern unit -> unit effect { barr } MEM_fence_i

(* 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
    (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]

typedef uop = enumerate {LUI; AUIPC} (* upper immediate ops *)
typedef bop = enumerate {BEQ; BNE; BLT; BGE; BLTU; BGEU} (* branch ops *)
typedef iop = enumerate {ADDI; SLTI; SLTIU; XORI; ORI; ANDI} (* immediate ops *)
typedef sop = enumerate {SLLI; SRLI; SRAI} (* shift ops *)
typedef rop = enumerate {ADD; SUB; SLL; SLT; SLTU; XOR; SRL; SRA; OR; AND} (* reg-reg ops *)
typedef ropw = enumerate {ADDW; SUBW; SLLW; SRLW; SRAW} (* reg-reg 32-bit ops *)
typedef amoop = enumerate {AMOSWAP; AMOADD; AMOXOR; AMOAND; AMOOR;
    AMOMIN; AMOMAX; AMOMINU; AMOMAXU} (* AMO ops *)


typedef word_width = enumerate {BYTE; HALF; WORD; DOUBLE}

scattered function unit execute
scattered typedef ast = const union

val bit[32] -> option<ast> effect pure decode

scattered function option<ast> decode

union ast member ((bit[20]), regno, uop) UTYPE

function clause decode ((bit[20]) imm : (regno) rd : 0b0110111) = Some(UTYPE(imm, rd, LUI))
function clause decode ((bit[20]) imm : (regno) rd : 0b0010111) = Some(UTYPE(imm, rd, AUIPC))

function clause execute (UTYPE(imm, rd, op)) =
    let (bit[64]) off = EXTS(imm : 0x000) in
    let ret = switch (op) {
      case LUI   -> off
      case AUIPC -> PC + off
    } in
    wGPR(rd, ret)

union ast member ((bit[21]), regno) JAL
function clause decode ((bit[20]) imm : (regno) rd : 0b1101111) = Some (JAL(imm[19] : imm[7..0] : imm[8] : imm[18..13] : imm[12..9] : 0b0, rd))
function clause execute (JAL(imm, rd)) =
    let (bit[64]) offset = EXTS(imm) in {
      nextPC :=  PC + offset;
      wGPR(rd, PC + 4);
    }

union ast member((bit[12]), regno, regno) JALR
function clause decode ((bit[12]) imm : (regno) rs1 : 0b000 : (regno) rd : 0b1100111) =
    Some(JALR(imm, rs1, rd))
function clause execute (JALR(imm, rs1, rd)) =
    let (bit[64]) newPC = rGPR(rs1) + EXTS(imm) in {
      nextPC := newPC[63..1] : 0b0;
      wGPR(rd, PC + 4);
    }

union ast member ((bit[13]), regno, regno, bop) BTYPE
function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b000 : (bit[5]) imm5 : 0b1100011) = Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1] : 0b0, rs2, rs1, BEQ))
function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b001 : (bit[5]) imm5 : 0b1100011) = Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1] : 0b0, rs2, rs1, BNE))
function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b100 : (bit[5]) imm5 : 0b1100011) = Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1] : 0b0, rs2, rs1, BLT))
function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b101 : (bit[5]) imm5 : 0b1100011) = Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1] : 0b0, rs2, rs1, BGE))
function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b110 : (bit[5]) imm5 : 0b1100011) = Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1] : 0b0, rs2, rs1, BLTU))
function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b111 : (bit[5]) imm5 : 0b1100011) = Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1] : 0b0, rs2, rs1, BGEU))

function clause execute (BTYPE(imm, rs2, rs1, op)) =
  let rs1_val = rGPR(rs1) in
  let rs2_val = rGPR(rs2) in
  let taken   = switch(op) {
    case BEQ  -> rs1_val == rs2_val
    case BNE  -> rs1_val != rs2_val
    case BLT  -> rs1_val <_s rs2_val
    case BGE  -> rs1_val >=_s rs2_val
    case BLTU -> rs1_val <_u rs2_val
    case BGEU -> unsigned(rs1_val) >= unsigned(rs2_val) (* XXX sail missing >=_u *)
  } in
  if (taken) then
      nextPC := PC + EXTS(imm)

union ast member ((bit[12]), regno, regno, iop) ITYPE
function clause decode ((bit[12]) imm : (regno) rs1 : 0b000 : (regno) rd : 0b0010011) = Some(ITYPE(imm, rs1, rd, ADDI))
function clause decode ((bit[12]) imm : (regno) rs1 : 0b010 : (regno) rd : 0b0010011) = Some(ITYPE(imm, rs1, rd, SLTI))
function clause decode ((bit[12]) imm : (regno) rs1 : 0b011 : (regno) rd : 0b0010011) = Some(ITYPE(imm, rs1, rd, SLTIU))
function clause decode ((bit[12]) imm : (regno) rs1 : 0b100 : (regno) rd : 0b0010011) = Some(ITYPE(imm, rs1, rd, XORI))
function clause decode ((bit[12]) imm : (regno) rs1 : 0b110 : (regno) rd : 0b0010011) = Some(ITYPE(imm, rs1, rd, ORI))
function clause decode ((bit[12]) imm : (regno) rs1 : 0b111 : (regno) rd : 0b0010011) = Some(ITYPE(imm, rs1, rd, ANDI))
function clause execute (ITYPE (imm, rs1, rd, op)) =
  let rs1_val = rGPR(rs1) in
  let imm64 = (bit[64]) (EXTS(imm)) in
  let (bit[64]) result = switch(op) {
    case ADDI  -> rs1_val + imm64
    case SLTI  -> EXTZ(rs1_val <_s imm64)
    case SLTIU -> EXTZ(rs1_val <_u imm64)
    case XORI  -> rs1_val ^ imm64
    case ORI   -> rs1_val | imm64
    case ANDI  -> rs1_val & imm64
  } in
  wGPR(rd, result)

union ast member ((bit[6]), regno, regno, sop) SHIFTIOP
function clause decode (0b000000 : (bit[6]) shamt : (regno) rs1 : 0b001 : (regno) rd : 0b0010011) = Some(SHIFTIOP(shamt, rs1, rd, SLLI))
function clause decode (0b000000 : (bit[6]) shamt : (regno) rs1 : 0b101 : (regno) rd : 0b0010011) = Some(SHIFTIOP(shamt, rs1, rd, SRLI))
function clause decode (0b010000 : (bit[6]) shamt : (regno) rs1 : 0b101 : (regno) rd : 0b0010011) = Some(SHIFTIOP(shamt, rs1, rd, SRAI))
function clause execute (SHIFTIOP(shamt, rs1, rd, op)) = 
    let rs1_val = rGPR(rs1) in
    let result = switch(op) {
      case SLLI -> rs1_val >> shamt
      case SRLI -> rs1_val << shamt
      case SRAI -> shift_right_arith64(rs1_val, shamt)
    } in
    wGPR(rd, result)

union ast member (regno, regno, regno, rop) RTYPE
function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b000 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, ADD))
function clause decode (0b0100000 : (regno) rs2 : (regno) rs1 : 0b000 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, SUB))
function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b001 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, SLL))
function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b010 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, SLT))
function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b011 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, SLTU))
function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b100 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, XOR))
function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b101 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, SRL))
function clause decode (0b0100000 : (regno) rs2 : (regno) rs1 : 0b101 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, SRA))
function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b110 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, OR))
function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b111 : (regno) rd : 0b0110011) = Some(RTYPE(rs2, rs1, rd, AND))
function clause execute (RTYPE(rs2, rs1, rd, op)) =
  let rs1_val = rGPR(rs1) in
  let rs2_val = rGPR(rs2) in
  let (bit[64]) result = switch(op) {
    case ADD  -> rs1_val + rs2_val
    case SUB  -> rs1_val - rs2_val
    case SLL  -> rs1_val << (rs2_val[5..0])
    case SLT  -> EXTZ(rs1_val <_s rs2_val)
    case SLTU -> EXTZ(rs1_val <_u rs2_val)
    case XOR  -> rs1_val ^ rs2_val
    case SRL  -> rs1_val >> (rs2_val[5..0])
    case SRA  -> shift_right_arith64(rs1_val, rs2_val[5..0])
    case OR   -> rs1_val | rs2_val
    case AND  -> rs1_val & rs2_val
  } in
  wGPR(rd, result)

union ast member ((bit[12]), regno, regno, bool, word_width, bool) LOAD
function clause decode ((bit[12]) imm : (regno) rs1 : 0b000 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, false, BYTE,   false))
function clause decode ((bit[12]) imm : (regno) rs1 : 0b001 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, false, HALF,   false))
function clause decode ((bit[12]) imm : (regno) rs1 : 0b010 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, false, WORD,   false))
function clause decode ((bit[12]) imm : (regno) rs1 : 0b011 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, false, DOUBLE, false))
function clause decode ((bit[12]) imm : (regno) rs1 : 0b100 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, true,  BYTE,   false))
function clause decode ((bit[12]) imm : (regno) rs1 : 0b101 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, true,  HALF,   false))
function clause decode ((bit[12]) imm : (regno) rs1 : 0b110 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, true,  WORD,   false))
function clause execute(LOAD(imm, rs1, rd, unsigned, width, aq)) =
    let (bit[64]) addr = rGPR(rs1) + EXTS(imm) in
    let (bit[64]) result = if unsigned then 
        switch (width) {
          case BYTE   -> EXTZ(mem_read(addr, 1, aq, false))
          case HALF   -> EXTZ(mem_read(addr, 2, aq, false))
          case WORD   -> EXTZ(mem_read(addr, 4, aq, false))
          case DOUBLE -> mem_read(addr, 8, aq, false)
        }
      else
        switch (width) {
          case BYTE   -> EXTS(mem_read(addr, 1, aq, false))
          case HALF   -> EXTS(mem_read(addr, 2, aq, false))
          case WORD   -> EXTS(mem_read(addr, 4, aq, false))
          case DOUBLE -> mem_read(addr, 8, aq, false)
        } in
    wGPR(rd, result)

union ast member ((bit[12]), regno, regno, word_width, bool) STORE
function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b000 : (bit[5]) imm5 : 0b0100011) = Some(STORE(imm7 : imm5, rs2, rs1, BYTE, false))
function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b001 : (bit[5]) imm5 : 0b0100011) = Some(STORE(imm7 : imm5, rs2, rs1, HALF, false))
function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b010 : (bit[5]) imm5 : 0b0100011) = Some(STORE(imm7 : imm5, rs2, rs1, WORD, false))
function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b011 : (bit[5]) imm5 : 0b0100011) = Some(STORE(imm7 : imm5, rs2, rs1, DOUBLE, false))
function clause execute (STORE(imm, rs2, rs1, width, rl)) =
    let (bit[64]) addr = rGPR(rs1) + EXTS(imm) in {
      switch (width) {
        case BYTE   -> mem_write_ea(addr, 1, rl, false)
        case HALF   -> mem_write_ea(addr, 2, rl, false)
        case WORD   -> mem_write_ea(addr, 4, rl, false)
        case DOUBLE -> mem_write_ea(addr, 8, rl, false)
      };
      let rs2_val = rGPR(rs2) in
      switch (width) {
        case BYTE   -> mem_write_value(addr, 1, rs2_val[7..0],  rl, false)
        case HALF   -> mem_write_value(addr, 2, rs2_val[15..0], rl, false)
        case WORD   -> mem_write_value(addr, 4, rs2_val[31..0], rl, false)
        case DOUBLE -> mem_write_value(addr, 8, rs2_val,        rl, false)
      }
    }

union ast member ((bit[12]), regno, regno) ADDIW
function clause decode ((bit[12]) imm : (regno) rs1 : 0b000 : (regno) rd : 0b0011011) = Some(ADDIW(imm, rs1, rd))
function clause execute (ADDIW(imm, rs1, rd)) =
  let (bit[64]) imm64 = EXTS(imm) in
  let (bit[64]) result64 = imm64 + rGPR(rs1) in
  let (bit[64]) result32 = EXTS(result64[31..0]) in
  wGPR(rd, result32)

union ast member ((bit[5]), regno, regno, sop) SHIFTW
function clause decode (0b0000000 : (bit[5]) shamt : (regno) rs1 : 0b001 : (regno) rd : 0b0011011) = Some(SHIFTW(shamt, rs1, rd, SLLI))
function clause decode (0b0000000 : (bit[5]) shamt : (regno) rs1 : 0b101 : (regno) rd : 0b0011011) = Some(SHIFTW(shamt, rs1, rd, SRLI))
function clause decode (0b0100000 : (bit[5]) shamt : (regno) rs1 : 0b101 : (regno) rd : 0b0011011) = Some(SHIFTW(shamt, rs1, rd, SRAI))
function clause execute (SHIFTW(shamt, rs1, rd, op)) = 
    let rs1_val = (rGPR(rs1))[31..0] in
    let result = switch(op) {
      case SLLI -> rs1_val >> shamt
      case SRLI -> rs1_val << shamt
      case SRAI -> shift_right_arith32(rs1_val, shamt)
    } in
    wGPR(rd, EXTS(result))

union ast member (regno, regno, regno, ropw) RTYPEW
function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b000 : (regno) rd : 0b0111011) = Some(RTYPEW(rs2, rs1, rd, ADDW))
function clause decode (0b0100000 : (regno) rs2 : (regno) rs1 : 0b000 : (regno) rd : 0b0111011) = Some(RTYPEW(rs2, rs1, rd, SUBW))
function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b001 : (regno) rd : 0b0111011) = Some(RTYPEW(rs2, rs1, rd, SLLW))
function clause decode (0b0000000 : (regno) rs2 : (regno) rs1 : 0b101 : (regno) rd : 0b0111011) = Some(RTYPEW(rs2, rs1, rd, SRLW))
function clause decode (0b0100000 : (regno) rs2 : (regno) rs1 : 0b101 : (regno) rd : 0b0111011) = Some(RTYPEW(rs2, rs1, rd, 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 (bit[32]) result = switch(op) {
    case ADDW -> rs1_val + rs2_val
    case SUBW -> rs1_val - rs2_val
    case SLLW -> rs1_val << (rs2_val[4..0])
    case SRLW -> rs1_val >> (rs2_val[4..0])
    case SRAW -> shift_right_arith32(rs1_val, rs2_val[4..0])
  } in
  wGPR(rd, EXTS(result))

union ast member (bit[4], bit[4]) FENCE
function clause decode (0b0000 : (bit[4]) pred : (bit[4]) succ : 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 (0b0011, 0b0001) -> MEM_fence_rw_w()
    case (0b0001, 0b0001) -> MEM_fence_w_w()
    case _ -> not_implemented("unsupported fence")
  }
}

union ast member unit 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 ())
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 ast member (bool, bool, regno, word_width, regno) LOADRES
function clause decode (0b00010 : [aq] : [rl] : 0b00000 : (regno) rs1 : 0b010 : (regno) rd : 0b0101111) = Some(LOADRES(aq, rl, rs1, WORD, rd))
function clause decode (0b00010 : [aq] : [rl] : 0b00000 : (regno) rs1 : 0b011 : (regno) rd : 0b0101111) = Some(LOADRES(aq, rl, rs1, DOUBLE, rd))
function clause execute(LOADRES(aq, rl, rs1, width, rd)) =
  if rl then not_implemented("load-reserved-release is not implemented")
  else {
    let (bit[64]) addr = rGPR(rs1) in
    let (bit[64]) result =
        switch width {
          case WORD   -> EXTS(mem_read(addr, 4, aq, true))
          case DOUBLE -> mem_read(addr, 8, aq, true)
        } in
    wGPR(rd, result)
  }

union ast member (bool, bool, regno, regno, word_width, regno) STORECON
function clause decode (0b00011 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b010 : (regno) rd : 0b0101111) = Some(STORECON(aq, rl, rs2, rs1, WORD, rd))
function clause decode (0b00011 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b011 : (regno) rd : 0b0101111) = Some(STORECON(aq, rl, rs2, rs1, DOUBLE, rd))
function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = {
  if aq then not_implemented("store-conditional-acquire is not implemented");

  (*(bit)*) status := if speculate_conditional_success() then 0 else 1;
  wGPR(rd) := (bit[64]) (EXTZ([status]));

  (bit[64]) addr := rGPR(rs1);
  switch width {
    case WORD   -> mem_write_ea(addr, 4, rl, true)
    case DOUBLE -> mem_write_ea(addr, 8, rl, true)
  };
  rs2_val := rGPR(rs2);
  switch width {
    case WORD   -> mem_write_value(addr, 4, rs2_val[31..0], rl, true)
    case DOUBLE -> mem_write_value(addr, 8, rs2_val,        rl, true)
  };
}

union ast member (amoop, bool, bool, regno, regno, word_width, regno) AMO

function clause decode (0b00001 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b010 : (regno) rd : 0b0101111) = Some(AMO(AMOSWAP, aq, rl, rs2, rs1, WORD,   rd))
function clause decode (0b00001 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b011 : (regno) rd : 0b0101111) = Some(AMO(AMOSWAP, aq, rl, rs2, rs1, DOUBLE, rd))
function clause decode (0b00000 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b010 : (regno) rd : 0b0101111) = Some(AMO(AMOADD , aq, rl, rs2, rs1, WORD,   rd))
function clause decode (0b00000 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b011 : (regno) rd : 0b0101111) = Some(AMO(AMOADD , aq, rl, rs2, rs1, DOUBLE, rd))
function clause decode (0b00100 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b010 : (regno) rd : 0b0101111) = Some(AMO(AMOXOR , aq, rl, rs2, rs1, WORD,   rd))
function clause decode (0b00100 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b011 : (regno) rd : 0b0101111) = Some(AMO(AMOXOR , aq, rl, rs2, rs1, DOUBLE, rd))
function clause decode (0b01100 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b010 : (regno) rd : 0b0101111) = Some(AMO(AMOAND , aq, rl, rs2, rs1, WORD,   rd))
function clause decode (0b01100 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b011 : (regno) rd : 0b0101111) = Some(AMO(AMOAND , aq, rl, rs2, rs1, DOUBLE, rd))
function clause decode (0b01000 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b010 : (regno) rd : 0b0101111) = Some(AMO(AMOOR  , aq, rl, rs2, rs1, WORD,   rd))
function clause decode (0b01000 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b011 : (regno) rd : 0b0101111) = Some(AMO(AMOOR  , aq, rl, rs2, rs1, DOUBLE, rd))
function clause decode (0b10000 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b010 : (regno) rd : 0b0101111) = Some(AMO(AMOMIN , aq, rl, rs2, rs1, WORD,   rd))
function clause decode (0b10000 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b011 : (regno) rd : 0b0101111) = Some(AMO(AMOMIN , aq, rl, rs2, rs1, DOUBLE, rd))
function clause decode (0b10100 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b010 : (regno) rd : 0b0101111) = Some(AMO(AMOMAX , aq, rl, rs2, rs1, WORD,   rd))
function clause decode (0b10100 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b011 : (regno) rd : 0b0101111) = Some(AMO(AMOMAX , aq, rl, rs2, rs1, DOUBLE, rd))
function clause decode (0b11000 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b010 : (regno) rd : 0b0101111) = Some(AMO(AMOMINU, aq, rl, rs2, rs1, WORD,   rd))
function clause decode (0b11000 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b011 : (regno) rd : 0b0101111) = Some(AMO(AMOMINU, aq, rl, rs2, rs1, DOUBLE, rd))
function clause decode (0b11100 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b010 : (regno) rd : 0b0101111) = Some(AMO(AMOMAXU, aq, rl, rs2, rs1, WORD,   rd))
function clause decode (0b11100 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b011 : (regno) rd : 0b0101111) = Some(AMO(AMOMAXU, aq, rl, rs2, rs1, DOUBLE, rd))
function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = {
  (bit[64]) addr := rGPR(rs1);

  switch (width) {
    case WORD   -> mem_write_ea(addr, 4, rl, true)
    case DOUBLE -> mem_write_ea(addr, 8, rl, true)
  };

  (bit[64]) loaded :=
    switch (width) {
      case WORD   -> EXTS(mem_read(addr, 4, aq, true))
      case DOUBLE -> mem_read(addr, 8, aq, true)
    };
  wGPR(rd, loaded);

  (bit[64]) rs2_val := rGPR(rs2);
  (bit[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  -> (bit[64]) (min(signed(rs2_val),   signed(loaded)))
      case AMOMAX  -> (bit[64]) (max(signed(rs2_val),   signed(loaded)))
      case AMOMINU -> (bit[64]) (min(unsigned(rs2_val), unsigned(loaded)))
      case AMOMAXU -> (bit[64]) (max(unsigned(rs2_val), unsigned(loaded)))
    };

  switch (width) {
    case WORD   -> mem_write_value(addr, 4, result[31..0], rl, true)
    case DOUBLE -> mem_write_value(addr, 8, result,        rl, true)
  };
}

function clause decode _ = None

end ast
end decode
end execute