summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--etc/regfp.sail8
-rw-r--r--risc-v/hgen/ast.hgen2
-rw-r--r--risc-v/hgen/fold.hgen2
-rw-r--r--risc-v/hgen/herdtools_ast_to_shallow_ast.hgen5
-rw-r--r--risc-v/hgen/lexer.hgen22
-rw-r--r--risc-v/hgen/map.hgen2
-rw-r--r--risc-v/hgen/parser.hgen2
-rw-r--r--risc-v/hgen/pretty.hgen3
-rw-r--r--risc-v/hgen/sail_trans_out.hgen3
-rw-r--r--risc-v/hgen/shallow_ast_to_herdtools_ast.hgen3
-rw-r--r--risc-v/hgen/token_types.hgen2
-rw-r--r--risc-v/hgen/trans_sail.hgen3
-rw-r--r--risc-v/hgen/types.hgen7
-rw-r--r--risc-v/riscv.sail45
-rw-r--r--risc-v/riscv_extras.lem6
-rw-r--r--risc-v/riscv_extras_embed.lem13
-rw-r--r--risc-v/riscv_extras_embed_sequential.lem14
-rw-r--r--risc-v/riscv_regfp.sail12
-rw-r--r--src/lem_interp/sail_impl_base.lem2
19 files changed, 104 insertions, 52 deletions
diff --git a/etc/regfp.sail b/etc/regfp.sail
index fb15310a..c98e3fa4 100644
--- a/etc/regfp.sail
+++ b/etc/regfp.sail
@@ -37,7 +37,10 @@ typedef read_kind = enumerate {
Read_acquire;
Read_exclusive;
Read_exclusive_acquire;
- Read_stream
+ Read_stream;
+ Read_RISCV_acquire;
+ Read_RISCV_reserved;
+ Read_RISCV_reserved_acquire;
}
typedef write_kind = enumerate {
@@ -62,6 +65,9 @@ typedef barrier_kind = enumerate {
Barrier_DSB_LD;
Barrier_ISB;
Barrier_MIPS_SYNC;
+ Barrier_RISCV_rw_rw;
+ Barrier_RISCV_r_rw;
+ Barrier_RISCV_rw_w;
}
typedef trans_kind = enumerate {
diff --git a/risc-v/hgen/ast.hgen b/risc-v/hgen/ast.hgen
index 8983b5ae..6e323e85 100644
--- a/risc-v/hgen/ast.hgen
+++ b/risc-v/hgen/ast.hgen
@@ -5,7 +5,7 @@
| `RISCVIType of bit12 * reg * reg * riscvIop
| `RISCVShiftIop of bit6 * reg * reg * riscvSop
| `RISCVRType of reg * reg * reg * riscvRop
-| `RISCVLoad of bit12 * reg * reg * bool * wordWidth
+| `RISCVLoad of bit12 * reg * reg * bool * wordWidth * bool
| `RISCVStore of bit12 * reg * reg * wordWidth
| `RISCVADDIW of bit12 * reg * reg
| `RISCVSHIFTW of bit5 * reg * reg * riscvSop
diff --git a/risc-v/hgen/fold.hgen b/risc-v/hgen/fold.hgen
index 03318805..be91659b 100644
--- a/risc-v/hgen/fold.hgen
+++ b/risc-v/hgen/fold.hgen
@@ -6,7 +6,7 @@
| `RISCVIType (_, r0, r1, _) -> fold_reg r0 (fold_reg r1 (y_reg, y_sreg))
| `RISCVShiftIop (_, r0, r1, _) -> fold_reg r0 (fold_reg r1 (y_reg, y_sreg))
| `RISCVRType (r0, r1, r2, _) -> fold_reg r0 (fold_reg r1 (fold_reg r2 (y_reg, y_sreg)))
-| `RISCVLoad (_, r0, r1, _, _) -> fold_reg r0 (fold_reg r1 (y_reg, y_sreg))
+| `RISCVLoad (_, r0, r1, _, _, _) -> fold_reg r0 (fold_reg r1 (y_reg, y_sreg))
| `RISCVStore (_, r0, r1, _) -> fold_reg r0 (fold_reg r1 (y_reg, y_sreg))
| `RISCVADDIW (_, r0, r1) -> fold_reg r0 (fold_reg r1 (y_reg, y_sreg))
| `RISCVSHIFTW (_, r0, r1, _) -> fold_reg r0 (fold_reg r1 (y_reg, y_sreg))
diff --git a/risc-v/hgen/herdtools_ast_to_shallow_ast.hgen b/risc-v/hgen/herdtools_ast_to_shallow_ast.hgen
index 50026612..0e8bfdc2 100644
--- a/risc-v/hgen/herdtools_ast_to_shallow_ast.hgen
+++ b/risc-v/hgen/herdtools_ast_to_shallow_ast.hgen
@@ -30,12 +30,13 @@
translate_reg "rs1" rs1,
translate_reg "rd" rd,
translate_rop op)
-| `RISCVLoad(imm, rs, rd, unsigned, width) -> LOAD(
+| `RISCVLoad(imm, rs, rd, unsigned, width, aq) -> LOAD(
translate_imm12 "imm" imm,
translate_reg "rs" rs,
translate_reg "rd" rd,
translate_bool "unsigned" unsigned,
- translate_wordWidth width)
+ translate_wordWidth width,
+ translate_bool "aq" aq)
| `RISCVStore(imm, rs, rd, width) -> STORE (
translate_imm12 "imm" imm,
translate_reg "rs" rs,
diff --git a/risc-v/hgen/lexer.hgen b/risc-v/hgen/lexer.hgen
index 5f2c8326..c4408139 100644
--- a/risc-v/hgen/lexer.hgen
+++ b/risc-v/hgen/lexer.hgen
@@ -33,13 +33,21 @@
"or", RTYPE{op=RISCVOR};
"and", RTYPE{op=RISCVAND};
-"lb", LOAD{unsigned=false; width=RISCVBYTE};
-"lbu", LOAD{unsigned=true; width=RISCVBYTE};
-"lh", LOAD{unsigned=false; width=RISCVHALF};
-"lhu", LOAD{unsigned=true; width=RISCVHALF};
-"lw", LOAD{unsigned=false; width=RISCVWORD};
-"lwu", LOAD{unsigned=true; width=RISCVWORD};
-"ld", LOAD{unsigned=false; width=RISCVDOUBLE};
+"lb", LOAD{unsigned=false; width=RISCVBYTE; aq=false};
+"lbu", LOAD{unsigned=true; width=RISCVBYTE; aq=false};
+"lh", LOAD{unsigned=false; width=RISCVHALF; aq=false};
+"lhu", LOAD{unsigned=true; width=RISCVHALF; aq=false};
+"lw", LOAD{unsigned=false; width=RISCVWORD; aq=false};
+"lwu", LOAD{unsigned=true; width=RISCVWORD; aq=false};
+"ld", LOAD{unsigned=false; width=RISCVDOUBLE; aq=false};
+
+"lb.aq", LOAD{unsigned=false; width=RISCVBYTE; aq=true};
+"lbu.aq", LOAD{unsigned=true; width=RISCVBYTE; aq=true};
+"lh.aq", LOAD{unsigned=false; width=RISCVHALF; aq=true};
+"lhu.aq", LOAD{unsigned=true; width=RISCVHALF; aq=true};
+"lw.aq", LOAD{unsigned=false; width=RISCVWORD; aq=true};
+"lwu.aq", LOAD{unsigned=true; width=RISCVWORD; aq=true};
+"ld.aq", LOAD{unsigned=false; width=RISCVDOUBLE; aq=true};
"sb", STORE{width=RISCVBYTE};
"sh", STORE{width=RISCVHALF};
diff --git a/risc-v/hgen/map.hgen b/risc-v/hgen/map.hgen
index ff14c428..1deacc06 100644
--- a/risc-v/hgen/map.hgen
+++ b/risc-v/hgen/map.hgen
@@ -5,7 +5,7 @@
| `RISCVIType (x, r0, r1, y) -> `RISCVIType (x, map_reg r0, map_reg r1, y)
| `RISCVShiftIop (x, r0, r1, y) -> `RISCVShiftIop (x, map_reg r0, map_reg r1, y)
| `RISCVRType (r0, r1, r2, y) -> `RISCVRType (r0, map_reg r1, map_reg r2, y)
-| `RISCVLoad (x, r0, r1, y, z) -> `RISCVLoad (x, map_reg r0, map_reg r1, y, z)
+| `RISCVLoad (x, r0, r1, y, z, a) -> `RISCVLoad (x, map_reg r0, map_reg r1, y, z, a)
| `RISCVStore (x, r0, r1, y) -> `RISCVStore (x, map_reg r0, map_reg r1, y)
| `RISCVADDIW (x, r0, r1) -> `RISCVADDIW (x, map_reg r0, map_reg r1)
| `RISCVSHIFTW (x, r0, r1, y) -> `RISCVSHIFTW (x, map_reg r0, map_reg r1, y)
diff --git a/risc-v/hgen/parser.hgen b/risc-v/hgen/parser.hgen
index 37fd8d8d..10257ecd 100644
--- a/risc-v/hgen/parser.hgen
+++ b/risc-v/hgen/parser.hgen
@@ -13,7 +13,7 @@
| RTYPE reg COMMA reg COMMA reg
{ `RISCVRType ($6, $4, $2, $1.op) }
| LOAD reg COMMA NUM LPAR reg RPAR
- { `RISCVLoad($4, $6, $2, $1.unsigned, $1.width) }
+ { `RISCVLoad($4, $6, $2, $1.unsigned, $1.width, $1.aq) }
| STORE reg COMMA NUM LPAR reg RPAR
{ `RISCVStore($4, $2, $6, $1.width) }
| ADDIW reg COMMA reg COMMA NUM
diff --git a/risc-v/hgen/pretty.hgen b/risc-v/hgen/pretty.hgen
index 1da3ef11..6c4f3e53 100644
--- a/risc-v/hgen/pretty.hgen
+++ b/risc-v/hgen/pretty.hgen
@@ -7,7 +7,8 @@
| `RISCVIType(imm, rs2, rs1, op) -> sprintf "%s %s, %s, %d" (pp_riscv_iop op) (pp_reg rs1) (pp_reg rs2) imm
| `RISCVShiftIop(imm, rs, rd, op) -> sprintf "%s %s, %s, %d" (pp_riscv_sop op) (pp_reg rd) (pp_reg rs) imm
| `RISCVRType (rs2, rs1, rd, op) -> sprintf "%s %s, %s, %s" (pp_riscv_rop op) (pp_reg rd) (pp_reg rs1) (pp_reg rs2)
-| `RISCVLoad(imm, rs, rd, unsigned, width) -> sprintf "%s %s, %d(%s)" (pp_riscv_load_op (unsigned, width)) (pp_reg rd) imm (pp_reg rs)
+| `RISCVLoad(imm, rs, rd, unsigned, width, aq)
+ -> sprintf "%s %s, %d(%s)" (pp_riscv_load_op (unsigned, width, aq)) (pp_reg rd) imm (pp_reg rs)
| `RISCVStore(imm, rs2, rs1, width) -> sprintf "%s %s, %d(%s)" (pp_riscv_store_op width) (pp_reg rs2) imm (pp_reg rs1)
| `RISCVADDIW(imm, rs, rd) -> sprintf "addiw %s, %s, %d" (pp_reg rd) (pp_reg rs) imm
| `RISCVSHIFTW(imm, rs, rd, op) -> sprintf "%s %s, %s, %d" (pp_riscv_sop op) (pp_reg rd) (pp_reg rs) imm
diff --git a/risc-v/hgen/sail_trans_out.hgen b/risc-v/hgen/sail_trans_out.hgen
index dca5bea1..2a161bda 100644
--- a/risc-v/hgen/sail_trans_out.hgen
+++ b/risc-v/hgen/sail_trans_out.hgen
@@ -6,7 +6,8 @@
| ("ITYPE", [imm; rs1; rd; op]) -> `RISCVIType(translate_out_simm12 imm, translate_out_ireg rs1, translate_out_ireg rd, translate_out_iop op)
| ("SHIFTIOP", [imm; rs; rd; op]) -> `RISCVShiftIop(translate_out_imm6 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_sop op)
| ("RTYPE", [rs2; rs1; rd; op]) -> `RISCVRType (translate_out_ireg rs2, translate_out_ireg rs1, translate_out_ireg rd, translate_out_rop op)
-| ("LOAD", [imm; rs; rd; unsigned; width]) -> `RISCVLoad(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_bool unsigned, translate_out_wordWidth width)
+| ("LOAD", [imm; rs; rd; unsigned; width; aq])
+ -> `RISCVLoad(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_bool unsigned, translate_out_wordWidth width, translate_out_bool aq)
| ("STORE", [imm; rs; rd; width]) -> `RISCVStore(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_wordWidth width)
| ("ADDIW", [imm; rs; rd]) -> `RISCVADDIW(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd)
| ("SHIFTW", [imm; rs; rd; op]) -> `RISCVSHIFTW(translate_out_imm5 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_sop op)
diff --git a/risc-v/hgen/shallow_ast_to_herdtools_ast.hgen b/risc-v/hgen/shallow_ast_to_herdtools_ast.hgen
index 6158ebd7..c24ecd8f 100644
--- a/risc-v/hgen/shallow_ast_to_herdtools_ast.hgen
+++ b/risc-v/hgen/shallow_ast_to_herdtools_ast.hgen
@@ -6,7 +6,8 @@
| ITYPE( imm, rs1, rd, op) -> `RISCVIType(translate_out_simm12 imm, translate_out_ireg rs1, translate_out_ireg rd, translate_out_iop op)
| SHIFTIOP( imm, rs, rd, op) -> `RISCVShiftIop(translate_out_imm6 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_sop op)
| RTYPE( rs2, rs1, rd, op) -> `RISCVRType (translate_out_ireg rs2, translate_out_ireg rs1, translate_out_ireg rd, translate_out_rop op)
-| LOAD( imm, rs, rd, unsigned, width) -> `RISCVLoad(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_bool unsigned, translate_out_wordWidth width)
+| LOAD( imm, rs, rd, unsigned, width, aq)
+ -> `RISCVLoad(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_bool unsigned, translate_out_wordWidth width, translate_out_bool aq)
| STORE( imm, rs, rd, width) -> `RISCVStore(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_wordWidth width)
| ADDIW( imm, rs, rd) -> `RISCVADDIW(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd)
| SHIFTW( imm, rs, rd, op) -> `RISCVSHIFTW(translate_out_imm5 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_sop op)
diff --git a/risc-v/hgen/token_types.hgen b/risc-v/hgen/token_types.hgen
index 2980b985..ca19c6eb 100644
--- a/risc-v/hgen/token_types.hgen
+++ b/risc-v/hgen/token_types.hgen
@@ -5,7 +5,7 @@ type token_BType = {op : riscvBop }
type token_IType = {op : riscvIop }
type token_ShiftIop = {op : riscvSop }
type token_RTYPE = {op : riscvRop }
-type token_Load = {unsigned: bool; width : wordWidth }
+type token_Load = {unsigned: bool; width : wordWidth; aq: bool }
type token_Store = {width : wordWidth }
type token_ADDIW = unit
type token_SHIFTW = {op : riscvSop }
diff --git a/risc-v/hgen/trans_sail.hgen b/risc-v/hgen/trans_sail.hgen
index df22d9dc..7fdfd516 100644
--- a/risc-v/hgen/trans_sail.hgen
+++ b/risc-v/hgen/trans_sail.hgen
@@ -58,7 +58,7 @@
translate_rop "op" op;
],
[])
-| `RISCVLoad(imm, rs, rd, unsigned, width) ->
+| `RISCVLoad(imm, rs, rd, unsigned, width, aq) ->
("LOAD",
[
translate_imm12 "imm" imm;
@@ -66,6 +66,7 @@
translate_reg "rd" rd;
translate_bool "unsigned" unsigned;
translate_width "width" width;
+ translate_bool "aq" aq;
],
[])
| `RISCVStore(imm, rs2, rs1, width) ->
diff --git a/risc-v/hgen/types.hgen b/risc-v/hgen/types.hgen
index 87fc9b95..bb6d164c 100644
--- a/risc-v/hgen/types.hgen
+++ b/risc-v/hgen/types.hgen
@@ -99,7 +99,8 @@ type wordWidth =
| RISCVWORD
| RISCVDOUBLE
-let pp_riscv_load_op (unsigned, width) = match (unsigned, width) with
+let pp_riscv_load_op (unsigned, width, aq) =
+ begin match (unsigned, width) with
| (false, RISCVBYTE) -> "lb"
| (true, RISCVBYTE) -> "lbu"
| (false, RISCVHALF) -> "lh"
@@ -107,7 +108,9 @@ let pp_riscv_load_op (unsigned, width) = match (unsigned, width) with
| (false, RISCVWORD) -> "lw"
| (true, RISCVWORD) -> "lwu"
| (_, RISCVDOUBLE) -> "ld"
- | _ -> failwith "unexpected load op"
+ | _ -> failwith "unexpected load op"
+ end
+ ^ (if aq then ".aq" else "")
let pp_riscv_store_op width = match width with
| RISCVBYTE -> "sb"
diff --git a/risc-v/riscv.sail b/risc-v/riscv.sail
index 4a80adb0..c9ba5256 100644
--- a/risc-v/riscv.sail
+++ b/risc-v/riscv.sail
@@ -58,6 +58,17 @@ function forall 'a. 'a effect { escape } not_implemented((string) 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|] , bit[8*'n]) -> unit effect { wmv } MEMval
val extern unit -> unit effect { barr } MEM_fence_rw_rw
@@ -202,29 +213,29 @@ function clause execute (RTYPE(rs2, rs1, rd, op)) =
} in
wGPR(rd, result)
-union ast member ((bit[12]), regno, regno, bool, word_width) LOAD
-function clause decode ((bit[12]) imm : (regno) rs1 : 0b000 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, false, BYTE))
-function clause decode ((bit[12]) imm : (regno) rs1 : 0b001 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, false, HALF))
-function clause decode ((bit[12]) imm : (regno) rs1 : 0b010 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, false, WORD))
-function clause decode ((bit[12]) imm : (regno) rs1 : 0b011 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, false, DOUBLE))
-function clause decode ((bit[12]) imm : (regno) rs1 : 0b100 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, true, BYTE))
-function clause decode ((bit[12]) imm : (regno) rs1 : 0b101 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, true, HALF))
-function clause decode ((bit[12]) imm : (regno) rs1 : 0b110 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, true, WORD))
-function clause execute(LOAD(imm, rs1, rd, unsigned, width)) =
+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(MEMr(addr, 1))
- case HALF -> EXTZ(MEMr(addr, 2))
- case WORD -> EXTZ(MEMr(addr, 4))
- case DOUBLE -> MEMr(addr, 8)
+ 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(MEMr(addr, 1))
- case HALF -> EXTS(MEMr(addr, 2))
- case WORD -> EXTS(MEMr(addr, 4))
- case DOUBLE -> MEMr(addr, 8)
+ 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)
diff --git a/risc-v/riscv_extras.lem b/risc-v/riscv_extras.lem
index aa5d8fb8..80f8bcc9 100644
--- a/risc-v/riscv_extras.lem
+++ b/risc-v/riscv_extras.lem
@@ -32,8 +32,10 @@ let memory_parameter_transformer_option_address _mode v =
let read_memory_functions : memory_reads =
- [ ("MEMr", (MR Read_plain memory_parameter_transformer));
- ("MEMr_reserve", (MR Read_reserve memory_parameter_transformer));
+ [ ("MEMr", (MR Read_plain memory_parameter_transformer));
+ ("MEMr_acquire", (MR Read_RISCV_acquire memory_parameter_transformer));
+ ("MEMr_reserved", (MR Read_RISCV_reserved memory_parameter_transformer));
+ ("MEMr_reserved_acquire", (MR Read_RISCV_reserved_acquire memory_parameter_transformer));
]
let memory_writes : memory_writes =
diff --git a/risc-v/riscv_extras_embed.lem b/risc-v/riscv_extras_embed.lem
index 1146d1cd..440ad378 100644
--- a/risc-v/riscv_extras_embed.lem
+++ b/risc-v/riscv_extras_embed.lem
@@ -4,11 +4,16 @@ open import Sail_impl_base
open import Sail_values
open import Prompt
-val MEMr : (vector bitU * integer) -> M (vector bitU)
-val MEMr_reserve : (vector bitU * integer) -> M (vector bitU)
+val MEMr : (vector bitU * integer) -> M (vector bitU)
+val MEMr_acquire : (vector bitU * integer) -> M (vector bitU)
+val MEMr_reserved : (vector bitU * integer) -> M (vector bitU)
+val MEMr_reserved_acquire : (vector bitU * integer) -> M (vector bitU)
+
+let MEMr (addr,size) = read_mem false Read_plain addr size
+let MEMr_acquire (addr,size) = read_mem false Read_RISCV_acquire addr size
+let MEMr_reserved (addr,size) = read_mem false Read_RISCV_reserved addr size
+let MEMr_reserved_acquire (addr,size) = read_mem false Read_RISCV_reserved_acquire addr size
-let MEMr (addr,size) = read_mem false Read_plain addr size
-let MEMr_reserve (addr,size) = read_mem false Read_reserve addr size
val MEMea : (vector bitU * integer) -> M unit
val MEMea_conditional : (vector bitU * integer) -> M unit
diff --git a/risc-v/riscv_extras_embed_sequential.lem b/risc-v/riscv_extras_embed_sequential.lem
index f6709ff7..518a5a15 100644
--- a/risc-v/riscv_extras_embed_sequential.lem
+++ b/risc-v/riscv_extras_embed_sequential.lem
@@ -4,11 +4,15 @@ open import Sail_impl_base
open import Sail_values
open import State
-val MEMr : (vector bitU * integer) -> M (vector bitU)
-val MEMr_reserve : (vector bitU * integer) -> M (vector bitU)
-
-let MEMr (addr,size) = read_mem false Read_plain addr size
-let MEMr_reserve (addr,size) = read_mem false Read_reserve addr size
+val MEMr : (vector bitU * integer) -> M (vector bitU)
+val MEMr_acquire : (vector bitU * integer) -> M (vector bitU)
+val MEMr_reserved : (vector bitU * integer) -> M (vector bitU)
+val MEMr_reserved_acquire : (vector bitU * integer) -> M (vector bitU)
+
+let MEMr (addr,size) = read_mem false Read_plain addr size
+let MEMr_acquire (addr,size) = read_mem false Read_RISCV_acquire addr size
+let MEMr_reserved (addr,size) = read_mem false Read_RISCV_reserved addr size
+let MEMr_reserved_acquire (addr,size) = read_mem false Read_RISCV_reserved_acquire addr size
val MEMea : (vector bitU * integer) -> M unit
val MEMea_conditional : (vector bitU * integer) -> M unit
diff --git a/risc-v/riscv_regfp.sail b/risc-v/riscv_regfp.sail
index 0c7a67d8..fe0efa43 100644
--- a/risc-v/riscv_regfp.sail
+++ b/risc-v/riscv_regfp.sail
@@ -51,11 +51,11 @@ function (regfps,regfps,regfps,niafps,diafp,instruction_kind) initial_analysis (
if (rs1 == 0) then () else iR := RFull(GPRstr[rs1]) :: iR;
if (rd == 0) then () else oR := RFull(GPRstr[rd]) :: oR;
}
- case (LOAD ( imm, rs, rd, unsign, width)) -> { (* XXX "unsigned" causes name conflict in lem shallow embedding... *)
+ case (LOAD ( imm, rs, rd, unsign, width, aq)) -> { (* XXX "unsigned" causes name conflict in lem shallow embedding... *)
if (rs == 0) then () else iR := RFull(GPRstr[rs]) :: iR;
if (rd == 0) then () else oR := RFull(GPRstr[rd]) :: oR;
aR := iR;
- ik := IK_mem_read (Read_plain);
+ ik := if aq then IK_mem_read (Read_RISCV_acquire) else IK_mem_read (Read_plain);
}
case (STORE( imm, rs2, rs1, width)) -> {
if (rs2 == 0) then () else iR := RFull(GPRstr[rs2]) :: iR;
@@ -77,7 +77,13 @@ function (regfps,regfps,regfps,niafps,diafp,instruction_kind) initial_analysis (
if (rd == 0) then () else oR := RFull(GPRstr[rd]) :: oR;
}
case (FENCE(pred, succ)) -> {
- ik := IK_barrier (Barrier_MIPS_SYNC);
+ ik :=
+ switch(pred, succ) {
+ case (0b0011, 0b0011) -> IK_barrier (Barrier_RISCV_rw_rw)
+ case (0b0010, 0b0011) -> IK_barrier (Barrier_RISCV_r_rw)
+ case (0b0011, 0b0001) -> IK_barrier (Barrier_RISCV_rw_w)
+ case _ -> exit "unsupported fence"
+ };
}
};
(iR,oR,aR,Nias,Dia,ik)
diff --git a/src/lem_interp/sail_impl_base.lem b/src/lem_interp/sail_impl_base.lem
index cda6702c..1642bc81 100644
--- a/src/lem_interp/sail_impl_base.lem
+++ b/src/lem_interp/sail_impl_base.lem
@@ -426,6 +426,8 @@ type read_kind =
| Read_reserve
(* AArch64 reads *)
| Read_acquire | Read_exclusive | Read_exclusive_acquire | Read_stream
+ (* RISC-V reads *)
+ | Read_RISCV_acquire | Read_RISCV_reserved | Read_RISCV_reserved_acquire
instance (Show read_kind)
let show = function
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 10:37:31 +0000