diff options
-rw-r--r-- | Makefile | 2 | ||||
-rw-r--r-- | model/prelude_mem.sail | 24 | ||||
-rw-r--r-- | model/riscv_duopod.sail | 2 | ||||
-rw-r--r-- | model/riscv_insts_base.sail | 64 | ||||
-rw-r--r-- | model/riscv_insts_cext.sail | 64 | ||||
-rw-r--r-- | model/riscv_insts_mext.sail | 34 | ||||
-rw-r--r-- | model/riscv_jalr_rmem.sail | 2 | ||||
-rw-r--r-- | model/riscv_jalr_seq.sail | 2 | ||||
-rw-r--r-- | model/riscv_platform.sail | 10 | ||||
-rw-r--r-- | model/riscv_sys_regs.sail | 8 | ||||
-rw-r--r-- | model/riscv_types.sail | 6 | ||||
-rw-r--r-- | model/riscv_vmem.sail | 6 | ||||
-rw-r--r-- | model/riscv_xlen.sail | 4 |
13 files changed, 114 insertions, 114 deletions
@@ -10,7 +10,7 @@ SAIL_SYS_SRCS = riscv_csr_map.sail riscv_sys_regs.sail riscv_next_regs.sail risc # non-instruction sources PRELUDE = prelude.sail prelude_mapping.sail riscv_xlen.sail prelude_mem.sail SAIL_OTHER_SRCS = $(PRELUDE) riscv_types.sail $(SAIL_SYS_SRCS) riscv_platform.sail riscv_mem.sail riscv_vmem.sail -SAIL_OTHER_RVFI_SRCS = $(PRELUDE) rvfi_dii.sail riscv_xlen.sail riscv_types.sail $(SAIL_SYS_SRCS) riscv_platform.sail riscv_mem.sail riscv_vmem.sail +SAIL_OTHER_RVFI_SRCS = $(PRELUDE) rvfi_dii.sail riscv_types.sail $(SAIL_SYS_SRCS) riscv_platform.sail riscv_mem.sail riscv_vmem.sail PRELUDE_SRCS = $(addprefix model/,$(PRELUDE)) SAIL_SRCS = $(addprefix model/,$(SAIL_OTHER_SRCS) $(SAIL_SEQ_INST_SRCS) riscv_step.sail riscv_analysis.sail) diff --git a/model/prelude_mem.sail b/model/prelude_mem.sail index 532d0fd..8593db1 100644 --- a/model/prelude_mem.sail +++ b/model/prelude_mem.sail @@ -23,12 +23,12 @@ val __WriteRAM_conditional_strong_release = {lem: "MEMw_conditional_strong_relea val __RISCV_write : forall 'n. (xlenbits, atom('n), bits(8 * 'n), bool, bool, bool) -> bool effect {wmv} function __RISCV_write (addr, width, data, aq, rl, con) = match (aq, rl, con) { - (false, false, false) => __WriteRAM(xlen_val, width, EXTZ(0x0), addr, data), - (false, true, false) => __WriteRAM_release(xlen_val, width, EXTZ(0x0), addr, data), - (false, false, true) => __WriteRAM_conditional(xlen_val, width, EXTZ(0x0), addr, data), - (false, true, true) => __WriteRAM_conditional_release(xlen_val, width, EXTZ(0x0), addr, data), - (true, true, false) => __WriteRAM_strong_release(xlen_val, width, EXTZ(0x0), addr, data), - (true, true, true) => __WriteRAM_conditional_strong_release(xlen_val, width, EXTZ(0x0), addr, data), + (false, false, false) => __WriteRAM(xlen, width, EXTZ(0x0), addr, data), + (false, true, false) => __WriteRAM_release(xlen, width, EXTZ(0x0), addr, data), + (false, false, true) => __WriteRAM_conditional(xlen, width, EXTZ(0x0), addr, data), + (false, true, true) => __WriteRAM_conditional_release(xlen, width, EXTZ(0x0), addr, data), + (true, true, false) => __WriteRAM_strong_release(xlen, width, EXTZ(0x0), addr, data), + (true, true, true) => __WriteRAM_conditional_strong_release(xlen, width, EXTZ(0x0), addr, data), (true, false, false) => false, (true, false, true) => false } @@ -57,12 +57,12 @@ val __ReadRAM_reserved_strong_acquire = { lem: "MEMr_reserved_strong_acquire", _ val __RISCV_read : forall 'n, 'n >= 0. (xlenbits, atom('n), bool, bool, bool) -> option(bits(8 * 'n)) effect {rmem} function __RISCV_read (addr, width, aq, rl, res) = match (aq, rl, res) { - (false, false, false) => Some(__ReadRAM(xlen_val, width, EXTZ(0x0), addr)), - (true, false, false) => Some(__ReadRAM_acquire(xlen_val, width, EXTZ(0x0), addr)), - (true, true, false) => Some(__ReadRAM_strong_acquire(xlen_val, width, EXTZ(0x0), addr)), - (false, false, true) => Some(__ReadRAM_reserved(xlen_val, width, EXTZ(0x0), addr)), - (true, false, true) => Some(__ReadRAM_reserved_acquire(xlen_val, width, EXTZ(0x0), addr)), - (true, true, true) => Some(__ReadRAM_reserved_strong_acquire(xlen_val, width, EXTZ(0x0), addr)), + (false, false, false) => Some(__ReadRAM(xlen, width, EXTZ(0x0), addr)), + (true, false, false) => Some(__ReadRAM_acquire(xlen, width, EXTZ(0x0), addr)), + (true, true, false) => Some(__ReadRAM_strong_acquire(xlen, width, EXTZ(0x0), addr)), + (false, false, true) => Some(__ReadRAM_reserved(xlen, width, EXTZ(0x0), addr)), + (true, false, true) => Some(__ReadRAM_reserved_acquire(xlen, width, EXTZ(0x0), addr)), + (true, true, true) => Some(__ReadRAM_reserved_strong_acquire(xlen, width, EXTZ(0x0), addr)), (false, true, false) => None(), (false, true, true) => None() } diff --git a/model/riscv_duopod.sail b/model/riscv_duopod.sail index c68a5a5..99dbbba 100644 --- a/model/riscv_duopod.sail +++ b/model/riscv_duopod.sail @@ -73,7 +73,7 @@ function clause decode imm : bits(12) @ rs1 : regbits @ 0b011 @ rd : regbits @ 0 function clause execute(LOAD(imm, rs1, rd)) = let addr : xlenbits = X(rs1) + EXTS(imm) in - let result : xlenbits = MEMr(addr, xlen_val_bytes) in + let result : xlenbits = MEMr(addr, xlen_bytes) in X(rd) = result /* ****************************************************************** */ diff --git a/model/riscv_insts_base.sail b/model/riscv_insts_base.sail index f54e078..bfd6551 100644 --- a/model/riscv_insts_base.sail +++ b/model/riscv_insts_base.sail @@ -373,9 +373,9 @@ mapping clause assembly = STORE(imm, rs1, rd, size, aq, rl) union clause ast = ADDIW : (bits(12), regbits, regbits) mapping clause encdec = ADDIW(imm, rs1, rd) - if xlen_val == 64 + if xlen == 64 <-> imm @ rs1 @ 0b000 @ rd @ 0b0011011 - if xlen_val == 64 + if xlen == 64 function clause execute (ADDIW(imm, rs1, rd)) = { let result : xlenbits = EXTS(imm) + X(rs1); @@ -384,25 +384,25 @@ function clause execute (ADDIW(imm, rs1, rd)) = { } mapping clause assembly = ADDIW(imm, rs1, rd) - if xlen_val == 64 + if xlen == 64 <-> "addiw" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ hex_bits_12(imm) - if xlen_val == 64 + if xlen == 64 /* ****************************************************************** */ union clause ast = SHIFTW : (bits(5), regbits, regbits, sop) mapping clause encdec = SHIFTW(shamt, rs1, rd, RISCV_SLLI) - if xlen_val == 64 + if xlen == 64 <-> 0b0000000 @ shamt @ rs1 @ 0b001 @ rd @ 0b0011011 - if xlen_val == 64 + if xlen == 64 mapping clause encdec = SHIFTW(shamt, rs1, rd, RISCV_SRLI) - if xlen_val == 64 + if xlen == 64 <-> 0b0000000 @ shamt @ rs1 @ 0b101 @ rd @ 0b0011011 - if xlen_val == 64 + if xlen == 64 mapping clause encdec = SHIFTW(shamt, rs1, rd, RISCV_SRAI) - if xlen_val == 64 + if xlen == 64 <-> 0b0100000 @ shamt @ rs1 @ 0b101 @ rd @ 0b0011011 - if xlen_val == 64 + if xlen == 64 function clause execute (SHIFTW(shamt, rs1, rd, op)) = { let rs1_val = (X(rs1))[31..0]; @@ -422,33 +422,33 @@ mapping shiftw_mnemonic : sop <-> string = { } mapping clause assembly = SHIFTW(shamt, rs1, rd, op) - if xlen_val == 64 + if xlen == 64 <-> shiftw_mnemonic(op) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ hex_bits_5(shamt) - if xlen_val == 64 + if xlen == 64 /* ****************************************************************** */ union clause ast = RTYPEW : (regbits, regbits, regbits, ropw) mapping clause encdec = RTYPEW(rs2, rs1, rd, RISCV_ADDW) - if xlen_val == 64 + if xlen == 64 <-> 0b0000000 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0111011 - if xlen_val == 64 + if xlen == 64 mapping clause encdec = RTYPEW(rs2, rs1, rd, RISCV_SUBW) - if xlen_val == 64 + if xlen == 64 <-> 0b0100000 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0111011 - if xlen_val == 64 + if xlen == 64 mapping clause encdec = RTYPEW(rs2, rs1, rd, RISCV_SLLW) - if xlen_val == 64 + if xlen == 64 <-> 0b0000000 @ rs2 @ rs1 @ 0b001 @ rd @ 0b0111011 - if xlen_val == 64 + if xlen == 64 mapping clause encdec = RTYPEW(rs2, rs1, rd, RISCV_SRLW) - if xlen_val == 64 + if xlen == 64 <-> 0b0000000 @ rs2 @ rs1 @ 0b101 @ rd @ 0b0111011 - if xlen_val == 64 + if xlen == 64 mapping clause encdec = RTYPEW(rs2, rs1, rd, RISCV_SRAW) - if xlen_val == 64 + if xlen == 64 <-> 0b0100000 @ rs2 @ rs1 @ 0b101 @ rd @ 0b0111011 - if xlen_val == 64 + if xlen == 64 function clause execute (RTYPEW(rs2, rs1, rd, op)) = { let rs1_val = (X(rs1))[31..0]; @@ -473,25 +473,25 @@ mapping rtypew_mnemonic : ropw <-> string = { } mapping clause assembly = RTYPEW(rs2, rs1, rd, op) - if xlen_val == 64 + if xlen == 64 <-> rtypew_mnemonic(op) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2) - if xlen_val == 64 + if xlen == 64 /* ****************************************************************** */ union clause ast = SHIFTIWOP : (bits(5), regbits, regbits, sopw) mapping clause encdec = SHIFTIWOP(shamt, rs1, rd, RISCV_SLLIW) - if xlen_val == 64 + if xlen == 64 <-> 0b0000000 @ shamt @ rs1 @ 0b001 @ rd @ 0b0011011 - if xlen_val == 64 + if xlen == 64 mapping clause encdec = SHIFTIWOP(shamt, rs1, rd, RISCV_SRLIW) - if xlen_val == 64 + if xlen == 64 <-> 0b0000000 @ shamt @ rs1 @ 0b101 @ rd @ 0b0011011 - if xlen_val == 64 + if xlen == 64 mapping clause encdec = SHIFTIWOP(shamt, rs1, rd, RISCV_SRAIW) - if xlen_val == 64 + if xlen == 64 <-> 0b0100000 @ shamt @ rs1 @ 0b101 @ rd @ 0b0011011 - if xlen_val == 64 + if xlen == 64 function clause execute (SHIFTIWOP(shamt, rs1, rd, op)) = { let rs1_val = X(rs1); @@ -511,9 +511,9 @@ mapping shiftiwop_mnemonic : sopw <-> string = { } mapping clause assembly = SHIFTIWOP(shamt, rs1, rd, op) - if xlen_val == 64 + if xlen == 64 <-> shiftiwop_mnemonic(op) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ hex_bits_5(shamt) - if xlen_val == 64 + if xlen == 64 /* ****************************************************************** */ union clause ast = FENCE : (bits(4), bits(4)) diff --git a/model/riscv_insts_cext.sail b/model/riscv_insts_cext.sail index d2b0695..3423f8e 100644 --- a/model/riscv_insts_cext.sail +++ b/model/riscv_insts_cext.sail @@ -56,9 +56,9 @@ mapping clause assembly = C_LW(uimm, rsc, rdc) union clause ast = C_LD : (bits(5), cregbits, cregbits) mapping clause encdec_compressed = C_LD(ui76 @ ui53, rs1, rd) - if xlen_val == 64 + if xlen == 64 <-> 0b011 @ ui53 : bits(3) @ rs1 : cregbits @ ui76 : bits(2) @ rd : cregbits @ 0b00 - if xlen_val == 64 + if xlen == 64 function clause execute (C_LD(uimm, rsc, rdc)) = { let imm : bits(12) = EXTZ(uimm @ 0b000); @@ -68,9 +68,9 @@ function clause execute (C_LD(uimm, rsc, rdc)) = { } mapping clause assembly = C_LD(uimm, rsc, rdc) - if xlen_val == 64 + if xlen == 64 <-> "c.ld" ^ spc() ^ creg_name(rdc) ^ sep() ^ creg_name(rsc) ^ sep() ^ hex_bits_8(uimm @ 0b000) - if xlen_val == 64 + if xlen == 64 /* ****************************************************************** */ union clause ast = C_SW : (bits(5), cregbits, cregbits) @@ -92,9 +92,9 @@ mapping clause assembly = C_SW(uimm, rsc1, rsc2) union clause ast = C_SD : (bits(5), cregbits, cregbits) mapping clause encdec_compressed = C_SD(ui76 @ ui53, rs1, rs2) - if xlen_val == 64 + if xlen == 64 <-> 0b111 @ ui53 : bits(3) @ rs1 : bits(3) @ ui76 : bits(2) @ rs2 : bits(3) @ 0b00 - if xlen_val == 64 + if xlen == 64 function clause execute (C_SD(uimm, rsc1, rsc2)) = { let imm : bits(12) = EXTZ(uimm @ 0b000); @@ -104,9 +104,9 @@ function clause execute (C_SD(uimm, rsc1, rsc2)) = { } mapping clause assembly = C_SD(uimm, rsc1, rsc2) - if xlen_val == 64 + if xlen == 64 <-> "c.sd" ^ spc() ^ creg_name(rsc1) ^ sep() ^ creg_name(rsc2) ^ sep() ^ hex_bits_8(uimm @ 0b000) - if xlen_val == 64 + if xlen == 64 /* ****************************************************************** */ union clause ast = C_ADDI : (bits(6), regbits) @@ -130,25 +130,25 @@ mapping clause assembly = C_ADDI(nzi, rsd) union clause ast = C_JAL : (bits(11)) mapping clause encdec_compressed = C_JAL(i11 @ i10 @ i98 @ i7 @ i6 @ i5 @ i4 @ i31) - if xlen_val == 32 + if xlen == 32 <-> 0b001 @ i11 : bits(1) @ i4 : bits(1) @ i98 : bits(2) @ i10 : bits(1) @ i6 : bits(1) @ i7 : bits(1) @ i31 : bits(3) @ i5 : bits(1) @ 0b01 - if xlen_val == 32 + if xlen == 32 function clause execute (C_JAL(imm)) = execute(RISCV_JAL(EXTS(imm @ 0b0), ra)) mapping clause assembly = C_JAL(imm) - if xlen_val == 32 + if xlen == 32 <-> "c.jal" ^ spc() ^ hex_bits_12(imm @ 0b0) - if xlen_val == 32 + if xlen == 32 /* ****************************************************************** */ union clause ast = C_ADDIW : (bits(6), regbits) mapping clause encdec_compressed = C_ADDIW(imm5 @ imm40, rsd) - if rsd != zreg & xlen_val == 64 + if rsd != zreg & xlen == 64 <-> 0b001 @ imm5 : bits(1) @ rsd : regbits @ imm40 : bits(5) @ 0b01 - if rsd != zreg & xlen_val == 64 + if rsd != zreg & xlen == 64 function clause execute (C_ADDIW(imm, rsd)) = { let imm : bits(32) = EXTS(imm); @@ -159,9 +159,9 @@ function clause execute (C_ADDIW(imm, rsd)) = { } mapping clause assembly = C_ADDIW(imm, rsd) - if xlen_val == 64 + if xlen == 64 <-> "c.addiw" ^ spc() ^ reg_name(rsd) ^ sep() ^ hex_bits_6(imm) - if xlen_val == 64 + if xlen == 64 /* ****************************************************************** */ union clause ast = C_LI : (bits(6), regbits) @@ -332,9 +332,9 @@ union clause ast = C_SUBW : (cregbits, cregbits) /* TODO: invalid on RV32 */ mapping clause encdec_compressed = C_SUBW(rsd, rs2) - if xlen_val == 64 + if xlen == 64 <-> 0b100 @ 0b1 @ 0b11 @ rsd : cregbits @ 0b00 @ rs2 : cregbits @ 0b01 - if xlen_val == 64 + if xlen == 64 function clause execute (C_SUBW(rsd, rs2)) = { let rsd = creg2reg_bits(rsd); @@ -343,18 +343,18 @@ function clause execute (C_SUBW(rsd, rs2)) = { } mapping clause assembly = C_SUBW(rsd, rs2) - if xlen_val == 64 + if xlen == 64 <-> "c.subw" ^ spc() ^ creg_name(rsd) ^ sep() ^ creg_name(rs2) - if xlen_val == 64 + if xlen == 64 /* ****************************************************************** */ union clause ast = C_ADDW : (cregbits, cregbits) /* TODO: invalid on RV32 */ mapping clause encdec_compressed = C_ADDW(rsd, rs2) - if xlen_val == 64 + if xlen == 64 <-> 0b100 @ 0b1 @ 0b11 @ rsd : cregbits @ 0b01 @ rs2 : cregbits @ 0b01 - if xlen_val == 64 + if xlen == 64 function clause execute (C_ADDW(rsd, rs2)) = { let rsd = creg2reg_bits(rsd); @@ -363,9 +363,9 @@ function clause execute (C_ADDW(rsd, rs2)) = { } mapping clause assembly = C_ADDW(rsd, rs2) - if xlen_val == 64 + if xlen == 64 <-> "c.addw" ^ spc() ^ creg_name(rsd) ^ sep() ^ creg_name(rs2) - if xlen_val == 64 + if xlen == 64 /* ****************************************************************** */ union clause ast = C_J : (bits(11)) @@ -436,9 +436,9 @@ mapping clause assembly = C_LWSP(uimm, rd) union clause ast = C_LDSP : (bits(6), regbits) mapping clause encdec_compressed = C_LDSP(ui86 @ ui5 @ ui43, rd) - if rd != zreg & xlen_val == 64 + if rd != zreg & xlen == 64 <-> 0b011 @ ui5 : bits(1) @ rd : regbits @ ui43 : bits(2) @ ui86 : bits(3) @ 0b10 - if rd != zreg & xlen_val == 64 + if rd != zreg & xlen == 64 function clause execute (C_LDSP(uimm, rd)) = { let imm : bits(12) = EXTZ(uimm @ 0b000); @@ -446,9 +446,9 @@ function clause execute (C_LDSP(uimm, rd)) = { } mapping clause assembly = C_LDSP(uimm, rd) - if rd != zreg & xlen_val == 64 + if rd != zreg & xlen == 64 <-> "c.ldsp" ^ spc() ^ reg_name(rd) ^ sep() ^ hex_bits_6(uimm) - if rd != zreg & xlen_val == 64 + if rd != zreg & xlen == 64 /* ****************************************************************** */ union clause ast = C_SWSP : (bits(6), regbits) @@ -468,9 +468,9 @@ mapping clause assembly = C_SWSP(uimm, rd) union clause ast = C_SDSP : (bits(6), regbits) mapping clause encdec_compressed = C_SDSP(ui86 @ ui53, rs2) - if xlen_val == 64 + if xlen == 64 <-> 0b111 @ ui53 : bits(3) @ ui86 : bits(3) @ rs2 : regbits @ 0b10 - if xlen_val == 64 + if xlen == 64 function clause execute (C_SDSP(uimm, rs2)) = { let imm : bits(12) = EXTZ(uimm @ 0b000); @@ -478,9 +478,9 @@ function clause execute (C_SDSP(uimm, rs2)) = { } mapping clause assembly = C_SDSP(uimm, rs2) - if xlen_val == 64 + if xlen == 64 <-> "c.sdsp" ^ spc() ^ reg_name(rs2) ^ sep() ^ hex_bits_6(uimm) - if xlen_val == 64 + if xlen == 64 /* ****************************************************************** */ union clause ast = C_JR : (regbits) diff --git a/model/riscv_insts_mext.sail b/model/riscv_insts_mext.sail index c4ca7e5..371966f 100644 --- a/model/riscv_insts_mext.sail +++ b/model/riscv_insts_mext.sail @@ -22,10 +22,10 @@ function clause execute (MUL(rs2, rs1, rd, high, signed1, signed2)) = { let rs2_val = X(rs2); let rs1_int : int = if signed1 then signed(rs1_val) else unsigned(rs1_val); let rs2_int : int = if signed2 then signed(rs2_val) else unsigned(rs2_val); - let result_wide = to_bits(2 * xlen_val, rs1_int * rs2_int); + let result_wide = to_bits(2 * xlen, rs1_int * rs2_int); let result = if high - then result_wide[(2 * xlen_val - 1) .. xlen_val] - else result_wide[(xlen_val - 1) .. 0]; + then result_wide[(2 * xlen - 1) .. xlen] + else result_wide[(xlen - 1) .. 0]; X(rd) = result; true } else { @@ -59,7 +59,7 @@ function clause execute (DIV(rs2, rs1, rd, s)) = { let q : int = if rs2_int == 0 then -1 else quot_round_zero(rs1_int, rs2_int); /* check for signed overflow */ let q': int = if s & q > xlen_max_signed then xlen_min_signed else q; - X(rd) = to_bits(xlen_val, q'); + X(rd) = to_bits(xlen, q'); true } else { handle_illegal(); @@ -89,7 +89,7 @@ function clause execute (REM(rs2, rs1, rd, s)) = { let rs2_int : int = if s then signed(rs2_val) else unsigned(rs2_val); let r : int = if rs2_int == 0 then rs1_int else rem_round_zero(rs1_int, rs2_int); /* signed overflow case returns zero naturally as required due to -1 divisor */ - X(rd) = to_bits(xlen_val, r); + X(rd) = to_bits(xlen, r); true } else { handle_illegal(); @@ -104,9 +104,9 @@ mapping clause assembly = REM(rs2, rs1, rd, s) union clause ast = MULW : (regbits, regbits, regbits) mapping clause encdec = MULW(rs2, rs1, rd) - if xlen_val == 64 + if xlen == 64 <-> 0b0000001 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0111011 - if xlen_val == 64 + if xlen == 64 function clause execute (MULW(rs2, rs1, rd)) = { if haveMulDiv() then { @@ -126,17 +126,17 @@ function clause execute (MULW(rs2, rs1, rd)) = { } mapping clause assembly = MULW(rs2, rs1, rd) - if xlen_val == 64 + if xlen == 64 <-> "mulw" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2) - if xlen_val == 64 + if xlen == 64 /* ****************************************************************** */ union clause ast = DIVW : (regbits, regbits, regbits, bool) mapping clause encdec = DIVW(rs2, rs1, rd, s) - if xlen_val == 64 + if xlen == 64 <-> 0b0000001 @ rs2 @ rs1 @ 0b10 @ bool_not_bits(s) @ rd @ 0b0111011 - if xlen_val == 64 + if xlen == 64 function clause execute (DIVW(rs2, rs1, rd, s)) = { if haveMulDiv() then { @@ -156,17 +156,17 @@ function clause execute (DIVW(rs2, rs1, rd, s)) = { } mapping clause assembly = DIVW(rs2, rs1, rd, s) - if xlen_val == 64 + if xlen == 64 <-> "div" ^ maybe_not_u(s) ^ "w" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2) - if xlen_val == 64 + if xlen == 64 /* ****************************************************************** */ union clause ast = REMW : (regbits, regbits, regbits, bool) mapping clause encdec = REMW(rs2, rs1, rd, s) - if xlen_val == 64 + if xlen == 64 <-> 0b0000001 @ rs2 @ rs1 @ 0b11 @ bool_not_bits(s) @ rd @ 0b0111011 - if xlen_val == 64 + if xlen == 64 function clause execute (REMW(rs2, rs1, rd, s)) = { if haveMulDiv() then { @@ -185,6 +185,6 @@ function clause execute (REMW(rs2, rs1, rd, s)) = { } mapping clause assembly = REMW(rs2, rs1, rd, s) - if xlen_val == 64 + if xlen == 64 <-> "rem" ^ maybe_not_u(s) ^ "w" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2) - if xlen_val == 64 + if xlen == 64 diff --git a/model/riscv_jalr_rmem.sail b/model/riscv_jalr_rmem.sail index 3069582..333f385 100644 --- a/model/riscv_jalr_rmem.sail +++ b/model/riscv_jalr_rmem.sail @@ -5,6 +5,6 @@ function clause execute (RISCV_JALR(imm, rs1, rd)) = { /* write rd before anything else to prevent unintended strength */ X(rd) = nextPC; /* compatible with JALR, C.JR and C.JALR */ let newPC : xlenbits = X(rs1) + EXTS(imm); - nextPC = newPC[(xlen_val - 1) .. 1] @ 0b0; + nextPC = newPC[(xlen - 1) .. 1] @ 0b0; true } diff --git a/model/riscv_jalr_seq.sail b/model/riscv_jalr_seq.sail index d4982c6..3dcae61 100644 --- a/model/riscv_jalr_seq.sail +++ b/model/riscv_jalr_seq.sail @@ -7,7 +7,7 @@ function clause execute (RISCV_JALR(imm, rs1, rd)) = { some manner, but for now, we just keep a reordered definition to improve simulator performance. */ - let newPC : xlenbits = (X(rs1) + EXTS(imm))[(xlen_val) - 1 .. 1] @ 0b0; + let newPC : xlenbits = (X(rs1) + EXTS(imm))[(xlen - 1) .. 1] @ 0b0; if newPC[1] & (~ (haveRVC())) then { handle_mem_exception(newPC, E_Fetch_Addr_Align); false; diff --git a/model/riscv_platform.sail b/model/riscv_platform.sail index 25739fc..c43ab52 100644 --- a/model/riscv_platform.sail +++ b/model/riscv_platform.sail @@ -117,12 +117,12 @@ function clint_load(addr, width) = { else if addr == MTIMECMP_BASE & ('n == 8) then { print_platform("clint[" ^ BitStr(addr) ^ "] -> " ^ BitStr(mtimecmp)); - MemValue(zero_extend(mtimecmp, xlen_val)) /* FIXME: Redundant zero_extend currently required by Lem backend */ + MemValue(zero_extend(mtimecmp, xlen)) /* FIXME: Redundant zero_extend currently required by Lem backend */ } else if addr == MTIME_BASE & ('n == 8) then { print_platform("clint[" ^ BitStr(addr) ^ "] -> " ^ BitStr(mtime)); - MemValue(zero_extend(mtime, xlen_val)) + MemValue(zero_extend(mtime, xlen)) } else { print_platform("clint[" ^ BitStr(addr) ^ "] -> <not-mapped>"); @@ -150,7 +150,7 @@ function clint_store(addr, width, data) = { MemValue(true) } else if addr == MTIMECMP_BASE & 'n == 8 then { print_platform("clint[" ^ BitStr(addr) ^ "] <- " ^ BitStr(data) ^ " (mtimecmp)"); - mtimecmp = zero_extend(data, xlen_val); /* FIXME: Redundant zero_extend currently required by Lem backend */ + mtimecmp = zero_extend(data, xlen); /* FIXME: Redundant zero_extend currently required by Lem backend */ clint_dispatch(); MemValue(true) } else { @@ -194,7 +194,7 @@ function htif_load(addr, width) = { print_platform("htif[" ^ BitStr(addr) ^ "] -> " ^ BitStr(htif_tohost)); /* FIXME: For now, only allow the expected access widths. */ if width == 8 - then MemValue(zero_extend(htif_tohost, xlen_val)) /* FIXME: Redundant zero_extend currently required by Lem backend */ + then MemValue(zero_extend(htif_tohost, xlen)) /* FIXME: Redundant zero_extend currently required by Lem backend */ else MemException(E_Load_Access_Fault) } @@ -213,7 +213,7 @@ function htif_store(addr, width, data) = { if cmd.payload()[0] == 0b1 then { htif_done = true; - htif_exit_code = (zero_extend(cmd.payload(), xlen_val) >> 0b01) : xlenbits + htif_exit_code = (zero_extend(cmd.payload(), xlen) >> 0b01) : xlenbits } else () }, diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail index 03f5520..46a2f77 100644 --- a/model/riscv_sys_regs.sail +++ b/model/riscv_sys_regs.sail @@ -120,13 +120,13 @@ bitfield Mstatus : xlenbits = { register mstatus : Mstatus function get_mstatus_SXL(m : Mstatus) -> arch_xlen = { - if sizeof(xlen) == 32 + if xlen == 32 then arch_to_bits(RV32) else m.bits()[35 .. 34] } function set_mstatus_SXL(m : Mstatus, a : arch_xlen) -> Mstatus = { - if sizeof(xlen) == 32 + if xlen == 32 then m else { let m = vector_update_subrange(m.bits(), 35, 34, a); @@ -135,13 +135,13 @@ function set_mstatus_SXL(m : Mstatus, a : arch_xlen) -> Mstatus = { } function get_mstatus_UXL(m : Mstatus) -> arch_xlen = { - if sizeof(xlen) == 32 + if xlen == 32 then arch_to_bits(RV32) else m.bits()[33 .. 32] } function set_mstatus_UXL(m : Mstatus, a : arch_xlen) -> Mstatus = { - if sizeof(xlen) == 32 + if xlen == 32 then m else { let m = vector_update_subrange(mstatus.bits(), 33, 32, a); diff --git a/model/riscv_types.sail b/model/riscv_types.sail index 94ca69b..e081e68 100644 --- a/model/riscv_types.sail +++ b/model/riscv_types.sail @@ -1,8 +1,8 @@ /* Basic type and function definitions used pervasively in the model. */ -let xlen_max_unsigned = 2 ^ xlen_val - 1 -let xlen_max_signed = 2 ^ (xlen_val - 1) - 1 -let xlen_min_signed = 0 - 2 ^ (xlen_val - 1) +let xlen_max_unsigned = 2 ^ xlen - 1 +let xlen_max_signed = 2 ^ (xlen - 1) - 1 +let xlen_min_signed = 0 - 2 ^ (xlen - 1) type half = bits(16) type word = bits(32) diff --git a/model/riscv_vmem.sail b/model/riscv_vmem.sail index eb0e957..8a61f1c 100644 --- a/model/riscv_vmem.sail +++ b/model/riscv_vmem.sail @@ -146,7 +146,7 @@ function walk39(vaddr, ac, priv, mxr, do_sum, ptb, level, global) -> PTW_Result PTE39_LOG_SIZE); let pte_addr = ptb + pt_ofs; /* FIXME: we assume here that walks only access physical-memory-backed addresses, and not MMIO regions. */ - match (phys_mem_read(Data, EXTZ(pte_addr), xlen_val_bytes, false, false, false)) { + match (phys_mem_read(Data, EXTZ(pte_addr), xlen_bytes, false, false, false)) { MemException(_) => { /* print("walk39(vaddr=" ^ BitStr(vaddr) ^ " level=" ^ string_of_int(level) ^ " pt_base=" ^ BitStr(ptb) @@ -313,7 +313,7 @@ function translate39(vAddr, ac, priv, mxr, do_sum, level) = { n_ent.pte = update_BITS(ent.pte, pbits.bits()); writeTLB39(idx, n_ent); /* update page table */ - match checked_mem_write(EXTZ(ent.pteAddr), xlen_val_bytes, ent.pte.bits(), false, false, false) { + match checked_mem_write(EXTZ(ent.pteAddr), xlen_bytes, ent.pte.bits(), false, false, false) { MemValue(_) => (), MemException(e) => internal_error("invalid physical address in TLB") }; @@ -339,7 +339,7 @@ function translate39(vAddr, ac, priv, mxr, do_sum, level) = { TR39_Failure(PTW_PTE_Update) } else { w_pte : SV39_PTE = update_BITS(pte, pbits.bits()); - match checked_mem_write(EXTZ(pteAddr), xlen_val_bytes, w_pte.bits(), false, false, false) { + match checked_mem_write(EXTZ(pteAddr), xlen_bytes, w_pte.bits(), false, false, false) { MemValue(_) => { addToTLB39(asid, vAddr, pAddr, w_pte, pteAddr, level, global); TR39_Address(pAddr) diff --git a/model/riscv_xlen.sail b/model/riscv_xlen.sail index 801aca8..d4b1b53 100644 --- a/model/riscv_xlen.sail +++ b/model/riscv_xlen.sail @@ -5,5 +5,5 @@ type xlen : Int = 64 type xlenbits = bits(xlen) // value-level definitions -let xlen_val = 64 -let xlen_val_bytes = 8 // byte-width of xlen bits +let xlen : int(xlen) = 64 +let xlen_bytes = 8 // byte-width of xlen bits |