diff options
-rw-r--r-- | Makefile | 4 | ||||
-rw-r--r-- | handwritten_support/mem_metadata.v | 2 | ||||
-rw-r--r-- | handwritten_support/riscv_extras.v | 22 | ||||
-rw-r--r-- | model/riscv_csr_ext.sail | 8 | ||||
-rw-r--r-- | model/riscv_csr_map.sail | 1 | ||||
-rw-r--r-- | model/riscv_insts_aext.sail | 33 | ||||
-rw-r--r-- | model/riscv_insts_zicsr.sail | 4 | ||||
-rw-r--r-- | model/riscv_mem.sail | 50 | ||||
-rw-r--r-- | model/riscv_types.sail | 8 | ||||
-rw-r--r-- | model/riscv_types_common.sail | 1 | ||||
-rw-r--r-- | model/riscv_types_ext.sail | 12 |
11 files changed, 84 insertions, 61 deletions
@@ -60,10 +60,10 @@ SAIL_REGS_SRCS += riscv_pmp_regs.sail riscv_pmp_control.sail SAIL_REGS_SRCS += riscv_ext_regs.sail $(SAIL_CHECK_SRCS) SAIL_ARCH_SRCS = $(PRELUDE) -SAIL_ARCH_SRCS += riscv_types_ext.sail riscv_types.sail +SAIL_ARCH_SRCS += riscv_types_common.sail riscv_types_ext.sail riscv_types.sail SAIL_ARCH_SRCS += riscv_vmem_types.sail $(SAIL_REGS_SRCS) $(SAIL_SYS_SRCS) riscv_platform.sail SAIL_ARCH_SRCS += riscv_mem.sail $(SAIL_VM_SRCS) -SAIL_ARCH_RVFI_SRCS = $(PRELUDE) rvfi_dii.sail riscv_types_ext.sail riscv_types.sail riscv_vmem_types.sail $(SAIL_REGS_SRCS) $(SAIL_SYS_SRCS) riscv_platform.sail riscv_mem.sail $(SAIL_VM_SRCS) +SAIL_ARCH_RVFI_SRCS = $(PRELUDE) rvfi_dii.sail riscv_types_common.sail riscv_types_ext.sail riscv_types.sail riscv_vmem_types.sail $(SAIL_REGS_SRCS) $(SAIL_SYS_SRCS) riscv_platform.sail riscv_mem.sail $(SAIL_VM_SRCS) SAIL_STEP_SRCS = riscv_step_common.sail riscv_step_ext.sail riscv_decode_ext.sail riscv_fetch.sail riscv_step.sail RVFI_STEP_SRCS = riscv_step_common.sail riscv_step_rvfi.sail riscv_decode_ext.sail riscv_fetch_rvfi.sail riscv_step.sail diff --git a/handwritten_support/mem_metadata.v b/handwritten_support/mem_metadata.v index 0e53888..e70d395 100644 --- a/handwritten_support/mem_metadata.v +++ b/handwritten_support/mem_metadata.v @@ -6,6 +6,6 @@ Require Import Sail2_prompt. Definition write_ram {rv e a} wk (addr : mword a) size (v : mword (8 * size)) (meta : unit) : monad rv bool e := write_mem wk a addr size v. -Definition read_ram {rv e a} rk (addr : mword a) size (read_tag : bool) `{ArithFact (size >= 0)} : monad rv (mword (8 * size) * unit) e := +Definition read_ram {rv e a} rk (addr : mword a) size (read_tag : bool) `{ArithFact (size >=? 0)} : monad rv (mword (8 * size) * unit) e := read_mem rk a addr size >>= fun data => returnm (data, tt). diff --git a/handwritten_support/riscv_extras.v b/handwritten_support/riscv_extras.v index 84f6761..7e350ed 100644 --- a/handwritten_support/riscv_extras.v +++ b/handwritten_support/riscv_extras.v @@ -45,12 +45,12 @@ val MEMr_reserved_acquire : forall 'rv 'a 'b 'e. Size 'a, Size 'b => inte val MEMr_reserved_strong_acquire : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e *) -Definition MEMr {rv e} addrsize size (hexRAM addr : mword addrsize) `{ArithFact (size >= 0)} : monad rv (mword (8 * size)) e := read_mem Read_plain addrsize addr size. -Definition MEMr_acquire {rv e} addrsize size (hexRAM addr : mword addrsize) `{ArithFact (size >= 0)} : monad rv (mword (8 * size)) e := read_mem Read_RISCV_acquire addrsize addr size. -Definition MEMr_strong_acquire {rv e} addrsize size (hexRAM addr : mword addrsize) `{ArithFact (size >= 0)} : monad rv (mword (8 * size)) e := read_mem Read_RISCV_strong_acquire addrsize addr size. -Definition MEMr_reserved {rv e} addrsize size (hexRAM addr : mword addrsize) `{ArithFact (size >= 0)} : monad rv (mword (8 * size)) e := read_mem Read_RISCV_reserved addrsize addr size. -Definition MEMr_reserved_acquire {rv e} addrsize size (hexRAM addr : mword addrsize) `{ArithFact (size >= 0)} : monad rv (mword (8 * size)) e := read_mem Read_RISCV_reserved_acquire addrsize addr size. -Definition MEMr_reserved_strong_acquire {rv e} addrsize size (hexRAM addr : mword addrsize) `{ArithFact (size >= 0)} : monad rv (mword (8 * size)) e := read_mem Read_RISCV_reserved_strong_acquire addrsize addr size. +Definition MEMr {rv e} addrsize size (hexRAM addr : mword addrsize) `{ArithFact (size >=? 0)} : monad rv (mword (8 * size)) e := read_mem Read_plain addrsize addr size. +Definition MEMr_acquire {rv e} addrsize size (hexRAM addr : mword addrsize) `{ArithFact (size >=? 0)} : monad rv (mword (8 * size)) e := read_mem Read_RISCV_acquire addrsize addr size. +Definition MEMr_strong_acquire {rv e} addrsize size (hexRAM addr : mword addrsize) `{ArithFact (size >=? 0)} : monad rv (mword (8 * size)) e := read_mem Read_RISCV_strong_acquire addrsize addr size. +Definition MEMr_reserved {rv e} addrsize size (hexRAM addr : mword addrsize) `{ArithFact (size >=? 0)} : monad rv (mword (8 * size)) e := read_mem Read_RISCV_reserved addrsize addr size. +Definition MEMr_reserved_acquire {rv e} addrsize size (hexRAM addr : mword addrsize) `{ArithFact (size >=? 0)} : monad rv (mword (8 * size)) e := read_mem Read_RISCV_reserved_acquire addrsize addr size. +Definition MEMr_reserved_strong_acquire {rv e} addrsize size (hexRAM addr : mword addrsize) `{ArithFact (size >=? 0)} : monad rv (mword (8 * size)) e := read_mem Read_RISCV_reserved_strong_acquire addrsize addr size. (* val MEMw : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> bitvector 'b -> monad 'rv bool 'e @@ -87,14 +87,14 @@ Definition undefined_string {rv e} (_:unit) : monad rv string e := returnm ""%st Definition undefined_unit {rv e} (_:unit) : monad rv unit e := returnm tt. Definition undefined_int {rv e} (_:unit) : monad rv Z e := returnm (0:ii). (*val undefined_vector : forall 'rv 'a 'e. integer -> 'a -> monad 'rv (list 'a) 'e*) -Definition undefined_vector {rv a e} len (u : a) `{ArithFact (len >= 0)} : monad rv (vec a len) e := returnm (vec_init u len). +Definition undefined_vector {rv a e} len (u : a) `{ArithFact (len >=? 0)} : monad rv (vec a len) e := returnm (vec_init u len). (*val undefined_bitvector : forall 'rv 'a 'e. Bitvector 'a => integer -> monad 'rv 'a 'e*) -Definition undefined_bitvector {rv e} len `{ArithFact (len >= 0)} : monad rv (mword len) e := returnm (mword_of_int 0). +Definition undefined_bitvector {rv e} len `{ArithFact (len >=? 0)} : monad rv (mword len) e := returnm (mword_of_int 0). (*val undefined_bits : forall 'rv 'a 'e. Bitvector 'a => integer -> monad 'rv 'a 'e*) Definition undefined_bits {rv e} := @undefined_bitvector rv e. Definition undefined_bit {rv e} (_:unit) : monad rv bitU e := returnm BU. (*Definition undefined_real {rv e} (_:unit) : monad rv real e := returnm (realFromFrac 0 1).*) -Definition undefined_range {rv e} i j `{ArithFact (i <= j)} : monad rv {z : Z & ArithFact (i <= z /\ z <= j)} e := returnm (build_ex i). +Definition undefined_range {rv e} i j `{ArithFact (i <=? j)} : monad rv {z : Z & ArithFact (i <=? z <=? j)} e := returnm (build_ex i). Definition undefined_atom {rv e} i : monad rv Z e := returnm i. Definition undefined_nat {rv e} (_:unit) : monad rv Z e := returnm (0:ii). @@ -119,10 +119,12 @@ Definition eq_bit (x : bitU) (y : bitU) : bool := end. Require Import Zeuclid. -Definition euclid_modulo (m n : Z) `{ArithFact (n > 0)} : {z : Z & ArithFact (0 <= z <= n-1)}. +Definition euclid_modulo (m n : Z) `{ArithFact (n >? 0)} : {z : Z & ArithFact (0 <=? z <=? n-1)}. apply existT with (x := ZEuclid.modulo m n). constructor. destruct H. +unbool_comparisons. +unbool_comparisons_goal. assert (Z.abs n = n). { rewrite Z.abs_eq; auto with zarith. } rewrite <- H at 3. lapply (ZEuclid.mod_always_pos m n); omega. diff --git a/model/riscv_csr_ext.sail b/model/riscv_csr_ext.sail index 8c0cc17..9220534 100644 --- a/model/riscv_csr_ext.sail +++ b/model/riscv_csr_ext.sail @@ -1,8 +1,12 @@ -/* numeric fallback XXX apparent sail bug prevents this from compiling for C */ -//mapping clause csr_name_map = reg <-> "UNKNOWN CSR: " ^ hex_bits_12(reg) +mapping clause csr_name_map = reg <-> hex_bits_12(reg) end csr_name_map +/* XXX due to an apparent Sail bug the definition of this function must appear + after the last csr_name_map clause and not by the val spec as it was + previously. */ +function csr_name(csr) = csr_name_map(csr) + function clause ext_is_CSR_defined(_, _) = false end ext_is_CSR_defined diff --git a/model/riscv_csr_map.sail b/model/riscv_csr_map.sail index 7ec161b..ba52da6 100644 --- a/model/riscv_csr_map.sail +++ b/model/riscv_csr_map.sail @@ -93,7 +93,6 @@ mapping clause csr_name_map = 0x7a2 <-> "tdata2" mapping clause csr_name_map = 0x7a3 <-> "tdata3" val csr_name : csreg -> string -function csr_name(csr) = csr_name_map(csr) overload to_str = {csr_name} /* Extensions may want to add additional CSR registers to the CSR address map. diff --git a/model/riscv_insts_aext.sail b/model/riscv_insts_aext.sail index f430a75..e760b90 100644 --- a/model/riscv_insts_aext.sail +++ b/model/riscv_insts_aext.sail @@ -198,21 +198,30 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = { let eares : MemoryOpResult(unit) = match (width, sizeof(xlen)) { (WORD, _) => mem_write_ea(addr, 4, aq & rl, rl, true), (DOUBLE, 64) => mem_write_ea(addr, 8, aq & rl, rl, true), - _ => internal_error ("AMO expected WORD or DOUBLE") + _ => internal_error("AMO expected WORD or DOUBLE") + }; + let is_unsigned : bool = match op { + AMOMINU => true, + AMOMAXU => true, + _ => false + }; + let rs2_val : xlenbits = match width { + WORD => if is_unsigned then EXTZ(X(rs2)[31..0]) else EXTS(X(rs2)[31..0]), + DOUBLE => X(rs2), + _ => internal_error("AMO expected WORD or DOUBLE") }; - rs2_val : xlenbits = X(rs2); match (eares) { MemException(e) => { handle_mem_exception(addr, e); RETIRE_FAIL }, MemValue(_) => { - let rval : MemoryOpResult(xlenbits) = match (width, sizeof(xlen)) { - (WORD, _) => extend_value(false, mem_read(ReadWrite(Data), addr, 4, aq, aq & rl, true)), - (DOUBLE, 64) => extend_value(false, mem_read(ReadWrite(Data), addr, 8, aq, aq & rl, true)), - _ => internal_error ("AMO expected WORD or DOUBLE") + let mval : MemoryOpResult(xlenbits) = match (width, sizeof(xlen)) { + (WORD, _) => extend_value(is_unsigned, mem_read(ReadWrite(Data), addr, 4, aq, aq & rl, true)), + (DOUBLE, 64) => extend_value(is_unsigned, mem_read(ReadWrite(Data), addr, 8, aq, aq & rl, true)), + _ => internal_error("AMO expected WORD or DOUBLE") }; - match (rval) { + match (mval) { MemException(e) => { handle_mem_exception(addr, e); RETIRE_FAIL }, MemValue(loaded) => { - result : xlenbits = + let result : xlenbits = match op { AMOSWAP => rs2_val, AMOADD => rs2_val + loaded, @@ -228,14 +237,18 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = { AMOMINU => to_bits(sizeof(xlen), min(unsigned(rs2_val), unsigned(loaded))), AMOMAXU => to_bits(sizeof(xlen), max(unsigned(rs2_val), unsigned(loaded))) }; - + let rval : xlenbits = match width { + WORD => EXTS(loaded[31..0]), + DOUBLE => loaded, + _ => internal_error("AMO expected WORD or DOUBLE") + }; let wval : MemoryOpResult(bool) = match (width, sizeof(xlen)) { (WORD, _) => mem_write_value(addr, 4, result[31..0], aq & rl, rl, true), (DOUBLE, 64) => mem_write_value(addr, 8, result, aq & rl, rl, true), _ => internal_error("AMO expected WORD or DOUBLE") }; match (wval) { - MemValue(true) => { X(rd) = loaded; RETIRE_SUCCESS }, + MemValue(true) => { X(rd) = rval; RETIRE_SUCCESS }, MemValue(false) => { internal_error("AMO got false from mem_write_value") }, MemException(e) => { handle_mem_exception(addr, e); RETIRE_FAIL } } diff --git a/model/riscv_insts_zicsr.sail b/model/riscv_insts_zicsr.sail index 056f537..3a23d9a 100644 --- a/model/riscv_insts_zicsr.sail +++ b/model/riscv_insts_zicsr.sail @@ -208,6 +208,6 @@ mapping csr_mnemonic : csrop <-> string = { } mapping clause assembly = CSR(csr, rs1, rd, true, op) - <-> csr_mnemonic(op) ^ "i" ^ spc() ^ reg_name(rd) ^ sep() ^ hex_bits_5(rs1) ^ sep() ^ csr_name_map(csr) + <-> csr_mnemonic(op) ^ "i" ^ spc() ^ reg_name(rd) ^ sep() ^ hex_bits_5(rs1) ^ sep() ^ hex_bits_12(csr) mapping clause assembly = CSR(csr, rs1, rd, false, op) - <-> csr_mnemonic(op) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ csr_name_map(csr) + <-> csr_mnemonic(op) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ hex_bits_12(csr) diff --git a/model/riscv_mem.sail b/model/riscv_mem.sail index 25065ab..b3fa37d 100644 --- a/model/riscv_mem.sail +++ b/model/riscv_mem.sail @@ -80,7 +80,8 @@ function rvfi_read (addr, width, result) = { MemValue(v) => if width <= 8 then { rvfi_exec->rvfi_mem_rdata() = sail_zero_extend(v,64); rvfi_exec->rvfi_mem_rmask() = rvfi_encode_width_mask(width) } - else (), + else { rvfi_exec->rvfi_mem_rdata() = v[63..0]; + rvfi_exec->rvfi_mem_rmask() = 0xFF}, MemException(_) => () }; } @@ -91,38 +92,28 @@ $endif /* NOTE: The rreg effect is due to MMIO. */ $ifdef RVFI_DII -val mem_read : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), xlenbits, atom('n), bool, bool, bool) -> MemoryOpResult(bits(8 * 'n)) effect {wreg, rmem, rmemt, rreg, escape} -val mem_read_meta : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), xlenbits, atom('n), bool, bool, bool) -> MemoryOpResult((bits(8 * 'n), mem_meta)) effect {wreg, rmem, rmemt, rreg, escape} +val mem_read : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), xlenbits, atom('n), bool, bool, bool) -> MemoryOpResult(bits(8 * 'n)) effect {wreg, rmem, rmemt, rreg, escape} +val mem_read_meta : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), xlenbits, atom('n), bool, bool, bool, bool) -> MemoryOpResult((bits(8 * 'n), mem_meta)) effect {wreg, rmem, rmemt, rreg, escape} $else -val mem_read : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), xlenbits, atom('n), bool, bool, bool) -> MemoryOpResult(bits(8 * 'n)) effect {rmem, rmemt, rreg, escape} -val mem_read_meta : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), xlenbits, atom('n), bool, bool, bool) -> MemoryOpResult((bits(8 * 'n), mem_meta)) effect {rmem, rmemt, rreg, escape} +val mem_read : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), xlenbits, atom('n), bool, bool, bool) -> MemoryOpResult(bits(8 * 'n)) effect {rmem, rmemt, rreg, escape} +val mem_read_meta : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), xlenbits, atom('n), bool, bool, bool, bool) -> MemoryOpResult((bits(8 * 'n), mem_meta)) effect {rmem, rmemt, rreg, escape} $endif -function mem_read (typ, paddr, width, aq, rl, res) = { - let result : MemoryOpResult(bits(8 * 'n)) = - if (aq | res) & (~ (is_aligned_addr(paddr, width))) - then MemException(E_Load_Addr_Align()) - else match (aq, rl, res) { - (false, true, false) => throw(Error_not_implemented("load.rl")), - (false, true, true) => throw(Error_not_implemented("lr.rl")), - (_, _, _) => MemoryOpResult_drop_meta(pmp_mem_read(typ, paddr, width, aq, rl, res, false)) - }; - rvfi_read(paddr, width, result); - result +function mem_read_meta (typ, paddr, width, aq, rl, res, meta) = { + let result : MemoryOpResult((bits(8 * 'n), mem_meta)) = + if (aq | res) & (~ (is_aligned_addr(paddr, width))) + then MemException(E_Load_Addr_Align()) + else match (aq, rl, res) { + (false, true, false) => throw(Error_not_implemented("load.rl")), + (false, true, true) => throw(Error_not_implemented("lr.rl")), + (_, _, _) => pmp_mem_read(typ, paddr, width, aq, rl, res, meta) + }; + rvfi_read(paddr, width, MemoryOpResult_drop_meta(result)); + result } -function mem_read_meta (typ, addr, width, aq, rl, res) = { - let result : MemoryOpResult((bits(8 * 'n), mem_meta)) = - if (aq | res) & (~ (is_aligned_addr(addr, width))) - then MemException(E_Load_Addr_Align()) - else match (aq, rl, res) { - (false, true, false) => throw(Error_not_implemented("load.rl")), - (false, true, true) => throw(Error_not_implemented("lr.rl")), - (_, _, _) => pmp_mem_read(typ, addr, width, aq, rl, res, true) - }; - rvfi_read(addr, width, MemoryOpResult_drop_meta(result)); - result -} +function mem_read (typ, paddr, width, aq, rl, res) = + MemoryOpResult_drop_meta(mem_read_meta(typ, paddr, width, aq, rl, res, false)) val mem_write_ea : forall 'n, 0 < 'n <= max_mem_access . (xlenbits, atom('n), bool, bool, bool) -> MemoryOpResult(unit) effect {eamem, escape} @@ -148,6 +139,9 @@ function rvfi_write (addr, width, value) = { if width <= 8 then { rvfi_exec->rvfi_mem_wdata() = sail_zero_extend(value,64); rvfi_exec->rvfi_mem_wmask() = rvfi_encode_width_mask(width); + } else { + rvfi_exec->rvfi_mem_wdata() = value[63..0]; + rvfi_exec->rvfi_mem_wmask() = 0xFF; } } $else diff --git a/model/riscv_types.sail b/model/riscv_types.sail index cacf0db..987743a 100644 --- a/model/riscv_types.sail +++ b/model/riscv_types.sail @@ -108,8 +108,6 @@ enum word_width = {BYTE, HALF, WORD, DOUBLE} /* architectural interrupt definitions */ -type exc_code = bits(8) - enum InterruptType = { I_U_Software, I_S_Software, @@ -181,7 +179,7 @@ function exceptionType_to_bits(e) = E_SAMO_Page_Fault() => 0x0f, /* extensions */ - E_Extension(e) => 0x18 /* First code for a custom extension */ + E_Extension(e) => ext_exc_type_to_bits(e) } val num_of_ExceptionType : ExceptionType -> {'n, (0 <= 'n < xlen). int('n)} @@ -205,7 +203,7 @@ function num_of_ExceptionType(e) = E_SAMO_Page_Fault() => 15, /* extensions */ - E_Extension(e) => 24 /* First code for a custom extension */ + E_Extension(e) => num_of_ext_exc_type(e) } @@ -230,7 +228,7 @@ function exceptionType_to_str(e) = E_SAMO_Page_Fault() => "store/amo-page-fault", /* extensions */ - E_Extension(e) => "extension-exception" + E_Extension(e) => ext_exc_type_to_str(e) } overload to_str = {exceptionType_to_str} diff --git a/model/riscv_types_common.sail b/model/riscv_types_common.sail new file mode 100644 index 0000000..9db34a0 --- /dev/null +++ b/model/riscv_types_common.sail @@ -0,0 +1 @@ +type exc_code = bits(8) diff --git a/model/riscv_types_ext.sail b/model/riscv_types_ext.sail index 5a05c39..6562981 100644 --- a/model/riscv_types_ext.sail +++ b/model/riscv_types_ext.sail @@ -20,3 +20,15 @@ type ext_exc_type = unit /* No exception extensions */ /* Default translation of PTW errors into exception annotations */ function ext_translate_exception(e : ext_ptw_error) -> ext_exc_type = e + +/* Default conversion of extension exceptions to bits */ +val ext_exc_type_to_bits : ext_exc_type -> exc_code +function ext_exc_type_to_bits(e) = 0x18 /* First code for a custom extension */ + +/* Default conversion of extension exceptions to integers */ +val num_of_ext_exc_type : ext_exc_type -> {'n, (0 <= 'n < xlen). int('n)} +function num_of_ext_exc_type(e) = 24 /* First code for a custom extension */ + +/* Default conversion of extension exceptions to strings */ +val ext_exc_type_to_str : ext_exc_type -> string +function ext_exc_type_to_str(e) = "extension-exception" |