From 621d54735054087792a9eb1522ff980a187521bb Mon Sep 17 00:00:00 2001 From: Tim Hutt Date: Tue, 15 Oct 2024 16:08:16 +0100 Subject: [PATCH] Replace zero_extend(0b0) with zeros() I left a couple where it made sense, e.g. in STORECON. --- model/riscv_freg_type.sail | 2 +- model/riscv_insts_zca.sail | 4 +-- model/riscv_next_regs.sail | 6 ++--- model/riscv_platform.sail | 8 +++--- model/riscv_reg_type.sail | 2 +- model/riscv_sys_control.sail | 52 ++++++++++++++++++------------------ model/riscv_sys_regs.sail | 6 ++--- model/rvfi_dii.sail | 14 +++++----- 8 files changed, 47 insertions(+), 47 deletions(-) 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_next_regs.sail b/model/riscv_next_regs.sail index 64c9f77c2..7da2d0ce2 100644 --- a/model/riscv_next_regs.sail +++ b/model/riscv_next_regs.sail @@ -16,7 +16,7 @@ bitfield Ustatus : xlenbits = { /* This is a view, so there is no register defined. */ function lower_sstatus(s : Sstatus) -> Ustatus = { - let u = Mk_Ustatus(zero_extend(0b0)); + let u = Mk_Ustatus(zeros()); [u with UPIE = s[UPIE], @@ -47,7 +47,7 @@ bitfield Uinterrupts : xlenbits = { /* Provides the uip read view of sip (s) as delegated by sideleg (d). */ function lower_sip(s : Sinterrupts, d : Sinterrupts) -> Uinterrupts = { - let u : Uinterrupts = Mk_Uinterrupts(zero_extend(0b0)); + let u : Uinterrupts = Mk_Uinterrupts(zeros()); [u with UEI = s[UEI] & d[UEI], UTI = s[UTI] & d[UTI], @@ -57,7 +57,7 @@ function lower_sip(s : Sinterrupts, d : Sinterrupts) -> Uinterrupts = { /* Provides the uie read view of sie as delegated by sideleg. */ function lower_sie(s : Sinterrupts, d : Sinterrupts) -> Uinterrupts = { - let u : Uinterrupts = Mk_Uinterrupts(zero_extend(0b0)); + let u : Uinterrupts = Mk_Uinterrupts(zeros()); [u with UEI = s[UEI] & d[UEI], UTI = s[UTI] & d[UTI], 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 80e6ea5c7..fd5af51c6 100644 --- a/model/riscv_sys_control.sail +++ b/model/riscv_sys_control.sail @@ -229,9 +229,9 @@ function processPending(xip : Minterrupts, xie : Minterrupts, xideleg : xlenbits /* the others are delegated */ let effective_delg = xip.bits & xideleg; /* we have pending interrupts if this privilege is enabled */ - if priv_enabled & (effective_pend != zero_extend(0b0)) + if priv_enabled & (effective_pend != zeros()) then Ints_Pending(effective_pend) - else if effective_delg != zero_extend(0b0) + else if effective_delg != zeros() then Ints_Delegated(effective_delg) else Ints_Empty() } @@ -246,7 +246,7 @@ function processPending(xip : Minterrupts, xie : Minterrupts, xideleg : xlenbits function getPendingSet(priv : Privilege) -> option((xlenbits, Privilege)) = { assert(extensionEnabled(Ext_U), "no user mode: M/U or M/S/U system required"); let effective_pending = mip.bits & mie.bits; - if effective_pending == zero_extend(0b0) then None() /* fast path */ + if effective_pending == zeros() then None() /* fast path */ else { /* Higher privileges than the current one are implicitly enabled, * while lower privileges are blocked. An unsupported privilege is @@ -323,7 +323,7 @@ union ctl_result = { function tval(excinfo : option(xlenbits)) -> xlenbits = { match (excinfo) { Some(e) => e, - None() => zero_extend(0b0) + None() => zeros() } } @@ -496,8 +496,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 */ @@ -527,28 +527,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 */ @@ -556,12 +556,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; @@ -572,7 +572,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 2a5a219c8..4238ae3ea 100644 --- a/model/riscv_sys_regs.sail +++ b/model/riscv_sys_regs.sail @@ -572,7 +572,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)); @@ -643,7 +643,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], @@ -657,7 +657,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);