diff --git a/model/riscv_freg_type.sail b/model/riscv_freg_type.sail index a084c0f73..503788d53 100644 --- a/model/riscv_freg_type.sail +++ b/model/riscv_freg_type.sail @@ -12,7 +12,7 @@ type fregtype = flenbits /* default zero register */ -let zero_freg : fregtype = zero_extend(0x0) +let zero_freg : fregtype = zeros() /* default register printer */ val FRegStr : fregtype -> string diff --git a/model/riscv_insts_zca.sail b/model/riscv_insts_zca.sail index 5a6dbfb77..cadf305ad 100644 --- a/model/riscv_insts_zca.sail +++ b/model/riscv_insts_zca.sail @@ -498,7 +498,7 @@ mapping clause encdec_compressed = C_JR(rs1) if rs1 != zreg & extensionEnabled(Ext_Zca) function clause execute (C_JR(rs1)) = - execute(RISCV_JALR(zero_extend(0b0), rs1, zreg)) + execute(RISCV_JALR(zeros(), rs1, zreg)) mapping clause assembly = C_JR(rs1) if rs1 != zreg @@ -514,7 +514,7 @@ mapping clause encdec_compressed = C_JALR(rs1) if rs1 != zreg & extensionEnabled(Ext_Zca) function clause execute (C_JALR(rs1)) = - execute(RISCV_JALR(zero_extend(0b0), rs1, ra)) + execute(RISCV_JALR(zeros(), rs1, ra)) mapping clause assembly = C_JALR(rs1) if rs1 != zreg diff --git a/model/riscv_platform.sail b/model/riscv_platform.sail index e407d8aae..b29eb8325 100644 --- a/model/riscv_platform.sail +++ b/model/riscv_platform.sail @@ -309,7 +309,7 @@ register htif_payload_writes : bits(4) function reset_htif () -> unit = { htif_cmd_write = bitzero; htif_payload_writes = 0x0; - htif_tohost = zero_extend(0b0); + htif_tohost = zeros(); } /* Since the htif tohost port is only available at a single address, @@ -437,11 +437,11 @@ function mmio_write forall 'n, 0 <'n <= max_mem_access . (paddr : xlenbits, widt /* Platform initialization and ticking. */ function init_platform() -> unit = { - htif_tohost = zero_extend(0b0); + htif_tohost = zeros(); htif_done = false; - htif_exit_code = zero_extend(0b0); + htif_exit_code = zeros(); htif_cmd_write = bitzero; - htif_payload_writes = zero_extend(0b0); + htif_payload_writes = zeros(); } function tick_platform() -> unit = { diff --git a/model/riscv_reg_type.sail b/model/riscv_reg_type.sail index b4a9a0803..6e9e58ce9 100644 --- a/model/riscv_reg_type.sail +++ b/model/riscv_reg_type.sail @@ -10,7 +10,7 @@ type regtype = xlenbits /* default zero register */ -let zero_reg : regtype = zero_extend(0x0) +let zero_reg : regtype = zeros() /* default register printer */ val RegStr : regtype -> string diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail index f408c0942..a2835dda1 100644 --- a/model/riscv_sys_control.sail +++ b/model/riscv_sys_control.sail @@ -275,7 +275,7 @@ union ctl_result = { function tval(excinfo : option(xlenbits)) -> xlenbits = { match (excinfo) { Some(e) => e, - None() => zero_extend(0b0) + None() => zeros() } } @@ -416,8 +416,8 @@ function handle_interrupt(i : InterruptType, del_priv : Privilege) -> unit = function init_sys() -> unit = { cur_privilege = Machine; - mhartid = zero_extend(0b0); - mconfigptr = zero_extend(0b0); + mhartid = zeros(); + mconfigptr = zeros(); misa[MXL] = arch_to_bits(if xlen == 32 then RV32 else RV64); misa[A] = 0b1; /* atomics */ @@ -447,28 +447,28 @@ function init_sys() -> unit = { if xlen == 64 then { mstatus = Mk_Mstatus([mstatus.bits with 37 .. 36 = 0b00]) }; - mstatush.bits = zero_extend(0b0); + mstatush.bits = zeros(); - mip.bits = zero_extend(0b0); - mie.bits = zero_extend(0b0); - mideleg.bits = zero_extend(0b0); - medeleg.bits = zero_extend(0b0); - mtvec.bits = zero_extend(0b0); - mcause.bits = zero_extend(0b0); - mepc = zero_extend(0b0); - mtval = zero_extend(0b0); - mscratch = zero_extend(0b0); + mip.bits = zeros(); + mie.bits = zeros(); + mideleg.bits = zeros(); + medeleg.bits = zeros(); + mtvec.bits = zeros(); + mcause.bits = zeros(); + mepc = zeros(); + mtval = zeros(); + mscratch = zeros(); - mcycle = zero_extend(0b0); - mtime = zero_extend(0b0); + mcycle = zeros(); + mtime = zeros(); - mcounteren.bits = zero_extend(0b0); + mcounteren.bits = zeros(); - minstret = zero_extend(0b0); + minstret = zeros(); minstret_increment = true; - menvcfg.bits = zero_extend(0b0); - senvcfg.bits = zero_extend(0b0); + menvcfg.bits = zeros(); + senvcfg.bits = zeros(); /* initialize vector csrs */ elen = 0b1; /* ELEN=64 as the common case */ vlen = 0b0100; /* VLEN=512 as a default value */ @@ -476,12 +476,12 @@ function init_sys() -> unit = { /* VLEN value needs to be manually changed currently. * See riscv_vlen.sail for details. */ - vstart = zero_extend(0b0); - vl = zero_extend(0b0); + vstart = zeros(); + vl = zeros(); vcsr[vxrm] = 0b00; vcsr[vxsat] = 0b0; vtype[vill] = 0b1; - vtype[reserved] = zero_extend(0b0); + vtype[reserved] = zeros(); vtype[vma] = 0b0; vtype[vta] = 0b0; vtype[vsew] = 0b000; @@ -492,7 +492,7 @@ function init_sys() -> unit = { // log compatibility with spike if get_config_print_reg() - then print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits) ^ " (input: " ^ BitStr(zero_extend(0b0) : xlenbits) ^ ")") + then print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits) ^ " (input: " ^ BitStr(zeros() : xlenbits) ^ ")") } /* memory access exceptions, defined here for use by the platform model. */ diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail index 787b77fd9..8bbf68e75 100644 --- a/model/riscv_sys_regs.sail +++ b/model/riscv_sys_regs.sail @@ -550,7 +550,7 @@ function set_sstatus_UXL(s : Sstatus, a : arch_xlen) -> Sstatus = { } function lower_mstatus(m : Mstatus) -> Sstatus = { - let s = Mk_Sstatus(zero_extend(0b0)); + let s = Mk_Sstatus(zeros()); let s = [s with SD = m[SD]]; let s = set_sstatus_UXL(s, get_mstatus_UXL(m)); @@ -599,7 +599,7 @@ bitfield Sinterrupts : xlenbits = { /* Provides the sip read view of mip (m) as delegated by mideleg (d). */ function lower_mip(m : Minterrupts, d : Minterrupts) -> Sinterrupts = { - let s : Sinterrupts = Mk_Sinterrupts(zero_extend(0b0)); + let s : Sinterrupts = Mk_Sinterrupts(zeros()); [s with SEI = m[SEI] & d[SEI], @@ -610,7 +610,7 @@ function lower_mip(m : Minterrupts, d : Minterrupts) -> Sinterrupts = { /* Provides the sie read view of mie (m) as delegated by mideleg (d). */ function lower_mie(m : Minterrupts, d : Minterrupts) -> Sinterrupts = { - let s : Sinterrupts = Mk_Sinterrupts(zero_extend(0b0)); + let s : Sinterrupts = Mk_Sinterrupts(zeros()); [s with SEI = m[SEI] & d[SEI], diff --git a/model/rvfi_dii.sail b/model/rvfi_dii.sail index 261f1922f..6b02155b0 100644 --- a/model/rvfi_dii.sail +++ b/model/rvfi_dii.sail @@ -202,13 +202,13 @@ register rvfi_mem_data_present : bool val rvfi_zero_exec_packet : unit -> unit function rvfi_zero_exec_packet () = { - rvfi_inst_data = Mk_RVFI_DII_Execution_Packet_InstMetaData(zero_extend(0b0)); - rvfi_pc_data = Mk_RVFI_DII_Execution_Packet_PC(zero_extend(0b0)); - rvfi_int_data = Mk_RVFI_DII_Execution_Packet_Ext_Integer(zero_extend(0x0)); + rvfi_inst_data = Mk_RVFI_DII_Execution_Packet_InstMetaData(zeros()); + rvfi_pc_data = Mk_RVFI_DII_Execution_Packet_PC(zeros()); + rvfi_int_data = Mk_RVFI_DII_Execution_Packet_Ext_Integer(zeros()); // magic = "int-data" -> 0x617461642d746e69 (big-endian) rvfi_int_data = update_magic(rvfi_int_data, 0x617461642d746e69); rvfi_int_data_present = false; - rvfi_mem_data = Mk_RVFI_DII_Execution_Packet_Ext_MemAccess(zero_extend(0x0)); + rvfi_mem_data = Mk_RVFI_DII_Execution_Packet_Ext_MemAccess(zeros()); // magic = "mem-data" -> 0x617461642d6d656d (big-endian) rvfi_mem_data = update_magic(rvfi_mem_data, 0x617461642d6d656d); rvfi_mem_data_present = false; @@ -223,7 +223,7 @@ function rvfi_halt_exec_packet () = val rvfi_get_v2_support_packet : unit -> bits(704) function rvfi_get_v2_support_packet () = { - let rvfi_exec = Mk_RVFI_DII_Execution_Packet_V1(zero_extend(0b0)); + let rvfi_exec = Mk_RVFI_DII_Execution_Packet_V1(zeros()); // Returning 0x3 (using the unused high bits) in halt instead of 0x1 means // that we support the version 2 wire format. This is required to keep // backwards compatibility with old implementations that do not support @@ -234,7 +234,7 @@ function rvfi_get_v2_support_packet () = { val rvfi_get_exec_packet_v1 : unit -> bits(704) function rvfi_get_exec_packet_v1 () = { - let v1_packet = Mk_RVFI_DII_Execution_Packet_V1(zero_extend(0b0)); + let v1_packet = Mk_RVFI_DII_Execution_Packet_V1(zeros()); // Convert the v2 packet to a v1 packet let v1_packet = update_rvfi_intr(v1_packet, rvfi_inst_data[rvfi_intr]); let v1_packet = update_rvfi_halt(v1_packet, rvfi_inst_data[rvfi_halt]); @@ -273,7 +273,7 @@ val rvfi_get_exec_packet_v2 : unit -> bits(512) function rvfi_get_exec_packet_v2 () = { // TODO: add the other data // TODO: find a way to return a variable-length bitvector - let packet = Mk_RVFI_DII_Execution_PacketV2(zero_extend(0b0)); + let packet = Mk_RVFI_DII_Execution_PacketV2(zeros()); let packet = update_magic(packet, 0x32762d6563617274); // ASCII "trace-v2" (BE) let packet = update_basic_data(packet, rvfi_inst_data.bits); let packet = update_pc_data(packet, rvfi_pc_data.bits);