diff options
Diffstat (limited to 'risc-v')
| -rw-r--r-- | risc-v/hgen/ast.hgen | 4 | ||||
| -rw-r--r-- | risc-v/hgen/fold.hgen | 26 | ||||
| -rw-r--r-- | risc-v/hgen/herdtools_ast_to_shallow_ast.hgen | 8 | ||||
| -rw-r--r-- | risc-v/hgen/lexer.hgen | 86 | ||||
| -rw-r--r-- | risc-v/hgen/map.hgen | 24 | ||||
| -rw-r--r-- | risc-v/hgen/parser.hgen | 7 | ||||
| -rw-r--r-- | risc-v/hgen/pretty.hgen | 42 | ||||
| -rw-r--r-- | risc-v/hgen/sail_trans_out.hgen | 8 | ||||
| -rw-r--r-- | risc-v/hgen/shallow_ast_to_herdtools_ast.hgen | 8 | ||||
| -rw-r--r-- | risc-v/hgen/token_types.hgen | 4 | ||||
| -rw-r--r-- | risc-v/hgen/trans_sail.hgen | 6 | ||||
| -rw-r--r-- | risc-v/hgen/types.hgen | 14 | ||||
| -rw-r--r-- | risc-v/hgen/types_trans_sail.hgen | 17 | ||||
| -rw-r--r-- | risc-v/riscv.sail | 155 | ||||
| -rw-r--r-- | risc-v/riscv_extras.lem | 29 | ||||
| -rw-r--r-- | risc-v/riscv_extras_embed.lem | 19 | ||||
| -rw-r--r-- | risc-v/riscv_extras_embed_sequential.lem | 19 | ||||
| -rw-r--r-- | risc-v/riscv_regfp.sail | 33 |
18 files changed, 301 insertions, 208 deletions
diff --git a/risc-v/hgen/ast.hgen b/risc-v/hgen/ast.hgen index 1839557f..b1968173 100644 --- a/risc-v/hgen/ast.hgen +++ b/risc-v/hgen/ast.hgen @@ -5,8 +5,8 @@ | `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 * bool -| `RISCVStore of bit12 * reg * reg * wordWidth * bool +| `RISCVLoad of bit12 * reg * reg * bool * wordWidth * bool * bool +| `RISCVStore of bit12 * reg * reg * wordWidth * bool * bool | `RISCVADDIW of bit12 * reg * reg | `RISCVSHIFTW of bit5 * reg * reg * riscvSop | `RISCVRTYPEW of reg * reg * reg * riscvRopw diff --git a/risc-v/hgen/fold.hgen b/risc-v/hgen/fold.hgen index d8806a37..4c51e114 100644 --- a/risc-v/hgen/fold.hgen +++ b/risc-v/hgen/fold.hgen @@ -1,16 +1,16 @@ -| `RISCVThreadStart -> (y_reg, y_sreg) -| `RISCVUTYPE (_, r0, _) -> fold_reg r0 (y_reg, y_sreg) -| `RISCVJAL (_, r0) -> fold_reg r0 (y_reg, y_sreg) -| `RISCVJALR (_, r0, r1) -> fold_reg r0 (fold_reg r1 (y_reg, y_sreg)) -| `RISCVBType (_, r0, r1, _) -> fold_reg r0 (fold_reg r1 (y_reg, y_sreg)) -| `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)) -| `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)) -| `RISCVRTYPEW (r0, r1, r2, _) -> fold_reg r0 (fold_reg r1 (fold_reg r2 (y_reg, y_sreg))) +| `RISCVThreadStart -> (y_reg, y_sreg) +| `RISCVUTYPE (_, r0, _) -> fold_reg r0 (y_reg, y_sreg) +| `RISCVJAL (_, r0) -> fold_reg r0 (y_reg, y_sreg) +| `RISCVJALR (_, r0, r1) -> fold_reg r0 (fold_reg r1 (y_reg, y_sreg)) +| `RISCVBType (_, r0, r1, _) -> fold_reg r0 (fold_reg r1 (y_reg, y_sreg)) +| `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)) +| `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)) +| `RISCVRTYPEW (r0, r1, r2, _) -> fold_reg r0 (fold_reg r1 (fold_reg r2 (y_reg, y_sreg))) | `RISCVLoadRes (_, _, rs1, _, rd) -> fold_reg rs1 (fold_reg rd (y_reg, y_sreg)) | `RISCVStoreCon (_, _, rs2, rs1, _, rd) -> fold_reg rs2 (fold_reg rs1 (fold_reg rd (y_reg, y_sreg))) | `RISCVAMO (_, _, _, rs2, rs1, _, rd) -> fold_reg rs2 (fold_reg rs1 (fold_reg rd (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 2e508678..e66608e6 100644 --- a/risc-v/hgen/herdtools_ast_to_shallow_ast.hgen +++ b/risc-v/hgen/herdtools_ast_to_shallow_ast.hgen @@ -30,18 +30,20 @@ translate_reg "rs1" rs1, translate_reg "rd" rd, translate_rop op) -| `RISCVLoad(imm, rs, rd, unsigned, width, aq) -> LOAD( +| `RISCVLoad(imm, rs, rd, unsigned, width, aq, rl) -> LOAD( translate_imm12 "imm" imm, translate_reg "rs" rs, translate_reg "rd" rd, translate_bool "unsigned" unsigned, translate_wordWidth width, - translate_bool "aq" aq) -| `RISCVStore(imm, rs, rd, width, rl) -> STORE ( + translate_bool "aq" aq, + translate_bool "rl" rl) +| `RISCVStore(imm, rs, rd, width, aq, rl) -> STORE ( translate_imm12 "imm" imm, translate_reg "rs" rs, translate_reg "rd" rd, translate_wordWidth width, + translate_bool "aq" aq, translate_bool "rl" rl) | `RISCVADDIW(imm, rs, rd) -> ADDIW( translate_imm12 "imm" imm, diff --git a/risc-v/hgen/lexer.hgen b/risc-v/hgen/lexer.hgen index 9d5df538..27df99f4 100644 --- a/risc-v/hgen/lexer.hgen +++ b/risc-v/hgen/lexer.hgen @@ -33,31 +33,44 @@ "or", RTYPE{op=RISCVOR}; "and", RTYPE{op=RISCVAND}; -"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; rl=false}; -"sh", STORE{width=RISCVHALF; rl=false}; -"sw", STORE{width=RISCVWORD; rl=false}; -"sd", STORE{width=RISCVDOUBLE; rl=false}; - -"sb.rl", STORE{width=RISCVBYTE; rl=true}; -"sh.rl", STORE{width=RISCVHALF; rl=true}; -"sw.rl", STORE{width=RISCVWORD; rl=true}; -"sd.rl", STORE{width=RISCVDOUBLE; rl=true}; +"lb", LOAD{unsigned=false; width=RISCVBYTE; aq=false; rl=false}; +"lbu", LOAD{unsigned=true; width=RISCVBYTE; aq=false; rl=false}; +"lh", LOAD{unsigned=false; width=RISCVHALF; aq=false; rl=false}; +"lhu", LOAD{unsigned=true; width=RISCVHALF; aq=false; rl=false}; +"lw", LOAD{unsigned=false; width=RISCVWORD; aq=false; rl=false}; +"lwu", LOAD{unsigned=true; width=RISCVWORD; aq=false; rl=false}; +"ld", LOAD{unsigned=false; width=RISCVDOUBLE; aq=false; rl=false}; + +"lb.aq", LOAD{unsigned=false; width=RISCVBYTE; aq=true; rl=false}; +"lbu.aq", LOAD{unsigned=true; width=RISCVBYTE; aq=true; rl=false}; +"lh.aq", LOAD{unsigned=false; width=RISCVHALF; aq=true; rl=false}; +"lhu.aq", LOAD{unsigned=true; width=RISCVHALF; aq=true; rl=false}; +"lw.aq", LOAD{unsigned=false; width=RISCVWORD; aq=true; rl=false}; +"lwu.aq", LOAD{unsigned=true; width=RISCVWORD; aq=true; rl=false}; +"ld.aq", LOAD{unsigned=false; width=RISCVDOUBLE; aq=true; rl=false}; + +"lb.aq.rl", LOAD{unsigned=false; width=RISCVBYTE; aq=true; rl=true}; +"lbu.aq.rl", LOAD{unsigned=true; width=RISCVBYTE; aq=true; rl=true}; +"lh.aq.rl", LOAD{unsigned=false; width=RISCVHALF; aq=true; rl=true}; +"lhu.aq.rl", LOAD{unsigned=true; width=RISCVHALF; aq=true; rl=true}; +"lw.aq.rl", LOAD{unsigned=false; width=RISCVWORD; aq=true; rl=true}; +"lwu.aq.rl", LOAD{unsigned=true; width=RISCVWORD; aq=true; rl=true}; +"ld.aq.rl", LOAD{unsigned=false; width=RISCVDOUBLE; aq=true; rl=true}; + +"sb", STORE{width=RISCVBYTE; aq=false; rl=false}; +"sh", STORE{width=RISCVHALF; aq=false; rl=false}; +"sw", STORE{width=RISCVWORD; aq=false; rl=false}; +"sd", STORE{width=RISCVDOUBLE; aq=false; rl=false}; + +"sb.rl", STORE{width=RISCVBYTE; aq=false; rl=true}; +"sh.rl", STORE{width=RISCVHALF; aq=false; rl=true}; +"sw.rl", STORE{width=RISCVWORD; aq=false; rl=true}; +"sd.rl", STORE{width=RISCVDOUBLE; aq=false; rl=true}; + +"sb.aq.rl", STORE{width=RISCVBYTE; aq=true; rl=true}; +"sh.aq.rl", STORE{width=RISCVHALF; aq=true; rl=true}; +"sw.aq.rl", STORE{width=RISCVWORD; aq=true; rl=true}; +"sd.aq.rl", STORE{width=RISCVDOUBLE; aq=true; rl=true}; "addiw", ADDIW (); @@ -75,17 +88,22 @@ "r", FENCEOPTION Fence_R; "w", FENCEOPTION Fence_W; "rw", FENCEOPTION Fence_RW; -"fence.i", FENCEI (); -"lr.w", LOADRES {width=RISCVWORD; aq=false; rl=false}; -"lr.w.aq", LOADRES {width=RISCVWORD; aq=true; rl=false}; -"lr.d", LOADRES {width=RISCVDOUBLE; aq=false; rl=false}; -"lr.d.aq", LOADRES {width=RISCVDOUBLE; aq=true; rl=false}; +"fence.i", FENCEI (); -"sc.w", STORECON {width=RISCVWORD; aq=false; rl=false}; -"sc.w.rl", STORECON {width=RISCVWORD; aq=false; rl=true}; -"sc.d", STORECON {width=RISCVDOUBLE; aq=false; rl=false}; -"sc.d.rl", STORECON {width=RISCVDOUBLE; aq=false; rl=true}; +"lr.w", LOADRES {width=RISCVWORD; aq=false; rl=false}; +"lr.w.aq", LOADRES {width=RISCVWORD; aq=true; rl=false}; +"lr.w.aq.rl", LOADRES {width=RISCVWORD; aq=true; rl=true}; +"lr.d", LOADRES {width=RISCVDOUBLE; aq=false; rl=false}; +"lr.d.aq", LOADRES {width=RISCVDOUBLE; aq=true; rl=false}; +"lr.d.aq.rl", LOADRES {width=RISCVDOUBLE; aq=true; rl=true}; + +"sc.w", STORECON {width=RISCVWORD; aq=false; rl=false}; +"sc.w.rl", STORECON {width=RISCVWORD; aq=false; rl=true}; +"sc.w.aq.rl", STORECON {width=RISCVWORD; aq=true; rl=true}; +"sc.d", STORECON {width=RISCVDOUBLE; aq=false; rl=false}; +"sc.d.rl", STORECON {width=RISCVDOUBLE; aq=false; rl=true}; +"sc.d.aq.rl", STORECON {width=RISCVDOUBLE; aq=true; rl=true}; "amoswap.w", AMO {width=RISCVWORD; aq=false; rl=false; op=RISCVAMOSWAP}; "amoadd.w", AMO {width=RISCVWORD; aq=false; rl=false; op=RISCVAMOADD}; diff --git a/risc-v/hgen/map.hgen b/risc-v/hgen/map.hgen index 91eecc56..bab5ced8 100644 --- a/risc-v/hgen/map.hgen +++ b/risc-v/hgen/map.hgen @@ -1,15 +1,15 @@ -| `RISCVUTYPE (x, r0, y) -> `RISCVUTYPE (x, map_reg r0, y) -| `RISCVJAL (x, r0) -> `RISCVJAL (x, map_reg r0) -| `RISCVJALR (x, r0, r1) -> `RISCVJALR (x, map_reg r0, map_reg r1) -| `RISCVBType (x, r0, r1, y) -> `RISCVBType (x, map_reg r0, map_reg r1, y) -| `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, a) -> `RISCVLoad (x, map_reg r0, map_reg r1, y, z, a) -| `RISCVStore (x, r0, r1, y, z) -> `RISCVStore (x, map_reg r0, map_reg r1, y, z) -| `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) -| `RISCVRTYPEW (r0, r1, r2, x) -> `RISCVRTYPEW (r0, map_reg r1, map_reg r2, x) +| `RISCVUTYPE (x, r0, y) -> `RISCVUTYPE (x, map_reg r0, y) +| `RISCVJAL (x, r0) -> `RISCVJAL (x, map_reg r0) +| `RISCVJALR (x, r0, r1) -> `RISCVJALR (x, map_reg r0, map_reg r1) +| `RISCVBType (x, r0, r1, y) -> `RISCVBType (x, map_reg r0, map_reg r1, y) +| `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, a, b) -> `RISCVLoad (x, map_reg r0, map_reg r1, y, z, a, b) +| `RISCVStore (x, r0, r1, y, z, a) -> `RISCVStore (x, map_reg r0, map_reg r1, y, z, a) +| `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) +| `RISCVRTYPEW (r0, r1, r2, x) -> `RISCVRTYPEW (r0, map_reg r1, map_reg r2, x) | `RISCVLoadRes (aq, rl, rs1, w, rd) -> `RISCVLoadRes (aq, rl, map_reg rs1, w, map_reg rd) | `RISCVStoreCon (aq, rl, rs2, rs1, w, rd) -> `RISCVStoreCon (aq, rl, map_reg rs2, map_reg rs1, w, map_reg rd) | `RISCVAMO (op, aq, rl, rs2, rs1, w, rd) -> `RISCVAMO (op, aq, rl, map_reg rs2, map_reg rs1, w, map_reg rd) diff --git a/risc-v/hgen/parser.hgen b/risc-v/hgen/parser.hgen index dc61e566..82bb1d5b 100644 --- a/risc-v/hgen/parser.hgen +++ b/risc-v/hgen/parser.hgen @@ -13,9 +13,9 @@ | 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, $1.aq) } + { `RISCVLoad($4, $6, $2, $1.unsigned, $1.width, $1.aq, $1.rl) } | STORE reg COMMA NUM LPAR reg RPAR - { `RISCVStore($4, $2, $6, $1.width, $1.rl) } + { `RISCVStore($4, $2, $6, $1.width, $1.aq, $1.rl) } | ADDIW reg COMMA reg COMMA NUM { `RISCVADDIW ($6, $4, $2) } | SHIFTW reg COMMA reg COMMA NUM @@ -48,3 +48,6 @@ `RISCVStoreCon($1.aq, $1.rl, $4, $8, $1.width, $2) } | AMO reg COMMA reg COMMA LPAR reg RPAR { `RISCVAMO($1.op, $1.aq, $1.rl, $4, $7, $1.width, $2) } +| AMO reg COMMA reg COMMA NUM LPAR reg RPAR + { if $6 <> 0 then failwith "'amo<op>' offset must be 0" else + `RISCVAMO($1.op, $1.aq, $1.rl, $4, $8, $1.width, $2) } diff --git a/risc-v/hgen/pretty.hgen b/risc-v/hgen/pretty.hgen index b5068c71..fc1c0000 100644 --- a/risc-v/hgen/pretty.hgen +++ b/risc-v/hgen/pretty.hgen @@ -7,34 +7,24 @@ | `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, 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, rl) - -> sprintf "%s %s, %d(%s)" (pp_riscv_store_op (width, rl)) (pp_reg rs2) imm (pp_reg rs1) + +| `RISCVLoad(imm, rs, rd, unsigned, width, aq, rl) -> + sprintf "%s %s, %d(%s)" (pp_riscv_load_op (unsigned, width, aq, rl)) (pp_reg rd) imm (pp_reg rs) + +| `RISCVStore(imm, rs2, rs1, width, aq, rl) -> + sprintf "%s %s, %d(%s)" (pp_riscv_store_op (width, aq, rl)) (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 | `RISCVRTYPEW(rs2, rs1, rd, op) -> sprintf "%s %s, %s, %s" (pp_riscv_ropw op) (pp_reg rd) (pp_reg rs1) (pp_reg rs2) | `RISCVFENCE(pred, succ) -> sprintf "fence %s, %s" (pp_riscv_fence_option pred) (pp_riscv_fence_option succ) | `RISCVFENCEI -> sprintf "fence.i" -| `RISCVLoadRes(aq, rl, rs1, width, rd) - -> - assert (rl = false); - sprintf "%s %s, (%s)" - (pp_riscv_load_reserved_op (aq, rl, width)) - (pp_reg rd) - (pp_reg rs1) -| `RISCVStoreCon(aq, rl, rs2, rs1, width, rd) - -> - assert (aq = false); - sprintf "%s %s, %s, (%s)" - (pp_riscv_store_conditional_op (aq, rl, width)) - (pp_reg rd) - (pp_reg rs2) - (pp_reg rs1) -| `RISCVAMO(op, aq, rl, rs2, rs1, width, rd) - -> - sprintf "%s %s, %s, (%s)" - (pp_riscv_amo_op (op, aq, rl, width)) - (pp_reg rd) - (pp_reg rs2) - (pp_reg rs1) + +| `RISCVLoadRes(aq, rl, rs1, width, rd) -> + sprintf "%s %s, (%s)" (pp_riscv_load_reserved_op (aq, rl, width)) (pp_reg rd) (pp_reg rs1) + +| `RISCVStoreCon(aq, rl, rs2, rs1, width, rd) -> + sprintf "%s %s, %s, (%s)" (pp_riscv_store_conditional_op (aq, rl, width)) (pp_reg rd) (pp_reg rs2) (pp_reg rs1) + +| `RISCVAMO(op, aq, rl, rs2, rs1, width, rd) -> + sprintf "%s %s, %s, (%s)" (pp_riscv_amo_op (op, aq, rl, width)) (pp_reg rd) (pp_reg rs2) (pp_reg rs1) diff --git a/risc-v/hgen/sail_trans_out.hgen b/risc-v/hgen/sail_trans_out.hgen index bec35203..2f9a80f1 100644 --- a/risc-v/hgen/sail_trans_out.hgen +++ b/risc-v/hgen/sail_trans_out.hgen @@ -6,10 +6,10 @@ | ("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; 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; rl]) - -> `RISCVStore(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_wordWidth width, translate_out_bool rl) +| ("LOAD", [imm; rs; rd; unsigned; width; aq; rl]) + -> `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, translate_out_bool rl) +| ("STORE", [imm; rs; rd; width; aq; rl]) + -> `RISCVStore(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_wordWidth width, translate_out_bool aq, translate_out_bool rl) | ("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) diff --git a/risc-v/hgen/shallow_ast_to_herdtools_ast.hgen b/risc-v/hgen/shallow_ast_to_herdtools_ast.hgen index 662b1044..23bcc4cb 100644 --- a/risc-v/hgen/shallow_ast_to_herdtools_ast.hgen +++ b/risc-v/hgen/shallow_ast_to_herdtools_ast.hgen @@ -6,10 +6,10 @@ | 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, 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, rl) - -> `RISCVStore(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_wordWidth width, translate_out_bool rl) +| LOAD( imm, rs, rd, unsigned, width, aq, rl) + -> `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, translate_out_bool rl) +| STORE( imm, rs, rd, width, aq, rl) + -> `RISCVStore(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_wordWidth width, translate_out_bool aq, translate_out_bool rl) | 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) diff --git a/risc-v/hgen/token_types.hgen b/risc-v/hgen/token_types.hgen index 9b469a27..d338d865 100644 --- a/risc-v/hgen/token_types.hgen +++ b/risc-v/hgen/token_types.hgen @@ -5,8 +5,8 @@ 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; aq: bool } -type token_Store = {width : wordWidth; rl: bool } +type token_Load = {unsigned: bool; width : wordWidth; aq: bool; rl: bool } +type token_Store = {width : wordWidth; aq: bool; rl: bool } type token_ADDIW = unit type token_SHIFTW = {op : riscvSop } type token_RTYPEW = {op : riscvRopw } diff --git a/risc-v/hgen/trans_sail.hgen b/risc-v/hgen/trans_sail.hgen index 12da62d8..8b7cbe11 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, aq) -> +| `RISCVLoad(imm, rs, rd, unsigned, width, aq, rl) -> ("LOAD", [ translate_imm12 "imm" imm; @@ -67,15 +67,17 @@ translate_bool "unsigned" unsigned; translate_width "width" width; translate_bool "aq" aq; + translate_bool "rl" rl; ], []) -| `RISCVStore(imm, rs2, rs1, width, rl) -> +| `RISCVStore(imm, rs2, rs1, width, aq, rl) -> ("STORE", [ translate_imm12 "imm" imm; translate_reg "rs2" rs2; translate_reg "rs1" rs1; translate_width "width" width; + translate_bool "aq" aq; translate_bool "rl" rl; ], []) diff --git a/risc-v/hgen/types.hgen b/risc-v/hgen/types.hgen index 83deb4a2..e0caed2d 100644 --- a/risc-v/hgen/types.hgen +++ b/risc-v/hgen/types.hgen @@ -99,7 +99,7 @@ type wordWidth = | RISCVWORD | RISCVDOUBLE -let pp_riscv_load_op (unsigned, width, aq) = +let pp_riscv_load_op (unsigned, width, aq, rl) = begin match (unsigned, width) with | (false, RISCVBYTE) -> "lb" | (true, RISCVBYTE) -> "lbu" @@ -108,17 +108,19 @@ let pp_riscv_load_op (unsigned, width, aq) = | (false, RISCVWORD) -> "lw" | (true, RISCVWORD) -> "lwu" | (_, RISCVDOUBLE) -> "ld" - end - ^ (if aq then ".aq" else "") + end ^ + (if aq then ".aq" else "") ^ + (if rl then ".rl" else "") -let pp_riscv_store_op (width, rl) = +let pp_riscv_store_op (width, aq, rl) = begin match width with | RISCVBYTE -> "sb" | RISCVHALF -> "sh" | RISCVWORD -> "sw" | RISCVDOUBLE -> "sd" - end - ^ (if rl then ".rl" else "") + end ^ + (if aq then ".aq" else "") ^ + (if rl then ".rl" else "") let pp_riscv_load_reserved_op (aq, rl, width) = "lr" ^ diff --git a/risc-v/hgen/types_trans_sail.hgen b/risc-v/hgen/types_trans_sail.hgen index 7528a522..238c7e5b 100644 --- a/risc-v/hgen/types_trans_sail.hgen +++ b/risc-v/hgen/types_trans_sail.hgen @@ -11,30 +11,47 @@ let translate_enum enum_values name value = (name, Range0 (Some size), IInt.bit_list_of_integer size (Nat_big_num.of_int index)) let translate_uop = translate_enum [RISCVLUI; RISCVAUIPC] + let translate_bop = translate_enum [RISCVBEQ; RISCVBNE; RISCVBLT; RISCVBGE; RISCVBLTU; RISCVBGEU] (* branch ops *) + let translate_iop = translate_enum [RISCVADDI; RISCVSLTI; RISCVSLTIU; RISCVXORI; RISCVORI; RISCVANDI] (* immediate ops *) + let translate_sop = translate_enum [RISCVSLLI; RISCVSRLI; RISCVSRAI] (* shift ops *) + let translate_rop = translate_enum [RISCVADD; RISCVSUB; RISCVSLL; RISCVSLT; RISCVSLTU; RISCVXOR; RISCVSRL; RISCVSRA; RISCVOR; RISCVAND] (* reg-reg ops *) + let translate_ropw = translate_enum [RISCVADDW; RISCVSUBW; RISCVSLLW; RISCVSRLW; RISCVSRAW] (* reg-reg 32-bit ops *) + let translate_amoop = translate_enum [RISCVAMOSWAP; RISCVAMOADD; RISCVAMOXOR; RISCVAMOAND; RISCVAMOOR; RISCVAMOMIN; RISCVAMOMAX; RISCVAMOMINU; RISCVAMOMAXU] + let translate_width = translate_enum [RISCVBYTE; RISCVHALF; RISCVWORD; RISCVDOUBLE] + let translate_reg name value = (name, Bvector (Some 5), bit_list_of_integer 5 (Nat_big_num.of_int (reg_to_int value))) + let translate_imm21 name value = (name, Bvector (Some 21), bit_list_of_integer 21 (Nat_big_num.of_int value)) + let translate_imm20 name value = (name, Bvector (Some 20), bit_list_of_integer 20 (Nat_big_num.of_int value)) + let translate_imm16 name value = (name, Bvector (Some 16), bit_list_of_integer 16 (Nat_big_num.of_int value)) + let translate_imm13 name value = (name, Bvector (Some 13), bit_list_of_integer 13 (Nat_big_num.of_int value)) + let translate_imm12 name value = (name, Bvector (Some 12), bit_list_of_integer 12 (Nat_big_num.of_int value)) + let translate_imm6 name value = (name, Bvector (Some 6), bit_list_of_integer 6 (Nat_big_num.of_int value)) + let translate_imm5 name value = (name, Bvector (Some 5), bit_list_of_integer 5 (Nat_big_num.of_int value)) + let translate_imm4 name value = (name, Bvector (Some 4), bit_list_of_integer 4 (Nat_big_num.of_int value)) + let translate_bool name value = (name, Bit, [if value then Bitc_one else Bitc_zero]) diff --git a/risc-v/riscv.sail b/risc-v/riscv.sail index cd0e5bf9..c5b19d26 100644 --- a/risc-v/riscv.sail +++ b/risc-v/riscv.sail @@ -62,38 +62,56 @@ 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_strong_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|] ) -> (bit[8 * 'n]) effect { rmem } MEMr_reserved_strong_acquire +function forall Nat 'n. (bit[8 * 'n]) effect { rmem } mem_read( (bit[64]) addr, ([|'n|]) width, (bool) aq, (bool) rl, (bool) res) = + switch (aq, rl, res) { + case (false, false, false) -> MEMr(addr, width) + case (true, false, false) -> MEMr_acquire(addr, width) + case (false, false, true) -> MEMr_reserved(addr, width) + case (true, false, true) -> MEMr_reserved_acquire(addr, width) + case (false, true, false) -> not_implemented("load.rl is not implemented") + case (true, true, false) -> MEMr_strong_acquire(addr, width) + case (false, true, true) -> not_implemented("lr.rl is not implemented") + case (true, true, true) -> MEMr_reserved_strong_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_strong_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|]) -> unit effect { eamem } MEMea_conditional_strong_release +function forall Nat 'n. unit effect { eamem } mem_write_ea( (bit[64]) addr , ([|'n|]) width, (bool) aq, (bool) rl, (bool) con) = + switch (aq, rl, con) { + case (false, false, false) -> MEMea(addr, width) + case (false, true, false) -> MEMea_release(addr, width) + case (false, false, true) -> MEMea_conditional(addr, width) + case (false, true , true) -> MEMea_conditional_release(addr, width) + case (true, false, false) -> not_implemented("store.aq is not implemented") + case (true, true, false) -> MEMea_strong_release(addr, width) + case (true, false, true) -> not_implemented("sc.aq is not implemented") + case (true, true , true) -> MEMea_conditional_strong_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_strong_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 forall Nat 'n. ( bit[64] , [|'n|] , bit[8*'n]) -> unit effect { wmv } MEMval_conditional_strong_release +function forall Nat 'n. unit effect { wmv } mem_write_value( (bit[64]) addr , ([|'n|]) width , (bit[8*'n]) value, (bool) aq, (bool) rl, (bool) con) = + switch (aq, rl, con) { + case (false, false, false) -> MEMval(addr, width, value) + case (false, true, false) -> MEMval_release(addr, width, value) + case (false, false, true) -> MEMval_conditional(addr, width, value) + case (false, true, true) -> MEMval_conditional_release(addr, width, value) + case (true, false, false) -> not_implemented("store.aq is not implemented") + case (true, true, false) -> MEMval_strong_release(addr, width, value) + case (true, false, true) -> not_implemented("sc.aq is not implemented") + case (true, true, true) -> MEMval_conditional_strong_release(addr, width, value) } val extern unit -> bool effect {exmem} speculate_conditional_success @@ -245,51 +263,51 @@ function clause execute (RTYPE(rs2, rs1, rd, op)) = } 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)) = +union ast member ((bit[12]), regno, regno, bool, word_width, bool, bool) LOAD +function clause decode ((bit[12]) imm : (regno) rs1 : 0b000 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, false, BYTE, false, false)) +function clause decode ((bit[12]) imm : (regno) rs1 : 0b001 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, false, HALF, false, false)) +function clause decode ((bit[12]) imm : (regno) rs1 : 0b010 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, false, WORD, false, false)) +function clause decode ((bit[12]) imm : (regno) rs1 : 0b011 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, false, DOUBLE, false, false)) +function clause decode ((bit[12]) imm : (regno) rs1 : 0b100 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, true, BYTE, false, false)) +function clause decode ((bit[12]) imm : (regno) rs1 : 0b101 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, true, HALF, false, false)) +function clause decode ((bit[12]) imm : (regno) rs1 : 0b110 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, true, WORD, false, false)) +function clause execute(LOAD(imm, rs1, rd, unsigned, width, aq, rl)) = 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) + 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) } 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) + 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) } 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)) = +union ast member ((bit[12]), regno, regno, word_width, bool, 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, false)) +function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b001 : (bit[5]) imm5 : 0b0100011) = Some(STORE(imm7 : imm5, rs2, rs1, HALF, false, false)) +function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b010 : (bit[5]) imm5 : 0b0100011) = Some(STORE(imm7 : imm5, rs2, rs1, WORD, false, false)) +function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b011 : (bit[5]) imm5 : 0b0100011) = Some(STORE(imm7 : imm5, rs2, rs1, DOUBLE, false, false)) +function clause execute (STORE(imm, rs2, rs1, width, aq, 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) + 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 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) + 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) } } @@ -360,36 +378,31 @@ 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) - } + let (bit[64]) addr = rGPR(rs1) in + let (bit[64]) result = + switch width { + case WORD -> EXTS(mem_read(addr, 4, aq, rl, true)) + case DOUBLE -> mem_read(addr, 8, aq, rl, 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])); if status == 1 then () else { (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) + case WORD -> mem_write_ea(addr, 4, aq, rl, true) + case 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], rl, true) - case DOUBLE -> mem_write_value(addr, 8, rs2_val, rl, true) + 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) }; }; } @@ -418,14 +431,14 @@ 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) + case WORD -> mem_write_ea(addr, 4, aq, rl, true) + case DOUBLE -> mem_write_ea(addr, 8, aq, rl, true) }; (bit[64]) loaded := switch (width) { - case WORD -> EXTS(mem_read(addr, 4, aq, true)) - case DOUBLE -> mem_read(addr, 8, aq, true) + case WORD -> EXTS(mem_read(addr, 4, aq, rl, true)) + case DOUBLE -> mem_read(addr, 8, aq, rl, true) }; wGPR(rd, loaded); @@ -445,8 +458,8 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = { }; switch (width) { - case WORD -> mem_write_value(addr, 4, result[31..0], rl, true) - case DOUBLE -> mem_write_value(addr, 8, result, rl, true) + case WORD -> mem_write_value(addr, 4, result[31..0], aq, rl, true) + case DOUBLE -> mem_write_value(addr, 8, result, aq, rl, true) }; } diff --git a/risc-v/riscv_extras.lem b/risc-v/riscv_extras.lem index 62a7bb91..280095e5 100644 --- a/risc-v/riscv_extras.lem +++ b/risc-v/riscv_extras.lem @@ -34,8 +34,11 @@ let memory_parameter_transformer_option_address _mode v = let read_memory_functions : memory_reads = [ ("MEMr", (MR Read_plain memory_parameter_transformer)); ("MEMr_acquire", (MR Read_RISCV_acquire memory_parameter_transformer)); + ("MEMr_strong_acquire", (MR Read_RISCV_strong_acquire memory_parameter_transformer)); ("MEMr_reserved", (MR Read_RISCV_reserved memory_parameter_transformer)); ("MEMr_reserved_acquire", (MR Read_RISCV_reserved_acquire memory_parameter_transformer)); + ("MEMr_reserved_strong_acquire", + (MR Read_RISCV_reserved_acquire memory_parameter_transformer)); ] let memory_writes : memory_writes = @@ -44,25 +47,23 @@ let memory_writes : memory_writes = let memory_eas : memory_write_eas = [ ("MEMea", (MEA Write_plain memory_parameter_transformer)); ("MEMea_release", (MEA Write_RISCV_release memory_parameter_transformer)); + ("MEMea_strong_release", (MEA Write_RISCV_strong_release memory_parameter_transformer)); ("MEMea_conditional", (MEA Write_RISCV_conditional memory_parameter_transformer)); ("MEMea_conditional_release", (MEA Write_RISCV_conditional_release memory_parameter_transformer)); + ("MEMea_conditional_strong_release", + (MEA Write_RISCV_conditional_strong_release + memory_parameter_transformer)); ] let memory_vals : memory_write_vals = - [ ("MEMval", (MV memory_parameter_transformer_option_address Nothing)); - ("MEMval_release", (MV memory_parameter_transformer_option_address Nothing)); - ("MEMval_conditional", (MV memory_parameter_transformer_option_address Nothing)); - (* (MV memory_parameter_transformer_option_address - (Just - (fun (IState interp context) b -> - let bit = Interp_ast.V_lit (L_aux (if b then L_one else L_zero) Interp_ast.Unknown) in - (IState (Interp.add_answer_to_stack interp bit) context))))); *) - ("MEMval_conditional_release", (MV memory_parameter_transformer_option_address Nothing)); - (* (MV memory_parameter_transformer_option_address - (Just - (fun (IState interp context) b -> - let bit = Interp_ast.V_lit (L_aux (if b then L_one else L_zero) Interp_ast.Unknown) in - (IState (Interp.add_answer_to_stack interp bit) context))))); *) + [ ("MEMval", (MV memory_parameter_transformer_option_address Nothing)); + ("MEMval_release", (MV memory_parameter_transformer_option_address Nothing)); + ("MEMval_strong_release", (MV memory_parameter_transformer_option_address Nothing)); + ("MEMval_conditional", (MV memory_parameter_transformer_option_address Nothing)); + ("MEMval_conditional_release",(MV memory_parameter_transformer_option_address Nothing)); + ("MEMval_conditional_strong_release", + (MV memory_parameter_transformer_option_address Nothing)); + ] let speculate_conditional_success : excl_res = diff --git a/risc-v/riscv_extras_embed.lem b/risc-v/riscv_extras_embed.lem index 3f04f9a2..d89dc44c 100644 --- a/risc-v/riscv_extras_embed.lem +++ b/risc-v/riscv_extras_embed.lem @@ -6,33 +6,48 @@ open import Prompt val MEMr : (vector bitU * integer) -> M (vector bitU) val MEMr_acquire : (vector bitU * integer) -> M (vector bitU) +val MEMr_strong_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) +val MEMr_reserved_strong_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_strong_acquire (addr,size) = read_mem false Read_RISCV_strong_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_reserved_strong_acquire (addr,size) + = read_mem false Read_RISCV_reserved_strong_acquire addr size val MEMea : (vector bitU * integer) -> M unit val MEMea_release : (vector bitU * integer) -> M unit +val MEMea_strong_release : (vector bitU * integer) -> M unit val MEMea_conditional : (vector bitU * integer) -> M unit val MEMea_conditional_release : (vector bitU * integer) -> M unit +val MEMea_conditional_strong_release : (vector bitU * integer) -> M unit let MEMea (addr,size) = write_mem_ea Write_plain addr size let MEMea_release (addr,size) = write_mem_ea Write_RISCV_release addr size +let MEMea_strong_release (addr,size) = write_mem_ea Write_RISCV_strong_release addr size let MEMea_conditional (addr,size) = write_mem_ea Write_RISCV_conditional addr size let MEMea_conditional_release (addr,size) = write_mem_ea Write_RISCV_conditional_release addr size +let MEMea_conditional_strong_release (addr,size) + = write_mem_ea Write_RISCV_conditional_strong_release addr size val MEMval : (vector bitU * integer * vector bitU) -> M unit val MEMval_release : (vector bitU * integer * vector bitU) -> M unit +val MEMval_strong_release : (vector bitU * integer * vector bitU) -> M unit val MEMval_conditional : (vector bitU * integer * vector bitU) -> M unit val MEMval_conditional_release : (vector bitU * integer * vector bitU) -> M unit +val MEMval_conditional_strong_release : (vector bitU * integer * vector bitU) -> M unit let MEMval (_,_,v) = write_mem_val v >>= fun _ -> return () let MEMval_release (_,_,v) = write_mem_val v >>= fun _ -> return () -let MEMval_conditional (_,_,v) = write_mem_val v >>= fun _ -> return () (* (if b then B1 else B0) *) -let MEMval_conditional_release (_,_,v) = write_mem_val v >>= fun _ -> return () (* (if b then B1 else B0) *) +let MEMval_strong_release (_,_,v) = write_mem_val v >>= fun _ -> return () +let MEMval_conditional (_,_,v) = write_mem_val v >>= fun _ -> return () +let MEMval_conditional_release (_,_,v) = write_mem_val v >>= fun _ -> return () +let MEMval_conditional_strong_release (_,_,v) + = write_mem_val v >>= fun _ -> return () let speculate_conditional_success () = excl_result () >>= fun b -> return (if b then B1 else B0) diff --git a/risc-v/riscv_extras_embed_sequential.lem b/risc-v/riscv_extras_embed_sequential.lem index dabd4d12..1f2a0e47 100644 --- a/risc-v/riscv_extras_embed_sequential.lem +++ b/risc-v/riscv_extras_embed_sequential.lem @@ -6,33 +6,48 @@ open import State val MEMr : (vector bitU * integer) -> M (vector bitU) val MEMr_acquire : (vector bitU * integer) -> M (vector bitU) +val MEMr_strong_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) +val MEMr_reserved_strong_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_strong_acquire (addr,size) = read_mem false Read_RISCV_strong_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_reserved_strong_acquire (addr,size) + = read_mem false Read_RISCV_reserved_strong_acquire addr size val MEMea : (vector bitU * integer) -> M unit val MEMea_release : (vector bitU * integer) -> M unit +val MEMea_strong_release : (vector bitU * integer) -> M unit val MEMea_conditional : (vector bitU * integer) -> M unit val MEMea_conditional_release : (vector bitU * integer) -> M unit +val MEMea_conditional_strong_release : (vector bitU * integer) -> M unit let MEMea (addr,size) = write_mem_ea Write_plain addr size let MEMea_release (addr,size) = write_mem_ea Write_RISCV_release addr size +let MEMea_strong_release (addr,size) = write_mem_ea Write_RISCV_strong_release addr size let MEMea_conditional (addr,size) = write_mem_ea Write_RISCV_conditional addr size let MEMea_conditional_release (addr,size) = write_mem_ea Write_RISCV_conditional_release addr size +let MEMea_conditional_strong_release (addr,size) + = write_mem_ea Write_RISCV_conditional_strong_release addr size val MEMval : (vector bitU * integer * vector bitU) -> M unit val MEMval_release : (vector bitU * integer * vector bitU) -> M unit +val MEMval_strong_release : (vector bitU * integer * vector bitU) -> M unit val MEMval_conditional : (vector bitU * integer * vector bitU) -> M unit val MEMval_conditional_release : (vector bitU * integer * vector bitU) -> M unit +val MEMval_conditional_strong_release : (vector bitU * integer * vector bitU) -> M unit let MEMval (_,_,v) = write_mem_val v >>= fun _ -> return () let MEMval_release (_,_,v) = write_mem_val v >>= fun _ -> return () -let MEMval_conditional (_,_,v) = write_mem_val v >>= fun _ -> return () (* (if b then B1 else B0) *) -let MEMval_conditional_release (_,_,v) = write_mem_val v >>= fun _ -> return () (* (if b then B1 else B0) *) +let MEMval_strong_release (_,_,v) = write_mem_val v >>= fun _ -> return () +let MEMval_conditional (_,_,v) = write_mem_val v >>= fun _ -> return () +let MEMval_conditional_release (_,_,v) = write_mem_val v >>= fun _ -> return () +let MEMval_conditional_strong_release (_,_,v) + = write_mem_val v >>= fun _ -> return () let speculate_conditional_success () = excl_result () >>= fun b -> return (if b then B1 else B0) diff --git a/risc-v/riscv_regfp.sail b/risc-v/riscv_regfp.sail index e6813c37..602f0bec 100644 --- a/risc-v/riscv_regfp.sail +++ b/risc-v/riscv_regfp.sail @@ -51,17 +51,29 @@ 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, aq)) -> { (* XXX "unsigned" causes name conflict in lem shallow embedding... *) + case (LOAD ( imm, rs, rd, unsign, width, aq, rl)) -> { (* 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 := if aq then IK_mem_read (Read_RISCV_acquire) else IK_mem_read (Read_plain); + ik := + switch (aq, rl) { + case (false, false) -> IK_mem_read (Read_plain) + case (true, false) -> IK_mem_read (Read_RISCV_acquire) + case (false, true) -> exit "not implemented" + case (true, true) -> IK_mem_read (Read_RISCV_strong_acquire) + }; } - case (STORE( imm, rs2, rs1, width, rl)) -> { + case (STORE( imm, rs2, rs1, width, aq, rl)) -> { if (rs2 == 0) then () else iR := RFull(GPRstr[rs2]) :: iR; if (rs1 == 0) then () else iR := RFull(GPRstr[rs1]) :: iR; if (rs1 == 0) then () else aR := RFull(GPRstr[rs1]) :: aR; - ik := if rl then IK_mem_write (Write_RISCV_release) else IK_mem_write (Write_plain); + ik := + switch (aq, rl) { + case (false, false) -> IK_mem_write (Write_plain) + case (true, false) -> exit "not implemented" + case (false, true) -> IK_mem_write (Write_RISCV_release) + case (true, true) -> IK_mem_write (Write_RISCV_strong_release) + }; } case (ADDIW ( imm, rs, rd)) -> { if (rs == 0) then () else iR := RFull(GPRstr[rs]) :: iR; @@ -96,7 +108,8 @@ function (regfps,regfps,regfps,niafps,diafp,instruction_kind) initial_analysis ( ik := switch (aq, rl) { case (false, false) -> IK_mem_read (Read_RISCV_reserved) case (true, false) -> IK_mem_read (Read_RISCV_reserved_acquire) - case (_, true) -> exit "not implemented" + case (false, true) -> exit "not implemented" + case (true, true) -> IK_mem_read (Read_RISCV_reserved_strong_acquire) }; } case (STORECON( aq, rl, rs2, rs1, width, rd)) -> { @@ -118,10 +131,12 @@ function (regfps,regfps,regfps,niafps,diafp,instruction_kind) initial_analysis ( if (rd == 0) then () else oR := RFull(GPRstr[rd]) :: oR; ik := switch (aq, rl) { - case (false, false) -> IK_mem_rmw (Read_RISCV_reserved, Write_RISCV_conditional) - case (false, true) -> IK_mem_rmw (Read_RISCV_reserved, Write_RISCV_conditional_release) - case (true, false) -> IK_mem_rmw (Read_RISCV_reserved_acquire, Write_RISCV_conditional) - case (true, true) -> IK_mem_rmw (Read_RISCV_reserved_acquire, Write_RISCV_conditional_release) + case (false, false) -> IK_mem_rmw (Read_RISCV_reserved, Write_RISCV_conditional) + case (false, true) -> IK_mem_rmw (Read_RISCV_reserved, Write_RISCV_conditional_release) + case (true, false) -> IK_mem_rmw (Read_RISCV_reserved_acquire, + Write_RISCV_conditional) + case (true, true) -> IK_mem_rmw (Read_RISCV_reserved_strong_acquire, + Write_RISCV_conditional_strong_release) }; } }; |