Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Replace zero_extend(0b0) with zeros() #598

Merged
merged 1 commit into from
Oct 16, 2024
Merged

Replace zero_extend(0b0) with zeros() #598

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion model/riscv_freg_type.sail
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
4 changes: 2 additions & 2 deletions model/riscv_insts_zca.sail
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand Down
8 changes: 4 additions & 4 deletions model/riscv_platform.sail
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down Expand Up @@ -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 = {
Expand Down
2 changes: 1 addition & 1 deletion model/riscv_reg_type.sail
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
46 changes: 23 additions & 23 deletions model/riscv_sys_control.sail
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -275,7 +275,7 @@ union ctl_result = {
function tval(excinfo : option(xlenbits)) -> xlenbits = {
match (excinfo) {
Some(e) => e,
None() => zero_extend(0b0)
None() => zeros()
}
}

Expand Down Expand Up @@ -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 */
Expand Down Expand Up @@ -447,41 +447,41 @@ 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 */
vlenb = to_bits(xlen, 2 ^ (get_vlen_pow() - 3)); /* vlenb holds the constant value VLEN/8 */
/* 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;
Expand All @@ -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. */
Expand Down
6 changes: 3 additions & 3 deletions model/riscv_sys_regs.sail
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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));

Expand Down Expand Up @@ -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],
Expand All @@ -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],
Expand Down
14 changes: 7 additions & 7 deletions model/rvfi_dii.sail
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -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
Expand All @@ -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]);
Expand Down Expand Up @@ -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);
Expand Down
Loading