diff options
author | Prashanth Mundkur <prashanth.mundkur@gmail.com> | 2019-02-19 15:49:56 -0800 |
---|---|---|
committer | Prashanth Mundkur <prashanth.mundkur@gmail.com> | 2019-02-19 15:49:56 -0800 |
commit | 6a4eb9211bab5070dc55cea9046e1ffc4e20eafc (patch) | |
tree | 2c9f667f8852a89f66896bbb62b4c09deceea034 /model | |
parent | a238acdcd83f2db3c6d549775f16ac8b4ad2291e (diff) | |
download | sail-riscv-6a4eb9211bab5070dc55cea9046e1ffc4e20eafc.zip sail-riscv-6a4eb9211bab5070dc55cea9046e1ffc4e20eafc.tar.gz sail-riscv-6a4eb9211bab5070dc55cea9046e1ffc4e20eafc.tar.bz2 |
Use sizeof xlen instead of the value definitions of xlen.
Diffstat (limited to 'model')
-rw-r--r-- | model/main.sail | 2 | ||||
-rw-r--r-- | model/prelude_mem.sail | 24 | ||||
-rw-r--r-- | model/riscv_insts_aext.sail | 20 | ||||
-rw-r--r-- | model/riscv_insts_base.sail | 78 | ||||
-rw-r--r-- | model/riscv_insts_cext.sail | 64 | ||||
-rw-r--r-- | model/riscv_insts_mext.sail | 34 | ||||
-rw-r--r-- | model/riscv_insts_zicsr.sail | 18 | ||||
-rw-r--r-- | model/riscv_jalr_rmem.sail | 2 | ||||
-rw-r--r-- | model/riscv_jalr_seq.sail | 2 | ||||
-rw-r--r-- | model/riscv_sys_control.sail | 10 | ||||
-rw-r--r-- | model/riscv_sys_regs.sail | 10 | ||||
-rw-r--r-- | model/riscv_types.sail | 6 | ||||
-rw-r--r-- | model/riscv_xlen32.sail | 4 | ||||
-rw-r--r-- | model/riscv_xlen64.sail | 4 |
14 files changed, 135 insertions, 143 deletions
diff --git a/model/main.sail b/model/main.sail index 5a6dba1..c454c46 100644 --- a/model/main.sail +++ b/model/main.sail @@ -13,7 +13,7 @@ val main : unit -> unit effect {barr, eamem, escape, exmem, rmem, rreg, wmv, wre function main () = { // PC = __GetSlice_int(64, elf_entry(), 0); - PC = zero_extend(0x1000, xlen); + PC = zero_extend(0x1000, sizeof(xlen)); print_bits("PC = ", PC); try { init_platform(); diff --git a/model/prelude_mem.sail b/model/prelude_mem.sail index 8593db1..8e483f8 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, 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), + (false, false, false) => __WriteRAM(sizeof(xlen), width, EXTZ(0x0), addr, data), + (false, true, false) => __WriteRAM_release(sizeof(xlen), width, EXTZ(0x0), addr, data), + (false, false, true) => __WriteRAM_conditional(sizeof(xlen), width, EXTZ(0x0), addr, data), + (false, true, true) => __WriteRAM_conditional_release(sizeof(xlen), width, EXTZ(0x0), addr, data), + (true, true, false) => __WriteRAM_strong_release(sizeof(xlen), width, EXTZ(0x0), addr, data), + (true, true, true) => __WriteRAM_conditional_strong_release(sizeof(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, 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, false, false) => Some(__ReadRAM(sizeof(xlen), width, EXTZ(0x0), addr)), + (true, false, false) => Some(__ReadRAM_acquire(sizeof(xlen), width, EXTZ(0x0), addr)), + (true, true, false) => Some(__ReadRAM_strong_acquire(sizeof(xlen), width, EXTZ(0x0), addr)), + (false, false, true) => Some(__ReadRAM_reserved(sizeof(xlen), width, EXTZ(0x0), addr)), + (true, false, true) => Some(__ReadRAM_reserved_acquire(sizeof(xlen), width, EXTZ(0x0), addr)), + (true, true, true) => Some(__ReadRAM_reserved_strong_acquire(sizeof(xlen), width, EXTZ(0x0), addr)), (false, true, false) => None(), (false, true, true) => None() } diff --git a/model/riscv_insts_aext.sail b/model/riscv_insts_aext.sail index 202dac2..c1ddebd 100644 --- a/model/riscv_insts_aext.sail +++ b/model/riscv_insts_aext.sail @@ -60,7 +60,7 @@ function clause execute(LOADRES(aq, rl, rs1, width, rd)) = { else match translateAddr(vaddr, Read, Data) { TR_Failure(e) => { handle_mem_exception(vaddr, e); false }, TR_Address(addr) => - match (width, xlen) { + match (width, sizeof(xlen)) { (WORD, _) => process_loadres(rd, vaddr, mem_read(addr, 4, aq, rl, true), false), (DOUBLE, 64) => process_loadres(rd, vaddr, mem_read(addr, 8, aq, rl, true), false), _ => internal_error("LOADRES expected WORD or DOUBLE") @@ -114,7 +114,7 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = { match translateAddr(vaddr, Write, Data) { TR_Failure(e) => { handle_mem_exception(vaddr, e); false }, TR_Address(addr) => { - let eares : MemoryOpResult(unit) = match (width, xlen) { + let eares : MemoryOpResult(unit) = match (width, sizeof(xlen)) { (WORD, _) => mem_write_ea(addr, 4, aq, rl, true), (DOUBLE, 64) => mem_write_ea(addr, 8, aq, rl, true), _ => internal_error("STORECON expected word or double") @@ -123,7 +123,7 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = { MemException(e) => { handle_mem_exception(addr, e); false }, MemValue(_) => { rs2_val = X(rs2); - let res : MemoryOpResult(bool) = match (width, xlen) { + let res : MemoryOpResult(bool) = match (width, sizeof(xlen)) { (WORD, _) => mem_write_value(addr, 4, rs2_val[31..0], aq, rl, true), (DOUBLE, 64) => mem_write_value(addr, 8, rs2_val, aq, rl, true), _ => internal_error("STORECON expected word or double") @@ -175,7 +175,7 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = { match translateAddr(vaddr, ReadWrite, Data) { TR_Failure(e) => { handle_mem_exception(vaddr, e); false }, TR_Address(addr) => { - let eares : MemoryOpResult(unit) = match (width, xlen) { + 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") @@ -184,7 +184,7 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = { match (eares) { MemException(e) => { handle_mem_exception(addr, e); false }, MemValue(_) => { - let rval : MemoryOpResult(xlenbits) = match (width, xlen) { + let rval : MemoryOpResult(xlenbits) = match (width, sizeof(xlen)) { (WORD, _) => extend_value(false, mem_read(addr, 4, aq, aq & rl, true)), (DOUBLE, 64) => extend_value(false, mem_read(addr, 8, aq, aq & rl, true)), _ => internal_error ("AMO expected WORD or DOUBLE") @@ -203,13 +203,13 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = { /* These operations convert bitvectors to integer values using [un]signed, * and back using to_bits(). */ - AMOMIN => to_bits(xlen, min(signed(rs2_val), signed(loaded))), - AMOMAX => to_bits(xlen, max(signed(rs2_val), signed(loaded))), - AMOMINU => to_bits(xlen, min(unsigned(rs2_val), unsigned(loaded))), - AMOMAXU => to_bits(xlen, max(unsigned(rs2_val), unsigned(loaded))) + AMOMIN => to_bits(sizeof(xlen), min(signed(rs2_val), signed(loaded))), + AMOMAX => to_bits(sizeof(xlen), max(signed(rs2_val), signed(loaded))), + AMOMINU => to_bits(sizeof(xlen), min(unsigned(rs2_val), unsigned(loaded))), + AMOMAXU => to_bits(sizeof(xlen), max(unsigned(rs2_val), unsigned(loaded))) }; - let wval : MemoryOpResult(bool) = match (width, xlen) { + 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") diff --git a/model/riscv_insts_base.sail b/model/riscv_insts_base.sail index f570fb2..c612039 100644 --- a/model/riscv_insts_base.sail +++ b/model/riscv_insts_base.sail @@ -179,16 +179,16 @@ mapping encdec_sop : sop <-> bits(3) = { RISCV_SRAI <-> 0b101 } -mapping clause encdec = SHIFTIOP(shamt, rs1, rd, RISCV_SLLI) <-> 0b000000 @ shamt @ rs1 @ 0b001 @ rd @ 0b0010011 if xlen == 64 | shamt[5] == false -mapping clause encdec = SHIFTIOP(shamt, rs1, rd, RISCV_SRLI) <-> 0b000000 @ shamt @ rs1 @ 0b101 @ rd @ 0b0010011 if xlen == 64 | shamt[5] == false -mapping clause encdec = SHIFTIOP(shamt, rs1, rd, RISCV_SRAI) <-> 0b010000 @ shamt @ rs1 @ 0b101 @ rd @ 0b0010011 if xlen == 64 | shamt[5] == false +mapping clause encdec = SHIFTIOP(shamt, rs1, rd, RISCV_SLLI) <-> 0b000000 @ shamt @ rs1 @ 0b001 @ rd @ 0b0010011 if sizeof(xlen) == 64 | shamt[5] == false +mapping clause encdec = SHIFTIOP(shamt, rs1, rd, RISCV_SRLI) <-> 0b000000 @ shamt @ rs1 @ 0b101 @ rd @ 0b0010011 if sizeof(xlen) == 64 | shamt[5] == false +mapping clause encdec = SHIFTIOP(shamt, rs1, rd, RISCV_SRAI) <-> 0b010000 @ shamt @ rs1 @ 0b101 @ rd @ 0b0010011 if sizeof(xlen) == 64 | shamt[5] == false function clause execute (SHIFTIOP(shamt, rs1, rd, op)) = { let rs1_val = X(rs1); let result : xlenbits = match op { RISCV_SLLI => rs1_val << shamt, RISCV_SRLI => rs1_val >> shamt, - RISCV_SRAI => if xlen == 32 + RISCV_SRAI => if sizeof(xlen) == 32 /* the decoder guard should ensure that shamt[5] = 0 for RV32 */ then shift_right_arith32(rs1_val, shamt[4..0]) else shift_right_arith64(rs1_val, shamt) @@ -233,7 +233,7 @@ function clause execute (RTYPE(rs2, rs1, rd, op)) = { RISCV_SLL => rs1_val << (rs2_val[5..0]), RISCV_SRL => rs1_val >> (rs2_val[5..0]), RISCV_SUB => rs1_val - rs2_val, - RISCV_SRA => if xlen == 32 + RISCV_SRA => if sizeof(xlen) == 32 then shift_right_arith32(rs1_val, rs2_val[4..0]) else shift_right_arith64(rs1_val, rs2_val[5..0]) }; @@ -294,7 +294,7 @@ function clause execute(LOAD(imm, rs1, rd, is_unsigned, width, aq, rl)) = { else match translateAddr(vaddr, Read, Data) { TR_Failure(e) => { handle_mem_exception(vaddr, e); false }, TR_Address(addr) => - match (width, xlen) { + match (width, sizeof(xlen)) { (BYTE, _) => process_load(rd, vaddr, mem_read(addr, 1, aq, rl, false), is_unsigned), (HALF, _) => @@ -354,7 +354,7 @@ function clause execute (STORE(imm, rs2, rs1, width, aq, rl)) = { MemException(e) => { handle_mem_exception(addr, e); false }, MemValue(_) => { let rs2_val = X(rs2); - let res : MemoryOpResult(bool) = match (width, xlen) { + let res : MemoryOpResult(bool) = match (width, sizeof(xlen)) { (BYTE, _) => mem_write_value(addr, 1, rs2_val[7..0], aq, rl, false), (HALF, _) => mem_write_value(addr, 2, rs2_val[15..0], aq, rl, false), (WORD, _) => mem_write_value(addr, 4, rs2_val[31..0], aq, rl, false), @@ -378,9 +378,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 == 64 + if sizeof(xlen) == 64 <-> imm @ rs1 @ 0b000 @ rd @ 0b0011011 - if xlen == 64 + if sizeof(xlen) == 64 function clause execute (ADDIW(imm, rs1, rd)) = { let result : xlenbits = EXTS(imm) + X(rs1); @@ -389,25 +389,25 @@ function clause execute (ADDIW(imm, rs1, rd)) = { } mapping clause assembly = ADDIW(imm, rs1, rd) - if xlen == 64 + if sizeof(xlen) == 64 <-> "addiw" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ hex_bits_12(imm) - if xlen == 64 + if sizeof(xlen) == 64 /* ****************************************************************** */ union clause ast = SHIFTW : (bits(5), regbits, regbits, sop) mapping clause encdec = SHIFTW(shamt, rs1, rd, RISCV_SLLI) - if xlen == 64 + if sizeof(xlen) == 64 <-> 0b0000000 @ shamt @ rs1 @ 0b001 @ rd @ 0b0011011 - if xlen == 64 + if sizeof(xlen) == 64 mapping clause encdec = SHIFTW(shamt, rs1, rd, RISCV_SRLI) - if xlen == 64 + if sizeof(xlen) == 64 <-> 0b0000000 @ shamt @ rs1 @ 0b101 @ rd @ 0b0011011 - if xlen == 64 + if sizeof(xlen) == 64 mapping clause encdec = SHIFTW(shamt, rs1, rd, RISCV_SRAI) - if xlen == 64 + if sizeof(xlen) == 64 <-> 0b0100000 @ shamt @ rs1 @ 0b101 @ rd @ 0b0011011 - if xlen == 64 + if sizeof(xlen) == 64 function clause execute (SHIFTW(shamt, rs1, rd, op)) = { let rs1_val = (X(rs1))[31..0]; @@ -427,33 +427,33 @@ mapping shiftw_mnemonic : sop <-> string = { } mapping clause assembly = SHIFTW(shamt, rs1, rd, op) - if xlen == 64 + if sizeof(xlen) == 64 <-> shiftw_mnemonic(op) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ hex_bits_5(shamt) - if xlen == 64 + if sizeof(xlen) == 64 /* ****************************************************************** */ union clause ast = RTYPEW : (regbits, regbits, regbits, ropw) mapping clause encdec = RTYPEW(rs2, rs1, rd, RISCV_ADDW) - if xlen == 64 + if sizeof(xlen) == 64 <-> 0b0000000 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0111011 - if xlen == 64 + if sizeof(xlen) == 64 mapping clause encdec = RTYPEW(rs2, rs1, rd, RISCV_SUBW) - if xlen == 64 + if sizeof(xlen) == 64 <-> 0b0100000 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0111011 - if xlen == 64 + if sizeof(xlen) == 64 mapping clause encdec = RTYPEW(rs2, rs1, rd, RISCV_SLLW) - if xlen == 64 + if sizeof(xlen) == 64 <-> 0b0000000 @ rs2 @ rs1 @ 0b001 @ rd @ 0b0111011 - if xlen == 64 + if sizeof(xlen) == 64 mapping clause encdec = RTYPEW(rs2, rs1, rd, RISCV_SRLW) - if xlen == 64 + if sizeof(xlen) == 64 <-> 0b0000000 @ rs2 @ rs1 @ 0b101 @ rd @ 0b0111011 - if xlen == 64 + if sizeof(xlen) == 64 mapping clause encdec = RTYPEW(rs2, rs1, rd, RISCV_SRAW) - if xlen == 64 + if sizeof(xlen) == 64 <-> 0b0100000 @ rs2 @ rs1 @ 0b101 @ rd @ 0b0111011 - if xlen == 64 + if sizeof(xlen) == 64 function clause execute (RTYPEW(rs2, rs1, rd, op)) = { let rs1_val = (X(rs1))[31..0]; @@ -478,25 +478,25 @@ mapping rtypew_mnemonic : ropw <-> string = { } mapping clause assembly = RTYPEW(rs2, rs1, rd, op) - if xlen == 64 + if sizeof(xlen) == 64 <-> rtypew_mnemonic(op) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2) - if xlen == 64 + if sizeof(xlen) == 64 /* ****************************************************************** */ union clause ast = SHIFTIWOP : (bits(5), regbits, regbits, sopw) mapping clause encdec = SHIFTIWOP(shamt, rs1, rd, RISCV_SLLIW) - if xlen == 64 + if sizeof(xlen) == 64 <-> 0b0000000 @ shamt @ rs1 @ 0b001 @ rd @ 0b0011011 - if xlen == 64 + if sizeof(xlen) == 64 mapping clause encdec = SHIFTIWOP(shamt, rs1, rd, RISCV_SRLIW) - if xlen == 64 + if sizeof(xlen) == 64 <-> 0b0000000 @ shamt @ rs1 @ 0b101 @ rd @ 0b0011011 - if xlen == 64 + if sizeof(xlen) == 64 mapping clause encdec = SHIFTIWOP(shamt, rs1, rd, RISCV_SRAIW) - if xlen == 64 + if sizeof(xlen) == 64 <-> 0b0100000 @ shamt @ rs1 @ 0b101 @ rd @ 0b0011011 - if xlen == 64 + if sizeof(xlen) == 64 function clause execute (SHIFTIWOP(shamt, rs1, rd, op)) = { let rs1_val = X(rs1); @@ -516,9 +516,9 @@ mapping shiftiwop_mnemonic : sopw <-> string = { } mapping clause assembly = SHIFTIWOP(shamt, rs1, rd, op) - if xlen == 64 + if sizeof(xlen) == 64 <-> shiftiwop_mnemonic(op) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ hex_bits_5(shamt) - if xlen == 64 + if sizeof(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 3423f8e..70d4978 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 == 64 + if sizeof(xlen) == 64 <-> 0b011 @ ui53 : bits(3) @ rs1 : cregbits @ ui76 : bits(2) @ rd : cregbits @ 0b00 - if xlen == 64 + if sizeof(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 == 64 + if sizeof(xlen) == 64 <-> "c.ld" ^ spc() ^ creg_name(rdc) ^ sep() ^ creg_name(rsc) ^ sep() ^ hex_bits_8(uimm @ 0b000) - if xlen == 64 + if sizeof(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 == 64 + if sizeof(xlen) == 64 <-> 0b111 @ ui53 : bits(3) @ rs1 : bits(3) @ ui76 : bits(2) @ rs2 : bits(3) @ 0b00 - if xlen == 64 + if sizeof(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 == 64 + if sizeof(xlen) == 64 <-> "c.sd" ^ spc() ^ creg_name(rsc1) ^ sep() ^ creg_name(rsc2) ^ sep() ^ hex_bits_8(uimm @ 0b000) - if xlen == 64 + if sizeof(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 == 32 + if sizeof(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 == 32 + if sizeof(xlen) == 32 function clause execute (C_JAL(imm)) = execute(RISCV_JAL(EXTS(imm @ 0b0), ra)) mapping clause assembly = C_JAL(imm) - if xlen == 32 + if sizeof(xlen) == 32 <-> "c.jal" ^ spc() ^ hex_bits_12(imm @ 0b0) - if xlen == 32 + if sizeof(xlen) == 32 /* ****************************************************************** */ union clause ast = C_ADDIW : (bits(6), regbits) mapping clause encdec_compressed = C_ADDIW(imm5 @ imm40, rsd) - if rsd != zreg & xlen == 64 + if rsd != zreg & sizeof(xlen) == 64 <-> 0b001 @ imm5 : bits(1) @ rsd : regbits @ imm40 : bits(5) @ 0b01 - if rsd != zreg & xlen == 64 + if rsd != zreg & sizeof(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 == 64 + if sizeof(xlen) == 64 <-> "c.addiw" ^ spc() ^ reg_name(rsd) ^ sep() ^ hex_bits_6(imm) - if xlen == 64 + if sizeof(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 == 64 + if sizeof(xlen) == 64 <-> 0b100 @ 0b1 @ 0b11 @ rsd : cregbits @ 0b00 @ rs2 : cregbits @ 0b01 - if xlen == 64 + if sizeof(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 == 64 + if sizeof(xlen) == 64 <-> "c.subw" ^ spc() ^ creg_name(rsd) ^ sep() ^ creg_name(rs2) - if xlen == 64 + if sizeof(xlen) == 64 /* ****************************************************************** */ union clause ast = C_ADDW : (cregbits, cregbits) /* TODO: invalid on RV32 */ mapping clause encdec_compressed = C_ADDW(rsd, rs2) - if xlen == 64 + if sizeof(xlen) == 64 <-> 0b100 @ 0b1 @ 0b11 @ rsd : cregbits @ 0b01 @ rs2 : cregbits @ 0b01 - if xlen == 64 + if sizeof(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 == 64 + if sizeof(xlen) == 64 <-> "c.addw" ^ spc() ^ creg_name(rsd) ^ sep() ^ creg_name(rs2) - if xlen == 64 + if sizeof(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 == 64 + if rd != zreg & sizeof(xlen) == 64 <-> 0b011 @ ui5 : bits(1) @ rd : regbits @ ui43 : bits(2) @ ui86 : bits(3) @ 0b10 - if rd != zreg & xlen == 64 + if rd != zreg & sizeof(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 == 64 + if rd != zreg & sizeof(xlen) == 64 <-> "c.ldsp" ^ spc() ^ reg_name(rd) ^ sep() ^ hex_bits_6(uimm) - if rd != zreg & xlen == 64 + if rd != zreg & sizeof(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 == 64 + if sizeof(xlen) == 64 <-> 0b111 @ ui53 : bits(3) @ ui86 : bits(3) @ rs2 : regbits @ 0b10 - if xlen == 64 + if sizeof(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 == 64 + if sizeof(xlen) == 64 <-> "c.sdsp" ^ spc() ^ reg_name(rs2) ^ sep() ^ hex_bits_6(uimm) - if xlen == 64 + if sizeof(xlen) == 64 /* ****************************************************************** */ union clause ast = C_JR : (regbits) diff --git a/model/riscv_insts_mext.sail b/model/riscv_insts_mext.sail index 371966f..cab8d9c 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, rs1_int * rs2_int); + let result_wide = to_bits(2 * sizeof(xlen), rs1_int * rs2_int); let result = if high - then result_wide[(2 * xlen - 1) .. xlen] - else result_wide[(xlen - 1) .. 0]; + then result_wide[(2 * sizeof(xlen) - 1) .. sizeof(xlen)] + else result_wide[(sizeof(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, q'); + X(rd) = to_bits(sizeof(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, r); + X(rd) = to_bits(sizeof(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 == 64 + if sizeof(xlen) == 64 <-> 0b0000001 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0111011 - if xlen == 64 + if sizeof(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 == 64 + if sizeof(xlen) == 64 <-> "mulw" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2) - if xlen == 64 + if sizeof(xlen) == 64 /* ****************************************************************** */ union clause ast = DIVW : (regbits, regbits, regbits, bool) mapping clause encdec = DIVW(rs2, rs1, rd, s) - if xlen == 64 + if sizeof(xlen) == 64 <-> 0b0000001 @ rs2 @ rs1 @ 0b10 @ bool_not_bits(s) @ rd @ 0b0111011 - if xlen == 64 + if sizeof(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 == 64 + if sizeof(xlen) == 64 <-> "div" ^ maybe_not_u(s) ^ "w" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2) - if xlen == 64 + if sizeof(xlen) == 64 /* ****************************************************************** */ union clause ast = REMW : (regbits, regbits, regbits, bool) mapping clause encdec = REMW(rs2, rs1, rd, s) - if xlen == 64 + if sizeof(xlen) == 64 <-> 0b0000001 @ rs2 @ rs1 @ 0b11 @ bool_not_bits(s) @ rd @ 0b0111011 - if xlen == 64 + if sizeof(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 == 64 + if sizeof(xlen) == 64 <-> "rem" ^ maybe_not_u(s) ^ "w" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2) - if xlen == 64 + if sizeof(xlen) == 64 diff --git a/model/riscv_insts_zicsr.sail b/model/riscv_insts_zicsr.sail index 521cf0c..749f20c 100644 --- a/model/riscv_insts_zicsr.sail +++ b/model/riscv_insts_zicsr.sail @@ -15,7 +15,7 @@ mapping clause encdec = CSR(csr, rs1, rd, is_imm, op) function readCSR csr : csreg -> xlenbits = { let res : xlenbits = - match (csr, xlen) { + match (csr, sizeof(xlen)) { /* machine mode */ (0xF11, _) => EXTZ(mvendorid), (0xF12, _) => marchid, @@ -38,8 +38,8 @@ function readCSR csr : csreg -> xlenbits = { (0x3B0, _) => pmpaddr0, /* machine mode counters */ - (0xB00, _) => mcycle[(xlen - 1) .. 0], - (0xB02, _) => minstret[(xlen - 1) .. 0], + (0xB00, _) => mcycle[(sizeof(xlen) - 1) .. 0], + (0xB02, _) => minstret[(sizeof(xlen) - 1) .. 0], (0xB80, 32) => mcycle[63 .. 32], (0xB82, 32) => minstret[63 .. 32], @@ -61,9 +61,9 @@ function readCSR csr : csreg -> xlenbits = { (0x180, _) => satp, /* user mode counters */ - (0xC00, _) => mcycle[(xlen - 1) .. 0], - (0xC01, _) => mtime[(xlen - 1) .. 0], - (0xC02, _) => minstret[(xlen - 1) .. 0], + (0xC00, _) => mcycle[(sizeof(xlen) - 1) .. 0], + (0xC01, _) => mtime[(sizeof(xlen) - 1) .. 0], + (0xC02, _) => minstret[(sizeof(xlen) - 1) .. 0], (0xC80, 32) => mcycle[63 .. 32], (0xC81, 32) => mtime[63 .. 32], (0xC82, 32) => minstret[63 .. 32], @@ -81,7 +81,7 @@ function readCSR csr : csreg -> xlenbits = { function writeCSR (csr : csreg, value : xlenbits) -> unit = { let res : option(xlenbits) = - match (csr, xlen) { + match (csr, sizeof(xlen)) { /* machine mode */ (0x300, _) => { mstatus = legalize_mstatus(mstatus, value); Some(mstatus.bits()) }, (0x301, _) => { misa = legalize_misa(misa, value); Some(misa.bits()) }, @@ -100,8 +100,8 @@ function writeCSR (csr : csreg, value : xlenbits) -> unit = { (0x3B0, _) => { pmpaddr0 = value; Some(pmpaddr0) }, /* FIXME: legalize */ /* machine mode counters */ - (0xB00, _) => { mcycle[(xlen - 1) .. 0] = value; Some(value) }, - (0xB02, _) => { minstret[(xlen - 1) .. 0] = value; minstret_written = true; Some(value) }, + (0xB00, _) => { mcycle[(sizeof(xlen) - 1) .. 0] = value; Some(value) }, + (0xB02, _) => { minstret[(sizeof(xlen) - 1) .. 0] = value; minstret_written = true; Some(value) }, (0xB80, 32) => { mcycle[63 .. 32] = value; Some(value) }, (0xB82, 32) => { minstret[63 .. 32] = value; minstret_written = true; Some(value) }, diff --git a/model/riscv_jalr_rmem.sail b/model/riscv_jalr_rmem.sail index 333f385..cd8174e 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 - 1) .. 1] @ 0b0; + nextPC = newPC[(sizeof(xlen) - 1) .. 1] @ 0b0; true } diff --git a/model/riscv_jalr_seq.sail b/model/riscv_jalr_seq.sail index 3dcae61..25b9dbb 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 - 1) .. 1] @ 0b0; + let newPC : xlenbits = (X(rs1) + EXTS(imm))[(sizeof(xlen) - 1) .. 1] @ 0b0; if newPC[1] & (~ (haveRVC())) then { handle_mem_exception(newPC, E_Fetch_Addr_Align); false; diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail index 5238066..8a0e1cf 100644 --- a/model/riscv_sys_control.sail +++ b/model/riscv_sys_control.sail @@ -36,8 +36,8 @@ function is_CSR_defined (csr : bits(12), p : Privilege) -> bool = 0xB00 => p == Machine, // mcycle 0xB02 => p == Machine, // minstret - 0xB80 => p == Machine & (xlen == 32), // mcycleh - 0xB82 => p == Machine & (xlen == 32), // minstreth + 0xB80 => p == Machine & (sizeof(xlen) == 32), // mcycleh + 0xB82 => p == Machine & (sizeof(xlen) == 32), // minstreth /* disabled trigger/debug module */ 0x7a0 => p == Machine, @@ -65,9 +65,9 @@ function is_CSR_defined (csr : bits(12), p : Privilege) -> bool = 0xC01 => p == User, // time 0xC02 => p == User, // instret - 0xC80 => p == User & (xlen == 32), // cycleh - 0xC81 => p == User & (xlen == 32), // timeh - 0xC82 => p == User & (xlen == 32), // instreth + 0xC80 => p == User & (sizeof(xlen) == 32), // cycleh + 0xC81 => p == User & (sizeof(xlen) == 32), // timeh + 0xC82 => p == User & (sizeof(xlen) == 32), // instreth /* check extensions */ _ => is_UExt_CSR_defined(csr, p) // 'N' extension diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail index 36ef0bd..439d12d 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 xlen == 32 + if sizeof(xlen) == 32 then arch_to_bits(RV32) else m.bits()[35 .. 34] } function set_mstatus_SXL(m : Mstatus, a : arch_xlen) -> Mstatus = { - if xlen == 32 + if sizeof(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 xlen == 32 + if sizeof(xlen) == 32 then arch_to_bits(RV32) else m.bits()[33 .. 32] } function set_mstatus_UXL(m : Mstatus, a : arch_xlen) -> Mstatus = { - if xlen == 32 + if sizeof(xlen) == 32 then m else { let m = vector_update_subrange(m.bits(), 33, 32, a); @@ -284,7 +284,7 @@ function legalize_medeleg(o : Medeleg, v : xlenbits) -> Medeleg = { bitfield Mtvec : xlenbits = { Base : xlen - 1 .. 2, - Mode : 1 .. 0 + Mode : 1 .. 0 } register mtvec : Mtvec /* Trap Vector */ diff --git a/model/riscv_types.sail b/model/riscv_types.sail index c0e538f..8e8e163 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 - 1 -let xlen_max_signed = 2 ^ (xlen - 1) - 1 -let xlen_min_signed = 0 - 2 ^ (xlen - 1) +let xlen_max_unsigned = 2 ^ sizeof(xlen) - 1 +let xlen_max_signed = 2 ^ (sizeof(xlen) - 1) - 1 +let xlen_min_signed = 0 - 2 ^ (sizeof(xlen) - 1) type half = bits(16) type word = bits(32) diff --git a/model/riscv_xlen32.sail b/model/riscv_xlen32.sail index de7cf74..e35ce57 100644 --- a/model/riscv_xlen32.sail +++ b/model/riscv_xlen32.sail @@ -4,7 +4,3 @@ type xlen : Int = 32 type xlen_bytes : Int = 4 type xlenbits = bits(xlen) - -// value-level definitions -let xlen : int(xlen) = 32 -let xlen_bytes = 4 // byte-width of xlen bits diff --git a/model/riscv_xlen64.sail b/model/riscv_xlen64.sail index 9130ec4..7b5e14a 100644 --- a/model/riscv_xlen64.sail +++ b/model/riscv_xlen64.sail @@ -4,7 +4,3 @@ type xlen : Int = 64 type xlen_bytes : Int = 8 type xlenbits = bits(xlen) - -// value-level definitions -let xlen : int(xlen) = 64 -let xlen_bytes = 8 // byte-width of xlen bits |