summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--risc-v/hgen/ast.hgen2
-rw-r--r--risc-v/hgen/herdtools_ast_to_shallow_ast.hgen7
-rw-r--r--risc-v/hgen/herdtools_types_to_shallow_types.hgen2
-rw-r--r--risc-v/hgen/lexer.hgen3
-rw-r--r--risc-v/hgen/parser.hgen14
-rw-r--r--risc-v/hgen/pretty.hgen2
-rw-r--r--risc-v/hgen/sail_trans_out.hgen2
-rw-r--r--risc-v/hgen/shallow_ast_to_herdtools_ast.hgen2
-rw-r--r--risc-v/hgen/shallow_types_to_herdtools_types.hgen1
-rw-r--r--risc-v/hgen/token_types.hgen2
-rw-r--r--risc-v/hgen/tokens.hgen3
-rw-r--r--risc-v/hgen/trans_sail.hgen6
-rw-r--r--risc-v/hgen/types.hgen7
-rw-r--r--risc-v/hgen/types_sail_trans_out.hgen3
-rw-r--r--risc-v/riscv.sail16
-rw-r--r--risc-v/riscv_extras.lem6
-rw-r--r--risc-v/riscv_extras_embed.lem8
-rw-r--r--risc-v/riscv_extras_embed_sequential.lem9
-rw-r--r--src/lem_interp/sail_impl_base.lem5
19 files changed, 75 insertions, 25 deletions
diff --git a/risc-v/hgen/ast.hgen b/risc-v/hgen/ast.hgen
index 2860484e..8983b5ae 100644
--- a/risc-v/hgen/ast.hgen
+++ b/risc-v/hgen/ast.hgen
@@ -10,4 +10,4 @@
| `RISCVADDIW of bit12 * reg * reg
| `RISCVSHIFTW of bit5 * reg * reg * riscvSop
| `RISCVRTYPEW of reg * reg * reg * riscvRopw
-| `RISCVFENCE
+| `RISCVFENCE of bit4 * bit4
diff --git a/risc-v/hgen/herdtools_ast_to_shallow_ast.hgen b/risc-v/hgen/herdtools_ast_to_shallow_ast.hgen
index 16d827e2..50026612 100644
--- a/risc-v/hgen/herdtools_ast_to_shallow_ast.hgen
+++ b/risc-v/hgen/herdtools_ast_to_shallow_ast.hgen
@@ -55,7 +55,6 @@
translate_reg "rs1" rs1,
translate_reg "rd" rd,
translate_ropw op)
-| `RISCVFENCE -> FENCE (
- translate_imm4 "pred" 0,
- translate_imm4 "succ" 0
-)
+| `RISCVFENCE(pred, succ) -> FENCE(
+ translate_imm4 "pred" pred,
+ translate_imm4 "succ" succ)
diff --git a/risc-v/hgen/herdtools_types_to_shallow_types.hgen b/risc-v/hgen/herdtools_types_to_shallow_types.hgen
index 361c0e61..4d8bd87a 100644
--- a/risc-v/hgen/herdtools_types_to_shallow_types.hgen
+++ b/risc-v/hgen/herdtools_types_to_shallow_types.hgen
@@ -75,5 +75,5 @@ let translate_imm6 name value =
let translate_imm5 name value =
Sail_values.to_vec0 is_inc (Nat_big_num.of_int 5,Nat_big_num.of_int value)
-let translate_imm4 name value =
+let translate_imm4 name value =
Sail_values.to_vec0 is_inc (Nat_big_num.of_int 4,Nat_big_num.of_int value)
diff --git a/risc-v/hgen/lexer.hgen b/risc-v/hgen/lexer.hgen
index 3badc338..5f2c8326 100644
--- a/risc-v/hgen/lexer.hgen
+++ b/risc-v/hgen/lexer.hgen
@@ -59,3 +59,6 @@
"sraw", RTYPEW{op=RISCVSRAW};
"fence", FENCE ();
+"r", FENCEOPTION Fence_R;
+"w", FENCEOPTION Fence_W;
+"rw", FENCEOPTION Fence_RW;
diff --git a/risc-v/hgen/parser.hgen b/risc-v/hgen/parser.hgen
index 8bb8ae2b..37fd8d8d 100644
--- a/risc-v/hgen/parser.hgen
+++ b/risc-v/hgen/parser.hgen
@@ -22,5 +22,15 @@
{ `RISCVSHIFTW ($6, $4, $2, $1.op) }
| RTYPEW reg COMMA reg COMMA reg
{ `RISCVRTYPEW ($6, $4, $2, $1.op) }
-| FENCE
- { `RISCVFENCE }
+| FENCE FENCEOPTION COMMA FENCEOPTION
+ { match ($2, $4) with
+ | (Fence_RW, Fence_RW) -> `RISCVFENCE (0b0011, 0b0011)
+ | (Fence_R, Fence_RW) -> `RISCVFENCE (0b0010, 0b0011)
+ | (Fence_RW, Fence_W) -> `RISCVFENCE (0b0011, 0b0001)
+ | (Fence_RW, Fence_R) -> failwith "'fence rw,r' is not supported"
+ | (Fence_R, Fence_R) -> failwith "'fence r,r' is not supported"
+ | (Fence_R, Fence_W) -> failwith "'fence r,w' is not supported"
+ | (Fence_W, Fence_RW) -> failwith "'fence w,rw' is not supported"
+ | (Fence_W, Fence_R) -> failwith "'fence w,r' is not supported"
+ | (Fence_W, Fence_W) -> failwith "'fence w,w' is not supported"
+ }
diff --git a/risc-v/hgen/pretty.hgen b/risc-v/hgen/pretty.hgen
index 0373783d..1da3ef11 100644
--- a/risc-v/hgen/pretty.hgen
+++ b/risc-v/hgen/pretty.hgen
@@ -12,4 +12,4 @@
| `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
| `RISCVRTYPEW(rs2, rs1, rd, op) -> sprintf "%s %s, %s, %s" (pp_riscv_ropw op) (pp_reg rd) (pp_reg rs1) (pp_reg rs2)
-| `RISCVFENCE -> "fence"
+| `RISCVFENCE(pred, succ) -> sprintf "fence %s, %s" (pp_riscv_fence_option pred) (pp_riscv_fence_option succ)
diff --git a/risc-v/hgen/sail_trans_out.hgen b/risc-v/hgen/sail_trans_out.hgen
index 6073242e..dca5bea1 100644
--- a/risc-v/hgen/sail_trans_out.hgen
+++ b/risc-v/hgen/sail_trans_out.hgen
@@ -11,4 +11,4 @@
| ("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)
| ("RTYPEW", [rs2; rs1; rd; op]) -> `RISCVRTYPEW(translate_out_ireg rs2, translate_out_ireg rs1, translate_out_ireg rd, translate_out_ropw op)
-| ("FENCE", []) -> `RISCVFENCE
+| ("FENCE", [pred; succ]) -> `RISCVFENCE(translate_out_imm4 pred, translate_out_imm4 succ)
diff --git a/risc-v/hgen/shallow_ast_to_herdtools_ast.hgen b/risc-v/hgen/shallow_ast_to_herdtools_ast.hgen
index da9047a3..6158ebd7 100644
--- a/risc-v/hgen/shallow_ast_to_herdtools_ast.hgen
+++ b/risc-v/hgen/shallow_ast_to_herdtools_ast.hgen
@@ -11,4 +11,4 @@
| 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)
| RTYPEW( rs2, rs1, rd, op) -> `RISCVRTYPEW(translate_out_ireg rs2, translate_out_ireg rs1, translate_out_ireg rd, translate_out_ropw op)
-| FENCE(pred, succ) -> `RISCVFENCE
+| FENCE( pred, succ) -> `RISCVFENCE(translate_out_imm4 pred, translate_out_imm4 succ)
diff --git a/risc-v/hgen/shallow_types_to_herdtools_types.hgen b/risc-v/hgen/shallow_types_to_herdtools_types.hgen
index 8ef18f06..a891d7d0 100644
--- a/risc-v/hgen/shallow_types_to_herdtools_types.hgen
+++ b/risc-v/hgen/shallow_types_to_herdtools_types.hgen
@@ -70,3 +70,4 @@ let translate_out_simm13 imm = translate_out_signed_int imm 13
let translate_out_simm12 imm = translate_out_signed_int imm 12
let translate_out_imm6 imm = translate_out_int imm
let translate_out_imm5 imm = translate_out_int imm
+let translate_out_imm4 imm = translate_out_int imm
diff --git a/risc-v/hgen/token_types.hgen b/risc-v/hgen/token_types.hgen
index e778d2a9..2980b985 100644
--- a/risc-v/hgen/token_types.hgen
+++ b/risc-v/hgen/token_types.hgen
@@ -11,3 +11,5 @@ type token_ADDIW = unit
type token_SHIFTW = {op : riscvSop }
type token_RTYPEW = {op : riscvRopw }
type token_FENCE = unit
+
+type token_FENCEOPTION = Fence_R | Fence_W | Fence_RW
diff --git a/risc-v/hgen/tokens.hgen b/risc-v/hgen/tokens.hgen
index abe6a6c3..f952cf77 100644
--- a/risc-v/hgen/tokens.hgen
+++ b/risc-v/hgen/tokens.hgen
@@ -10,4 +10,5 @@
%token <RISCVHGenBase.token_ADDIW> ADDIW
%token <RISCVHGenBase.token_SHIFTW> SHIFTW
%token <RISCVHGenBase.token_RTYPEW> RTYPEW
-%token <RISCVHGenBase.token_FENCE> FENCE
+%token <RISCVHGenBase.token_FENCE> FENCE
+%token <RISCVHGenBase.token_FENCEOPTION> FENCEOPTION
diff --git a/risc-v/hgen/trans_sail.hgen b/risc-v/hgen/trans_sail.hgen
index c72e84d5..df22d9dc 100644
--- a/risc-v/hgen/trans_sail.hgen
+++ b/risc-v/hgen/trans_sail.hgen
@@ -103,10 +103,10 @@
translate_ropw "op" op;
],
[])
-| `RISCVFENCE ->
+| `RISCVFENCE(pred, succ) ->
("FENCE",
[
- translate_imm4 "pred" 0;
- translate_imm4 "succ" 0;
+ translate_imm4 "pred" pred;
+ translate_imm4 "succ" succ;
],
[])
diff --git a/risc-v/hgen/types.hgen b/risc-v/hgen/types.hgen
index e31b11f8..87fc9b95 100644
--- a/risc-v/hgen/types.hgen
+++ b/risc-v/hgen/types.hgen
@@ -2,6 +2,7 @@ type bit20 = int
type bit12 = int
type bit6 = int
type bit5 = int
+type bit4 = int
type riscvUop = (* upper immediate ops *)
| RISCVLUI
@@ -114,3 +115,9 @@ let pp_riscv_store_op width = match width with
| RISCVWORD -> "sw"
| RISCVDOUBLE -> "sd"
| _ -> failwith "unexpected store op"
+
+let pp_riscv_fence_option = function
+ | 0b0011 -> "rw"
+ | 0b0010 -> "r"
+ | 0b0001 -> "w"
+ | _ -> failwith "unexpected fence option"
diff --git a/risc-v/hgen/types_sail_trans_out.hgen b/risc-v/hgen/types_sail_trans_out.hgen
index 297d0cf3..e22110d0 100644
--- a/risc-v/hgen/types_sail_trans_out.hgen
+++ b/risc-v/hgen/types_sail_trans_out.hgen
@@ -17,6 +17,7 @@ let translate_out_simm13 imm = translate_out_signed_int imm 13
let translate_out_simm12 imm = translate_out_signed_int imm 12
let translate_out_imm6 imm = translate_out_int imm
let translate_out_imm5 imm = translate_out_int imm
+let translate_out_imm4 imm = translate_out_int imm
let translate_out_bool = function
| (name, Bit, [Bitc_one]) -> true
@@ -82,4 +83,4 @@ let translate_out_ropw op = match translate_out_enum op with
| 2 -> RISCVSLLW
| 3 -> RISCVSRLW
| 4 -> RISCVSRAW
-| _ -> failwith "Unknown ropw in sail translate out" \ No newline at end of file
+| _ -> failwith "Unknown ropw in sail translate out"
diff --git a/risc-v/riscv.sail b/risc-v/riscv.sail
index 962d8280..4a80adb0 100644
--- a/risc-v/riscv.sail
+++ b/risc-v/riscv.sail
@@ -52,10 +52,17 @@ 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|]) -> 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_sync
+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
(* Ideally these would be sail builtin *)
function (bit[64]) shift_right_arith64 ((bit[64]) v, (bit[6]) shift) =
@@ -285,7 +292,12 @@ function clause execute (RTYPEW(rs2, rs1, rd, op)) =
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)) = {
- MEM_sync(); (* XXX use pred and 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 _ -> not_implemented("unsupported fence")
+ }
}
union ast member unit FENCEI
diff --git a/risc-v/riscv_extras.lem b/risc-v/riscv_extras.lem
index c09c85c2..aa5d8fb8 100644
--- a/risc-v/riscv_extras.lem
+++ b/risc-v/riscv_extras.lem
@@ -53,6 +53,8 @@ let memory_vals : memory_write_vals =
(IState (Interp.add_answer_to_stack interp bit) context)))));
]
-let barrier_functions = [
- ("MEM_sync", Barrier_MIPS_SYNC);
+let barrier_functions =
+ [ ("MEM_fence_rw_rw", Barrier_RISCV_rw_rw);
+ ("MEM_fence_r_rw", Barrier_RISCV_r_rw);
+ ("MEM_fence_rw_w", Barrier_RISCV_rw_w);
]
diff --git a/risc-v/riscv_extras_embed.lem b/risc-v/riscv_extras_embed.lem
index cbc8bd0d..1146d1cd 100644
--- a/risc-v/riscv_extras_embed.lem
+++ b/risc-v/riscv_extras_embed.lem
@@ -22,9 +22,13 @@ val MEMval_conditional : (vector bitU * integer * vector bitU) -> M bitU
let MEMval (_,_,v) = write_mem_val v >>= fun _ -> return ()
let MEMval_conditional (_,_,v) = write_mem_val v >>= fun b -> return (if b then B1 else B0)
-val MEM_sync : unit -> M unit
+val MEM_fence_rw_rw : unit -> M unit
+val MEM_fence_r_rw : unit -> M unit
+val MEM_fence_rw_w : unit -> M unit
-let MEM_sync () = barrier Barrier_Isync
+let MEM_fence_rw_rw () = barrier Barrier_RISCV_rw_rw
+let MEM_fence_r_rw () = barrier Barrier_RISCV_r_rw
+let MEM_fence_rw_w () = barrier Barrier_RISCV_rw_w
let duplicate (bit,len) =
let bits = repeat [bit] len in
diff --git a/risc-v/riscv_extras_embed_sequential.lem b/risc-v/riscv_extras_embed_sequential.lem
index 7fb62161..f6709ff7 100644
--- a/risc-v/riscv_extras_embed_sequential.lem
+++ b/risc-v/riscv_extras_embed_sequential.lem
@@ -23,10 +23,13 @@ val MEMval_conditional : (vector bitU * integer * vector bitU) -> M bitU
let MEMval (_,_,v) = write_mem_val v >>= fun _ -> return ()
let MEMval_conditional (_,_,v) = write_mem_val v >>= fun b -> return (if b then B1 else B0)
-val MEM_sync : unit -> M unit
-
-let MEM_sync () = barrier Barrier_MIPS_SYNC
+val MEM_fence_rw_rw : unit -> M unit
+val MEM_fence_r_rw : unit -> M unit
+val MEM_fence_rw_w : unit -> M unit
+let MEM_fence_rw_rw () = barrier Barrier_RISCV_rw_rw
+let MEM_fence_r_rw () = barrier Barrier_RISCV_r_rw
+let MEM_fence_rw_w () = barrier Barrier_RISCV_rw_w
let duplicate (bit,len) =
let bits = repeat [bit] len in
diff --git a/src/lem_interp/sail_impl_base.lem b/src/lem_interp/sail_impl_base.lem
index 0cdeb414..cda6702c 100644
--- a/src/lem_interp/sail_impl_base.lem
+++ b/src/lem_interp/sail_impl_base.lem
@@ -465,6 +465,11 @@ type barrier_kind =
| Barrier_TM_COMMIT
(* MIPS barriers *)
| Barrier_MIPS_SYNC
+ (* RISC-V barriers *)
+ | Barrier_RISCV_rw_rw
+ | Barrier_RISCV_r_rw
+ | Barrier_RISCV_rw_w
+
instance (Show barrier_kind)
let show = function
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 08:16:36 +0000