Skip to content

Commit

Permalink
Failed to prove constraint, missing source line
Browse files Browse the repository at this point in the history
  • Loading branch information
@Timmmm
Timmmm committed Dec 6, 2024
1 parent fd1be4b commit 332b888
Show file tree
Hide file tree
Showing 8 changed files with 298 additions and 312 deletions.
18 changes: 12 additions & 6 deletions model/riscv_csr_ext.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -14,11 +14,17 @@ end csr_name_map
previously. */
function csr_name(csr) = csr_name_map(csr)

function clause ext_is_CSR_defined(_) = false
end ext_is_CSR_defined
function clause is_CSR_defined(_) = false
end is_CSR_defined

function clause ext_read_CSR _ = None()
end ext_read_CSR
function clause read_CSR(csr) = {
// This should be impossible because is_CSR_defined() should have returned false.
internal_error(__FILE__, __LINE__, "Read from CSR that does not exist: " ^ bits_str(csr));
}
end read_CSR

function clause ext_write_CSR (_, _) = None()
end ext_write_CSR
function clause write_CSR(csr, _) = {
// This should be impossible because is_CSR_defined() should have returned false.
internal_error(__FILE__, __LINE__, "Write to CSR that does not exist: " ^ bits_str(csr));
}
end write_CSR
12 changes: 6 additions & 6 deletions model/riscv_csr_map.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -190,13 +190,13 @@ overload to_str = {csr_name}

/* returns whether a CSR exists
*/
val ext_is_CSR_defined : (csreg) -> bool
scattered function ext_is_CSR_defined
val is_CSR_defined : (csreg) -> bool
scattered function is_CSR_defined

/* returns the value of the CSR if it is defined */
val ext_read_CSR : csreg -> option(xlenbits)
scattered function ext_read_CSR
val read_CSR : csreg -> xlenbits
scattered function read_CSR

/* returns new value (after legalisation) if the CSR is defined */
val ext_write_CSR : (csreg, xlenbits) -> option(xlenbits)
scattered function ext_write_CSR
val write_CSR : (csreg, xlenbits) -> xlenbits
scattered function write_CSR
20 changes: 10 additions & 10 deletions model/riscv_fdext_control.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -24,18 +24,18 @@ function clause extensionEnabled(Ext_D) = (misa[D] == 0b1) & (mstatus[FS] != 0b0
enum clause extension = Ext_Zfinx
function clause extensionEnabled(Ext_Zfinx) = sys_enable_zfinx()

/* val clause ext_is_CSR_defined : (csreg) -> bool */
/* val clause is_CSR_defined : (csreg) -> bool */

function clause ext_is_CSR_defined (0x001) = extensionEnabled(Ext_F) | extensionEnabled(Ext_Zfinx)
function clause ext_is_CSR_defined (0x002) = extensionEnabled(Ext_F) | extensionEnabled(Ext_Zfinx)
function clause ext_is_CSR_defined (0x003) = extensionEnabled(Ext_F) | extensionEnabled(Ext_Zfinx)
function clause is_CSR_defined (0x001) = extensionEnabled(Ext_F) | extensionEnabled(Ext_Zfinx)
function clause is_CSR_defined (0x002) = extensionEnabled(Ext_F) | extensionEnabled(Ext_Zfinx)
function clause is_CSR_defined (0x003) = extensionEnabled(Ext_F) | extensionEnabled(Ext_Zfinx)

function clause ext_read_CSR (0x001) = Some(zero_extend(fcsr[FFLAGS]))
function clause ext_read_CSR (0x002) = Some(zero_extend(fcsr[FRM]))
function clause ext_read_CSR (0x003) = Some(zero_extend(fcsr.bits))
function clause read_CSR (0x001) = zero_extend(fcsr[FFLAGS])
function clause read_CSR (0x002) = zero_extend(fcsr[FRM])
function clause read_CSR (0x003) = zero_extend(fcsr.bits)

function clause ext_write_CSR (0x001, value) = { ext_write_fcsr(fcsr[FRM], value[4..0]); Some(zero_extend(fcsr[FFLAGS])) }
function clause ext_write_CSR (0x002, value) = { ext_write_fcsr(value[2..0], fcsr[FFLAGS]); Some(zero_extend(fcsr[FRM])) }
function clause ext_write_CSR (0x003, value) = { ext_write_fcsr(value[7..5], value[4..0]); Some(zero_extend(fcsr.bits)) }
function clause write_CSR (0x001, value) = { ext_write_fcsr(fcsr[FRM], value[4..0]); zero_extend(fcsr[FFLAGS]) }
function clause write_CSR (0x002, value) = { ext_write_fcsr(value[2..0], fcsr[FFLAGS]); zero_extend(fcsr[FRM]) }
function clause write_CSR (0x003, value) = { ext_write_fcsr(value[7..5], value[4..0]); zero_extend(fcsr.bits) }

/* **************************************************************** */
323 changes: 154 additions & 169 deletions model/riscv_insts_zicsr.sail
View file

Large diffs are not rendered by default.

52 changes: 26 additions & 26 deletions model/riscv_next_control.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,33 +8,33 @@

/* Functional specification for the 'N' user-level interrupts standard extension. */

function clause ext_is_CSR_defined(0x000) = extensionEnabled(Ext_U) & extensionEnabled(Ext_N) // ustatus
function clause ext_is_CSR_defined(0x004) = extensionEnabled(Ext_U) & extensionEnabled(Ext_N) // uie
function clause ext_is_CSR_defined(0x005) = extensionEnabled(Ext_U) & extensionEnabled(Ext_N) // utvec
function clause ext_is_CSR_defined(0x040) = extensionEnabled(Ext_U) & extensionEnabled(Ext_N) // uscratch
function clause ext_is_CSR_defined(0x041) = extensionEnabled(Ext_U) & extensionEnabled(Ext_N) // uepc
function clause ext_is_CSR_defined(0x042) = extensionEnabled(Ext_U) & extensionEnabled(Ext_N) // ucause
function clause ext_is_CSR_defined(0x043) = extensionEnabled(Ext_U) & extensionEnabled(Ext_N) // utval
function clause ext_is_CSR_defined(0x044) = extensionEnabled(Ext_U) & extensionEnabled(Ext_N) // uip
function clause is_CSR_defined(0x000) = extensionEnabled(Ext_U) & extensionEnabled(Ext_N) // ustatus
function clause is_CSR_defined(0x004) = extensionEnabled(Ext_U) & extensionEnabled(Ext_N) // uie
function clause is_CSR_defined(0x005) = extensionEnabled(Ext_U) & extensionEnabled(Ext_N) // utvec
function clause is_CSR_defined(0x040) = extensionEnabled(Ext_U) & extensionEnabled(Ext_N) // uscratch
function clause is_CSR_defined(0x041) = extensionEnabled(Ext_U) & extensionEnabled(Ext_N) // uepc
function clause is_CSR_defined(0x042) = extensionEnabled(Ext_U) & extensionEnabled(Ext_N) // ucause
function clause is_CSR_defined(0x043) = extensionEnabled(Ext_U) & extensionEnabled(Ext_N) // utval
function clause is_CSR_defined(0x044) = extensionEnabled(Ext_U) & extensionEnabled(Ext_N) // uip

function clause ext_read_CSR(0x000) = Some(lower_sstatus(lower_mstatus(mstatus)).bits)
function clause ext_read_CSR(0x004) = Some(lower_sie(lower_mie(mie, mideleg), sideleg).bits)
function clause ext_read_CSR(0x005) = Some(get_utvec())
function clause ext_read_CSR(0x040) = Some(uscratch)
function clause ext_read_CSR(0x041) = Some(get_xret_target(User) & pc_alignment_mask())
function clause ext_read_CSR(0x042) = Some(ucause.bits)
function clause ext_read_CSR(0x043) = Some(utval)
function clause ext_read_CSR(0x044) = Some(lower_sip(lower_mip(mip, mideleg), sideleg).bits)
function clause read_CSR(0x000) = lower_sstatus(lower_mstatus(mstatus)).bits
function clause read_CSR(0x004) = lower_sie(lower_mie(mie, mideleg), sideleg).bits
function clause read_CSR(0x005) = get_utvec()
function clause read_CSR(0x040) = uscratch
function clause read_CSR(0x041) = get_xret_target(User) & pc_alignment_mask()
function clause read_CSR(0x042) = ucause.bits
function clause read_CSR(0x043) = utval
function clause read_CSR(0x044) = lower_sip(lower_mip(mip, mideleg), sideleg).bits

function clause ext_write_CSR(0x000, value) = { mstatus = legalize_ustatus(mstatus, value); Some(mstatus.bits) }
function clause ext_write_CSR(0x004, value) = { let sie = legalize_uie(lower_mie(mie, mideleg), sideleg, value);
function clause write_CSR(0x000, value) = { mstatus = legalize_ustatus(mstatus, value); mstatus.bits }
function clause write_CSR(0x004, value) = { let sie = legalize_uie(lower_mie(mie, mideleg), sideleg, value);
mie = lift_sie(mie, mideleg, sie);
Some(mie.bits) }
function clause ext_write_CSR(0x005, value) = { Some(set_utvec(value)) }
function clause ext_write_CSR(0x040, value) = { uscratch = value; Some(uscratch) }
function clause ext_write_CSR(0x041, value) = { Some(set_xret_target(User, value)) }
function clause ext_write_CSR(0x042, value) = { ucause.bits = value; Some(ucause.bits) }
function clause ext_write_CSR(0x043, value) = { utval = value; Some(utval) }
function clause ext_write_CSR(0x044, value) = { let sip = legalize_uip(lower_mip(mip, mideleg), sideleg, value);
mie.bits }
function clause write_CSR(0x005, value) = { set_utvec(value) }
function clause write_CSR(0x040, value) = { uscratch = value; uscratch }
function clause write_CSR(0x041, value) = { set_xret_target(User, value) }
function clause write_CSR(0x042, value) = { ucause.bits = value; ucause.bits }
function clause write_CSR(0x043, value) = { utval = value; utval }
function clause write_CSR(0x044, value) = { let sip = legalize_uip(lower_mip(mip, mideleg), sideleg, value);
mip = lift_sip(mip, mideleg, sip);
Some(mip.bits) }
mip.bits }
151 changes: 73 additions & 78 deletions model/riscv_sys_control.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -16,84 +16,79 @@ function clause extensionEnabled(Ext_Zkr) = true
function csrAccess(csr : csreg) -> csrRW = csr[11..10]
function csrPriv(csr : csreg) -> priv_level = csr[9..8]

function is_CSR_defined (csr : csreg) -> bool =
match (csr) {
/* machine mode: informational */
0xf11 => true, // mvendorid
0xf12 => true, // marchdid
0xf13 => true, // mimpid
0xf14 => true, // mhartid
0xf15 => true, // mconfigptr
/* machine mode: trap setup */
0x300 => true, // mstatus
0x301 => true, // misa
0x302 => extensionEnabled(Ext_S) | extensionEnabled(Ext_N), // medeleg
0x303 => extensionEnabled(Ext_S) | extensionEnabled(Ext_N), // mideleg
0x304 => true, // mie
0x305 => true, // mtvec
0x306 => extensionEnabled(Ext_U), // mcounteren
0x30A => extensionEnabled(Ext_U), // menvcfg
0x310 => sizeof(xlen) == 32, // mstatush
0x31A => extensionEnabled(Ext_U) & (sizeof(xlen) == 32), // menvcfgh
0x320 => true, // mcountinhibit
/* machine mode: trap handling */
0x340 => true, // mscratch
0x341 => true, // mepc
0x342 => true, // mcause
0x343 => true, // mtval
0x344 => true, // mip

// pmpcfgN
0x3A @ idx : bits(4) => sys_pmp_count() > unsigned(idx) & (idx[0] == bitzero | sizeof(xlen) == 32),

// pmpaddrN. Unfortunately the PMP index does not nicely align with the CSR index bits.
0x3B @ idx : bits(4) => sys_pmp_count() > unsigned(0b00 @ idx),
0x3C @ idx : bits(4) => sys_pmp_count() > unsigned(0b01 @ idx),
0x3D @ idx : bits(4) => sys_pmp_count() > unsigned(0b10 @ idx),
0x3E @ idx : bits(4) => sys_pmp_count() > unsigned(0b11 @ idx),
0xB00 => true, // mcycle
0xB02 => true, // minstret

0xB80 => sizeof(xlen) == 32, // mcycleh
0xB82 => sizeof(xlen) == 32, // minstreth

/* disabled trigger/debug module */
0x7a0 => true,

/* supervisor mode: trap setup */
0x100 => extensionEnabled(Ext_S), // sstatus
0x102 => extensionEnabled(Ext_S) & extensionEnabled(Ext_N), // sedeleg
0x103 => extensionEnabled(Ext_S) & extensionEnabled(Ext_N), // sideleg
0x104 => extensionEnabled(Ext_S), // sie
0x105 => extensionEnabled(Ext_S), // stvec
0x106 => extensionEnabled(Ext_S), // scounteren
0x10A => extensionEnabled(Ext_S), // senvcfg

/* supervisor mode: trap handling */
0x140 => extensionEnabled(Ext_S), // sscratch
0x141 => extensionEnabled(Ext_S), // sepc
0x142 => extensionEnabled(Ext_S), // scause
0x143 => extensionEnabled(Ext_S), // stval
0x144 => extensionEnabled(Ext_S), // sip

/* supervisor mode: address translation */
0x180 => extensionEnabled(Ext_S), // satp

/* user mode: counters */
0xC00 => extensionEnabled(Ext_U), // cycle
0xC01 => extensionEnabled(Ext_U), // time
0xC02 => extensionEnabled(Ext_U), // instret

0xC80 => extensionEnabled(Ext_U) & (sizeof(xlen) == 32), // cycleh
0xC81 => extensionEnabled(Ext_U) & (sizeof(xlen) == 32), // timeh
0xC82 => extensionEnabled(Ext_U) & (sizeof(xlen) == 32), // instreth

/* user mode: Zkr */
0x015 => extensionEnabled(Ext_Zkr),

/* check extensions */
_ => ext_is_CSR_defined(csr)
}
/* machine mode: informational */
function clause is_CSR_defined(0xf11) = true // mvendorid
function clause is_CSR_defined(0xf12) = true // marchdid
function clause is_CSR_defined(0xf13) = true // mimpid
function clause is_CSR_defined(0xf14) = true // mhartid
function clause is_CSR_defined(0xf15) = true // mconfigptr
/* machine mode: trap setup */
function clause is_CSR_defined(0x300) = true // mstatus
function clause is_CSR_defined(0x301) = true // misa
function clause is_CSR_defined(0x302) = extensionEnabled(Ext_S) | extensionEnabled(Ext_N) // medeleg
function clause is_CSR_defined(0x303) = extensionEnabled(Ext_S) | extensionEnabled(Ext_N) // mideleg
function clause is_CSR_defined(0x304) = true // mie
function clause is_CSR_defined(0x305) = true // mtvec
function clause is_CSR_defined(0x306) = extensionEnabled(Ext_U) // mcounteren
function clause is_CSR_defined(0x30A) = extensionEnabled(Ext_U) // menvcfg
function clause is_CSR_defined(0x310) = sizeof(xlen) == 32 // mstatush
function clause is_CSR_defined(0x31A) = extensionEnabled(Ext_U) & (sizeof(xlen) == 32) // menvcfgh
function clause is_CSR_defined(0x320) = true // mcountinhibit
/* machine mode: trap handling */
function clause is_CSR_defined(0x340) = true // mscratch
function clause is_CSR_defined(0x341) = true // mepc
function clause is_CSR_defined(0x342) = true // mcause
function clause is_CSR_defined(0x343) = true // mtval
function clause is_CSR_defined(0x344) = true // mip

// pmpcfgN
function clause is_CSR_defined(0x3A) @ idx : bits(4) = sys_pmp_count() > unsigned(idx) & (idx[0] == bitzero | sizeof(xlen) == 32)

// pmpaddrN. Unfortunately the PMP index does not nicely align with the CSR index bits.
function clause is_CSR_defined(0x3B) @ idx : bits(4) = sys_pmp_count() > unsigned(0b00 @ idx)
function clause is_CSR_defined(0x3C) @ idx : bits(4) = sys_pmp_count() > unsigned(0b01 @ idx)
function clause is_CSR_defined(0x3D) @ idx : bits(4) = sys_pmp_count() > unsigned(0b10 @ idx)
function clause is_CSR_defined(0x3E) @ idx : bits(4) = sys_pmp_count() > unsigned(0b11 @ idx)
function clause is_CSR_defined(0xB00) = true // mcycle
function clause is_CSR_defined(0xB02) = true // minstret

function clause is_CSR_defined(0xB80) = sizeof(xlen) == 32 // mcycleh
function clause is_CSR_defined(0xB82) = sizeof(xlen) == 32 // minstreth

/* disabled trigger/debug module */
function clause is_CSR_defined(0x7a0) = true

/* supervisor mode: trap setup */
function clause is_CSR_defined(0x100) = extensionEnabled(Ext_S) // sstatus
function clause is_CSR_defined(0x102) = extensionEnabled(Ext_S) & extensionEnabled(Ext_N) // sedeleg
function clause is_CSR_defined(0x103) = extensionEnabled(Ext_S) & extensionEnabled(Ext_N) // sideleg
function clause is_CSR_defined(0x104) = extensionEnabled(Ext_S) // sie
function clause is_CSR_defined(0x105) = extensionEnabled(Ext_S) // stvec
function clause is_CSR_defined(0x106) = extensionEnabled(Ext_S) // scounteren
function clause is_CSR_defined(0x10A) = extensionEnabled(Ext_S) // senvcfg

/* supervisor mode: trap handling */
function clause is_CSR_defined(0x140) = extensionEnabled(Ext_S) // sscratch
function clause is_CSR_defined(0x141) = extensionEnabled(Ext_S) // sepc
function clause is_CSR_defined(0x142) = extensionEnabled(Ext_S) // scause
function clause is_CSR_defined(0x143) = extensionEnabled(Ext_S) // stval
function clause is_CSR_defined(0x144) = extensionEnabled(Ext_S) // sip

/* supervisor mode: address translation */
function clause is_CSR_defined(0x180) = extensionEnabled(Ext_S) // satp

/* user mode: counters */
function clause is_CSR_defined(0xC00) = extensionEnabled(Ext_U) // cycle
function clause is_CSR_defined(0xC01) = extensionEnabled(Ext_U) // time
function clause is_CSR_defined(0xC02) = extensionEnabled(Ext_U) // instret

function clause is_CSR_defined(0xC80) = extensionEnabled(Ext_U) & (sizeof(xlen) == 32) // cycleh
function clause is_CSR_defined(0xC81) = extensionEnabled(Ext_U) & (sizeof(xlen) == 32) // timeh
function clause is_CSR_defined(0xC82) = extensionEnabled(Ext_U) & (sizeof(xlen) == 32) // instreth

/* user mode: Zkr */
function clause is_CSR_defined(0x015) = extensionEnabled(Ext_Zkr)


val check_CSR_access : (csrRW, priv_level, Privilege, bool) -> bool
function check_CSR_access(csrrw, csrpr, p, isWrite) =
Expand Down
2 changes: 1 addition & 1 deletion model/riscv_sys_regs.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -752,7 +752,7 @@ function read_seed_csr() -> xlenbits = {
}

/* Writes to the seed CSR are ignored */
function write_seed_csr () -> option(xlenbits) = None()
function write_seed_csr () -> xlenbits = zeros()

bitfield MEnvcfg : bits(64) = {
// Supervisor TimeCmp Extension
Expand Down
32 changes: 16 additions & 16 deletions model/riscv_vext_control.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6,23 +6,23 @@
/* SPDX-License-Identifier: BSD-2-Clause */
/*=======================================================================================*/

function clause ext_is_CSR_defined (0x008) = true
function clause ext_is_CSR_defined (0xC20) = true
function clause ext_is_CSR_defined (0xC21) = true
function clause ext_is_CSR_defined (0xC22) = true
function clause is_CSR_defined (0x008) = true
function clause is_CSR_defined (0xC20) = true
function clause is_CSR_defined (0xC21) = true
function clause is_CSR_defined (0xC22) = true

function clause ext_is_CSR_defined (0x009) = true
function clause ext_is_CSR_defined (0x00A) = true
function clause ext_is_CSR_defined (0x00F) = true
function clause is_CSR_defined (0x009) = true
function clause is_CSR_defined (0x00A) = true
function clause is_CSR_defined (0x00F) = true

function clause ext_read_CSR (0x009) = Some (zero_extend(vcsr[vxsat]))
function clause ext_read_CSR (0x00A) = Some (zero_extend(vcsr[vxrm]))
function clause ext_read_CSR (0x00F) = Some (zero_extend(vcsr.bits))
function clause read_CSR (0x009) = zero_extend(vcsr[vxsat])
function clause read_CSR (0x00A) = zero_extend(vcsr[vxrm])
function clause read_CSR (0x00F) = zero_extend(vcsr.bits)

function clause ext_read_CSR (0x009) = Some (zero_extend(vcsr[vxsat]))
function clause ext_read_CSR (0x00A) = Some (zero_extend(vcsr[vxrm]))
function clause ext_read_CSR (0x00F) = Some (zero_extend(vcsr.bits))
function clause read_CSR (0x009) = zero_extend(vcsr[vxsat])
function clause read_CSR (0x00A) = zero_extend(vcsr[vxrm])
function clause read_CSR (0x00F) = zero_extend(vcsr.bits)

function clause ext_write_CSR (0x009, value) = { ext_write_vcsr (vcsr[vxrm], value[0 .. 0]); Some(zero_extend(vcsr[vxsat])) }
function clause ext_write_CSR (0x00A, value) = { ext_write_vcsr (value[1 .. 0], vcsr[vxsat]); Some(zero_extend(vcsr[vxrm])) }
function clause ext_write_CSR (0x00F, value) = { ext_write_vcsr (value [2 .. 1], value [0 .. 0]); Some(zero_extend(vcsr.bits)) }
function clause write_CSR (0x009, value) = { ext_write_vcsr (vcsr[vxrm], value[0 .. 0]); zero_extend(vcsr[vxsat]) }
function clause write_CSR (0x00A, value) = { ext_write_vcsr (value[1 .. 0], vcsr[vxsat]); zero_extend(vcsr[vxrm]) }
function clause write_CSR (0x00F, value) = { ext_write_vcsr (value [2 .. 1], value [0 .. 0]); zero_extend(vcsr.bits) }

0 comments on commit 332b888

Please sign in to comment.