diff options
author | Alasdair <alasdair.armstrong@cl.cam.ac.uk> | 2023-12-12 15:48:13 +0000 |
---|---|---|
committer | Bill McSpadden <bill@riscv.org> | 2024-01-31 12:38:33 -0600 |
commit | e7c369d6993d13c1f714f66403267ee19a8ba815 (patch) | |
tree | d51d6a149b874b9b88ad66b0e5fa0671f0a9a88b /model | |
parent | 563446c477f5e905df905e0d30371a2c4d51d7a5 (diff) | |
download | sail-riscv-e7c369d6993d13c1f714f66403267ee19a8ba815.zip sail-riscv-e7c369d6993d13c1f714f66403267ee19a8ba815.tar.gz sail-riscv-e7c369d6993d13c1f714f66403267ee19a8ba815.tar.bz2 |
Update bitfield update syntax
Bitfields allow [<bitfield> with field = value], like bitvectors,
so use that instead of the old-style `update_field` overloads.
Diffstat (limited to 'model')
-rw-r--r-- | model/riscv_next_regs.sail | 28 | ||||
-rw-r--r-- | model/riscv_sys_regs.sail | 158 |
2 files changed, 83 insertions, 103 deletions
diff --git a/model/riscv_next_regs.sail b/model/riscv_next_regs.sail index c0c584b..73d4d17 100644 --- a/model/riscv_next_regs.sail +++ b/model/riscv_next_regs.sail @@ -79,14 +79,14 @@ 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 = update_UPIE(u, s[UPIE]); - let u = update_UIE(u, s[UIE]); + let u = [u with UPIE = s[UPIE]]; + let u = [u with UIE = s[UIE]]; u } function lift_ustatus(s : Sstatus, u : Ustatus) -> Sstatus = { - let s = update_UPIE(s, u[UPIE]); - let s = update_UIE(s, u[UIE]); + let s = [s with UPIE = u[UPIE]]; + let s = [s with UIE = u[UIE]]; s } @@ -107,25 +107,25 @@ 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 = update_UEI(u, s[UEI] & d[UEI]); - let u = update_UTI(u, s[UTI] & d[UTI]); - let u = update_USI(u, s[USI] & d[USI]); + let u = [u with UEI = s[UEI] & d[UEI]]; + let u = [u with UTI = s[UTI] & d[UTI]]; + let u = [u with USI = s[USI] & d[USI]]; u } /* 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 = update_UEI(u, s[UEI] & d[UEI]); - let u = update_UTI(u, s[UTI] & d[UTI]); - let u = update_USI(u, s[USI] & d[USI]); + let u = [u with UEI = s[UEI] & d[UEI]]; + let u = [u with UTI = s[UTI] & d[UTI]]; + let u = [u with USI = s[USI] & d[USI]]; u } /* Returns the new value of sip from the previous sip (o) and the written uip (u) as delegated by sideleg (d). */ function lift_uip(o : Sinterrupts, d : Sinterrupts, u : Uinterrupts) -> Sinterrupts = { let s : Sinterrupts = o; - let s = if d[USI] == 0b1 then update_USI(s, u[USI]) else s; + let s = if d[USI] == 0b1 then [s with USI = u[USI]] else s; s } @@ -136,9 +136,9 @@ function legalize_uip(s : Sinterrupts, d : Sinterrupts, v : xlenbits) -> Sinterr /* Returns the new value of sie from the previous sie (o) and the written uie (u) as delegated by sideleg (d). */ function lift_uie(o : Sinterrupts, d : Sinterrupts, u : Uinterrupts) -> Sinterrupts = { let s : Sinterrupts = o; - let s = if d[UEI] == 0b1 then update_UEI(s, u[UEI]) else s; - let s = if d[UTI] == 0b1 then update_UTI(s, u[UTI]) else s; - let s = if d[USI] == 0b1 then update_USI(s, u[USI]) else s; + let s = if d[UEI] == 0b1 then [s with UEI = u[UEI]] else s; + let s = if d[UTI] == 0b1 then [s with UTI = u[UTI]] else s; + let s = if d[USI] == 0b1 then [s with USI = u[USI]] else s; s } diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail index d11f611..fac0c97 100644 --- a/model/riscv_sys_regs.sail +++ b/model/riscv_sys_regs.sail @@ -168,11 +168,11 @@ function legalize_misa(m : Misa, v : xlenbits) -> Misa = { then m else { /* Suppress enabling C if C was disabled at boot (i.e. not supported) */ - let m = if not(sys_enable_rvc()) then m else update_C(m, v[C]); + let m = if not(sys_enable_rvc()) then m else [m with C = v[C]]; /* Suppress updates to misa.{f,d} if disabled at boot */ if not(sys_enable_fdext()) then m - else update_D(update_F(m, v[F]), v[D] & v[F]) + else [m with F = v[F], D = v[D] & v[F]] } } @@ -303,17 +303,17 @@ function legalize_mstatus(o : Mstatus, v : xlenbits) -> Mstatus = { let m : Mstatus = Mk_Mstatus(zero_extend(v[22 .. 7] @ 0b0 @ v[5 .. 3] @ 0b0 @ v[1 .. 0])); /* We don't have any extension context yet. */ - let m = update_XS(m, extStatus_to_bits(Off)); + let m = [m with XS = extStatus_to_bits(Off)]; /* FS is WARL, and making FS writable can support the M-mode emulation of an FPU * to support code running in S/U-modes. Spike does this, and for now, we match it, * but only if Zfinx isn't enabled. * FIXME: This should be made a platform parameter. */ - let m = if sys_enable_zfinx() then update_FS(m, extStatus_to_bits(Off)) else m; + let m = if sys_enable_zfinx() then [m with FS = extStatus_to_bits(Off)] else m; let dirty = extStatus_of_bits(m[FS]) == Dirty | extStatus_of_bits(m[XS]) == Dirty | extStatus_of_bits(m[VS]) == Dirty; - let m = update_SD(m, bool_to_bits(dirty)); + let m = [m with SD = bool_to_bits(dirty)]; /* We don't support dynamic changes to SXL and UXL. */ let m = set_mstatus_SXL(m, get_mstatus_SXL(o)); @@ -326,13 +326,13 @@ function legalize_mstatus(o : Mstatus, v : xlenbits) -> Mstatus = { /* Hardwired to zero in the absence of 'U' or 'N'. */ let m = if not(haveNExt()) then { - let m = update_UPIE(m, 0b0); - let m = update_UIE(m, 0b0); + let m = [m with UPIE = 0b0]; + let m = [m with UIE = 0b0]; m } else m; if not(haveUsrMode()) then { - let m = update_MPRV(m, 0b0); + let m = [m with MPRV = 0b0]; m } else m } @@ -392,42 +392,32 @@ function legalize_mip(o : Minterrupts, v : xlenbits) -> Minterrupts = { /* The only writable bits are the S-mode bits, and with the 'N' * extension, the U-mode bits. */ let v = Mk_Minterrupts(v); - let m = update_SEI(o, v[SEI]); - let m = update_STI(m, v[STI]); - let m = update_SSI(m, v[SSI]); + let m = [o with SEI = v[SEI], STI = v[STI], SSI = v[SSI]]; if haveUsrMode() & haveNExt() then { - let m = update_UEI(m, v[UEI]); - let m = update_UTI(m, v[UTI]); - let m = update_USI(m, v[USI]); - m + [m with UEI = v[UEI], UTI = v[UTI], USI = v[USI]] } else m } function legalize_mie(o : Minterrupts, v : xlenbits) -> Minterrupts = { let v = Mk_Minterrupts(v); - let m = update_MEI(o, v[MEI]); - let m = update_MTI(m, v[MTI]); - let m = update_MSI(m, v[MSI]); - let m = update_SEI(m, v[SEI]); - let m = update_STI(m, v[STI]); - let m = update_SSI(m, v[SSI]); + let m = [o with + MEI = v[MEI], + MTI = v[MTI], + MSI = v[MSI], + SEI = v[SEI], + STI = v[STI], + SSI = v[SSI] + ]; /* The U-mode bits will be modified if we have the 'N' extension. */ if haveUsrMode() & haveNExt() then { - let m = update_UEI(m, v[UEI]); - let m = update_UTI(m, v[UTI]); - let m = update_USI(m, v[USI]); - m + [m with UEI = v[UEI], UTI = v[UTI], USI = v[USI]] } else m } function legalize_mideleg(o : Minterrupts, v : xlenbits) -> Minterrupts = { /* M-mode interrupt delegation bits "should" be hardwired to 0. */ /* FIXME: needs verification against eventual spec language. */ - let m = Mk_Minterrupts(v); - let m = update_MEI(m, 0b0); - let m = update_MTI(m, 0b0); - let m = update_MSI(m, 0b0); - m + [Mk_Minterrupts(v) with MEI = 0b0, MTI = 0b0, MSI = 0b0] } /* exception processing state */ @@ -451,10 +441,8 @@ bitfield Medeleg : xlenbits = { register medeleg : Medeleg /* Delegation to S-mode */ function legalize_medeleg(o : Medeleg, v : xlenbits) -> Medeleg = { - let m = Mk_Medeleg(v); /* M-EnvCalls delegation is not supported */ - let m = update_MEnvCall(m, 0b0); - m + [Mk_Medeleg(v) with MEnvCall = 0b0] } /* registers for trap handling */ @@ -470,7 +458,7 @@ function legalize_tvec(o : Mtvec, v : xlenbits) -> Mtvec = { match (trapVectorMode_of_bits(v[Mode])) { TV_Direct => v, TV_Vector => v, - _ => update_Mode(v, o[Mode]) + _ => [v with Mode = o[Mode]] } } @@ -529,18 +517,12 @@ register scounteren : Counteren function legalize_mcounteren(c : Counteren, v : xlenbits) -> Counteren = { /* no HPM counters yet */ - let c = update_IR(c, [v[2]]); - let c = update_TM(c, [v[1]]); - let c = update_CY(c, [v[0]]); - c + [c with IR = [v[2]], TM = [v[1]], CY = [v[0]]] } function legalize_scounteren(c : Counteren, v : xlenbits) -> Counteren = { /* no HPM counters yet */ - let c = update_IR(c, [v[2]]); - let c = update_TM(c, [v[1]]); - let c = update_CY(c, [v[0]]); - c + [c with IR = [v[2]], TM = [v[1]], CY = [v[0]]] } bitfield Counterin : bits(32) = { @@ -551,9 +533,7 @@ bitfield Counterin : bits(32) = { register mcountinhibit : Counterin function legalize_mcountinhibit(c : Counterin, v : xlenbits) -> Counterin = { - let c = update_IR(c, [v[2]]); - let c = update_CY(c, [v[0]]); - c + [c with IR = [v[2]], CY = [v[0]]] } register mcycle : bits(64) @@ -620,38 +600,38 @@ 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 = update_SD(s, m[SD]); + let s = [s with SD = m[SD]]; let s = set_sstatus_UXL(s, get_mstatus_UXL(m)); - let s = update_MXR(s, m[MXR]); - let s = update_SUM(s, m[SUM]); - let s = update_XS(s, m[XS]); - let s = update_FS(s, m[FS]); - let s = update_VS(s, m[VS]); - let s = update_SPP(s, m[SPP]); - let s = update_SPIE(s, m[SPIE]); - let s = update_UPIE(s, m[UPIE]); - let s = update_SIE(s, m[SIE]); - let s = update_UIE(s, m[UIE]); + let s = [s with MXR = m[MXR]]; + let s = [s with SUM = m[SUM]]; + let s = [s with XS = m[XS]]; + let s = [s with FS = m[FS]]; + let s = [s with VS = m[VS]]; + let s = [s with SPP = m[SPP]]; + let s = [s with SPIE = m[SPIE]]; + let s = [s with UPIE = m[UPIE]]; + let s = [s with SIE = m[SIE]]; + let s = [s with UIE = m[UIE]]; s } function lift_sstatus(m : Mstatus, s : Sstatus) -> Mstatus = { - let m = update_MXR(m, s[MXR]); - let m = update_SUM(m, s[SUM]); + let m = [m with MXR = s[MXR]]; + let m = [m with SUM = s[SUM]]; - let m = update_XS(m, s[XS]); + let m = [m with XS = s[XS]]; // See comment for mstatus.FS. - let m = update_FS(m, s[FS]); - let m = update_VS(m, s[VS]); + let m = [m with FS = s[FS]]; + let m = [m with VS = s[VS]]; let dirty = extStatus_of_bits(m[FS]) == Dirty | extStatus_of_bits(m[XS]) == Dirty | extStatus_of_bits(m[VS]) == Dirty; - let m = update_SD(m, bool_to_bits(dirty)); + let m = [m with SD = bool_to_bits(dirty)]; - let m = update_SPP(m, s[SPP]); - let m = update_SPIE(m, s[SPIE]); - let m = update_UPIE(m, s[UPIE]); - let m = update_SIE(m, s[SIE]); - let m = update_UIE(m, s[UIE]); + let m = [m with SPP = s[SPP]]; + let m = [m with SPIE = s[SPIE]]; + let m = [m with UPIE = s[UPIE]]; + let m = [m with SIE = s[SIE]]; + let m = [m with UIE = s[UIE]]; m } @@ -690,35 +670,35 @@ 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 = update_SEI(s, m[SEI] & d[SEI]); - let s = update_STI(s, m[STI] & d[STI]); - let s = update_SSI(s, m[SSI] & d[SSI]); + let s = [s with SEI = m[SEI] & d[SEI]]; + let s = [s with STI = m[STI] & d[STI]]; + let s = [s with SSI = m[SSI] & d[SSI]]; - let s = update_UEI(s, m[UEI] & d[UEI]); - let s = update_UTI(s, m[UTI] & d[UTI]); - let s = update_USI(s, m[USI] & d[USI]); + let s = [s with UEI = m[UEI] & d[UEI]]; + let s = [s with UTI = m[UTI] & d[UTI]]; + let s = [s with USI = m[USI] & d[USI]]; s } /* 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 = update_SEI(s, m[SEI] & d[SEI]); - let s = update_STI(s, m[STI] & d[STI]); - let s = update_SSI(s, m[SSI] & d[SSI]); - let s = update_UEI(s, m[UEI] & d[UEI]); - let s = update_UTI(s, m[UTI] & d[UTI]); - let s = update_USI(s, m[USI] & d[USI]); + let s = [s with SEI = m[SEI] & d[SEI]]; + let s = [s with STI = m[STI] & d[STI]]; + let s = [s with SSI = m[SSI] & d[SSI]]; + let s = [s with UEI = m[UEI] & d[UEI]]; + let s = [s with UTI = m[UTI] & d[UTI]]; + let s = [s with USI = m[USI] & d[USI]]; s } /* Returns the new value of mip from the previous mip (o) and the written sip (s) as delegated by mideleg (d). */ function lift_sip(o : Minterrupts, d : Minterrupts, s : Sinterrupts) -> Minterrupts = { let m : Minterrupts = o; - let m = if d[SSI] == 0b1 then update_SSI(m, s[SSI]) else m; + let m = if d[SSI] == 0b1 then [m with SSI = s[SSI]] else m; if haveNExt() then { - let m = if d[UEI] == 0b1 then update_UEI(m, s[UEI]) else m; - let m = if d[USI] == 0b1 then update_USI(m, s[USI]) else m; + let m = if d[UEI] == 0b1 then [m with UEI = s[UEI]] else m; + let m = if d[USI] == 0b1 then [m with USI = s[USI]] else m; m } else m } @@ -730,13 +710,13 @@ function legalize_sip(m : Minterrupts, d : Minterrupts, v : xlenbits) -> Minterr /* Returns the new value of mie from the previous mie (o) and the written sie (s) as delegated by mideleg (d). */ function lift_sie(o : Minterrupts, d : Minterrupts, s : Sinterrupts) -> Minterrupts = { let m : Minterrupts = o; - let m = if d[SEI] == 0b1 then update_SEI(m, s[SEI]) else m; - let m = if d[STI] == 0b1 then update_STI(m, s[STI]) else m; - let m = if d[SSI] == 0b1 then update_SSI(m, s[SSI]) else m; + let m = if d[SEI] == 0b1 then [m with SEI = s[SEI]] else m; + let m = if d[STI] == 0b1 then [m with STI = s[STI]] else m; + let m = if d[SSI] == 0b1 then [m with SSI = s[SSI]] else m; if haveNExt() then { - let m = if d[UEI] == 0b1 then update_UEI(m, s[UEI]) else m; - let m = if d[UTI] == 0b1 then update_UTI(m, s[UTI]) else m; - let m = if d[USI] == 0b1 then update_USI(m, s[USI]) else m; + let m = if d[UEI] == 0b1 then [m with UEI = s[UEI]] else m; + let m = if d[UTI] == 0b1 then [m with UTI = s[UTI]] else m; + let m = if d[USI] == 0b1 then [m with USI = s[USI]] else m; m } else m } @@ -867,7 +847,7 @@ register senvcfg : Envcfg function legalize_envcfg(o : Envcfg, v : bits(64)) -> Envcfg = { let v = Mk_Envcfg(v); - let o = update_FIOM(o, if sys_enable_writable_fiom() then v[FIOM] else 0b0); + let o = [o with FIOM = if sys_enable_writable_fiom() then v[FIOM] else 0b0]; // Other extensions are not implemented yet so all other fields are read only zero. o } |