diff options
| -rw-r--r-- | riscv/Makefile | 3 | ||||
| -rw-r--r-- | riscv/riscv.sail | 18 | ||||
| -rw-r--r-- | riscv/riscv_types.sail | 6 |
3 files changed, 21 insertions, 6 deletions
diff --git a/riscv/Makefile b/riscv/Makefile index 00451f6f..7f52dde7 100644 --- a/riscv/Makefile +++ b/riscv/Makefile @@ -5,6 +5,9 @@ export SAIL_DIR all: riscv Riscv_embed_sequential.thy +check: $(SAIL_SRCS) main.sail + $(SAIL_DIR)/sail $^ + riscv: $(SAIL_SRCS) main.sail $(SAIL_DIR)/sail -ocaml -o riscv $^ diff --git a/riscv/riscv.sail b/riscv/riscv.sail index 7007086f..72b3aec9 100644 --- a/riscv/riscv.sail +++ b/riscv/riscv.sail @@ -310,7 +310,8 @@ function clause execute(LOADRES(aq, rl, rs1, width, rd)) = let result : bits(64) = match width { WORD => EXTS(mem_read(addr, 4, aq, rl, true)), - DOUBLE => mem_read(addr, 8, aq, rl, true) + DOUBLE => mem_read(addr, 8, aq, rl, true), + _ => internal_error("LOADRES expected WORD or DOUBLE") } in wGPR(rd, result) @@ -328,12 +329,14 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = { addr : bits(64) = rGPR(rs1); match width { WORD => mem_write_ea(addr, 4, aq, rl, true), - DOUBLE => mem_write_ea(addr, 8, aq, rl, true) + DOUBLE => mem_write_ea(addr, 8, aq, rl, true), + _ => internal_error("STORECON expected word or double") }; rs2_val = rGPR(rs2); match width { WORD => mem_write_value(addr, 4, rs2_val[31..0], aq, rl, true), - DOUBLE => mem_write_value(addr, 8, rs2_val, aq, rl, true) + DOUBLE => mem_write_value(addr, 8, rs2_val, aq, rl, true), + _ => internal_error("STORECON expected word or double") }; }; } @@ -365,13 +368,15 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = { match width { WORD => mem_write_ea(addr, 4, aq & rl, rl, true), - DOUBLE => mem_write_ea(addr, 8, aq & rl, rl, true) + DOUBLE => mem_write_ea(addr, 8, aq & rl, rl, true), + _ => internal_error ("AMO expected WORD or DOUBLE") }; loaded : bits(64) = match width { WORD => EXTS(mem_read(addr, 4, aq, aq & rl, true)), - DOUBLE => mem_read(addr, 8, aq, aq & rl, true) + DOUBLE => mem_read(addr, 8, aq, aq & rl, true), + _ => internal_error ("AMO expected WORD or DOUBLE") }; wGPR(rd) = loaded; @@ -393,7 +398,8 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = { match width { WORD => mem_write_value(addr, 4, result[31..0], aq & rl, rl, true), - DOUBLE => mem_write_value(addr, 8, result, aq & rl, rl, true) + DOUBLE => mem_write_value(addr, 8, result, aq & rl, rl, true), + _ => internal_error("AMO expected WORD or DOUBLE") }; } diff --git a/riscv/riscv_types.sail b/riscv/riscv_types.sail index bfb80b49..e627518d 100644 --- a/riscv/riscv_types.sail +++ b/riscv/riscv_types.sail @@ -2,6 +2,12 @@ val not_implemented : forall ('a : Type). string -> 'a effect {escape} function not_implemented message = throw(Error_not_implemented(message)) +val internal_error : forall ('a : Type). string -> 'a effect {escape} +function internal_error(s) = { + assert (false, s); + throw (Error_internal_error) +} + type regval = bits(64) type regno ('n : Int), 0 <= 'n < 32 = atom('n) |