diff --git a/model/prelude.sail b/model/prelude.sail index 6e6718b72..fbf30ff7b 100644 --- a/model/prelude.sail +++ b/model/prelude.sail @@ -108,6 +108,8 @@ function not_bit(b) = if b == bitone then bitzero else bitone overload ~ = {not_bool, not_vec, not_bit} +val not = pure {coq: "negb", _: "not"} : forall ('p : Bool). bool('p) -> bool(not('p)) + val neq_vec = {lem: "neq"} : forall 'n. (bits('n), bits('n)) -> bool function neq_vec (x, y) = not_bool(eq_bits(x, y)) diff --git a/model/riscv_analysis.sail b/model/riscv_analysis.sail index 14cba3b62..598763d71 100644 --- a/model/riscv_analysis.sail +++ b/model/riscv_analysis.sail @@ -133,7 +133,7 @@ function initial_analysis (instr:ast) -> (regfps,regfps,regfps,niafps,diafp,inst _ => if is_imm then unsigned(rs1) != 0 else unsigned(rs1) != 0 }; iR = RFull(csr_name(csr)) :: iR; - if ~(is_imm) then { + if not(is_imm) then { iR = RFull(GPRstr(rs1)) :: iR; }; if isWrite then { @@ -306,7 +306,7 @@ function initial_analysis (instr:ast) -> (regfps,regfps,regfps,niafps,diafp,inst _ => if is_imm then unsigned(rs1) != 0 else unsigned(rs1) != 0 }; iR = RFull(csr_name(csr)) :: iR; - if ~(is_imm) then { + if not(is_imm) then { iR = RFull(GPRstr(rs1)) :: iR; }; if isWrite then { diff --git a/model/riscv_fetch.sail b/model/riscv_fetch.sail index 608ba01ea..3120cc6fd 100644 --- a/model/riscv_fetch.sail +++ b/model/riscv_fetch.sail @@ -70,7 +70,7 @@ * to check PC validity *before* standard fetch processing checks. */ -function isRVC(h : half) -> bool = ~ (h[1 .. 0] == 0b11) +function isRVC(h : half) -> bool = not(h[1 .. 0] == 0b11) val fetch : unit -> FetchResult effect {escape, rmem, rmemt, rreg, wmv, wmvt, wreg} function fetch() -> FetchResult = @@ -80,7 +80,7 @@ function fetch() -> FetchResult = match ext_fetch_check_pc(PC, PC) { Ext_FetchAddr_Error(e) => F_Ext_Error(e), Ext_FetchAddr_OK(use_pc) => { - if (use_pc[0] != bitzero | (use_pc[1] != bitzero & (~ (haveRVC())))) + if (use_pc[0] != bitzero | (use_pc[1] != bitzero & not(haveRVC()))) then F_Error(E_Fetch_Addr_Align(), PC) else match translateAddr(use_pc, Execute()) { TR_Failure(e, _) => F_Error(e, PC), diff --git a/model/riscv_fetch_rvfi.sail b/model/riscv_fetch_rvfi.sail index ca3cca3af..5c7ba3bcc 100644 --- a/model/riscv_fetch_rvfi.sail +++ b/model/riscv_fetch_rvfi.sail @@ -77,7 +77,7 @@ function fetch() -> FetchResult = { Ext_FetchAddr_Error(e) => F_Ext_Error(e), Ext_FetchAddr_OK(use_pc) => { /* then check PC alignment */ - if (use_pc[0] != bitzero | (use_pc[1] != bitzero & (~ (haveRVC())))) + if (use_pc[0] != bitzero | (use_pc[1] != bitzero & not(haveRVC()))) then F_Error(E_Fetch_Addr_Align(), PC) else match translateAddr(use_pc, Execute()) { TR_Failure(e, _) => F_Error(e, PC), diff --git a/model/riscv_insts_aext.sail b/model/riscv_insts_aext.sail index 1fb995c46..22523e266 100644 --- a/model/riscv_insts_aext.sail +++ b/model/riscv_insts_aext.sail @@ -141,7 +141,7 @@ function clause execute(LOADRES(aq, rl, rs1, width, rd)) = { /* "LR faults like a normal load, even though it's in the AMO major opcode space." * - Andrew Waterman, isa-dev, 10 Jul 2018. */ - if (~ (aligned)) + if not(aligned) then { handle_mem_exception(vaddr, E_Load_Addr_Align()); RETIRE_FAIL } else match translateAddr(vaddr, Read(Data)) { TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, @@ -199,7 +199,7 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = { WORD => vaddr[1..0] == 0b00, DOUBLE => vaddr[2..0] == 0b000 }; - if (~ (aligned)) + if not(aligned) then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); RETIRE_FAIL } else { if match_reservation(vaddr) == false then { diff --git a/model/riscv_insts_base.sail b/model/riscv_insts_base.sail index 071c3a9af..b6d792cb6 100644 --- a/model/riscv_insts_base.sail +++ b/model/riscv_insts_base.sail @@ -127,7 +127,7 @@ function clause execute (RISCV_JAL(imm, rd)) = { }, Ext_ControlAddr_OK(target) => { /* Perform standard alignment check */ - if bit_to_bool(target[1]) & (~ (haveRVC())) + if bit_to_bool(target[1]) & not(haveRVC()) then { handle_mem_exception(target, E_Fetch_Addr_Align()); RETIRE_FAIL @@ -191,7 +191,7 @@ function clause execute (BTYPE(imm, rs2, rs1, op)) = { RETIRE_FAIL }, Ext_ControlAddr_OK(target) => { - if bit_to_bool(target[1]) & (~ (haveRVC())) then { + if bit_to_bool(target[1]) & not(haveRVC()) then { handle_mem_exception(target, E_Fetch_Addr_Align()); RETIRE_FAIL; } else { @@ -357,8 +357,8 @@ union clause ast = LOAD : (bits(12), regidx, regidx, bool, word_width, bool, boo /* unsigned loads are only present for widths strictly less than xlen, signed loads also present for widths equal to xlen */ -mapping clause encdec = LOAD(imm, rs1, rd, is_unsigned, size, false, false) if (word_width_bytes(size) < sizeof(xlen_bytes)) | (not_bool(is_unsigned) & word_width_bytes(size) <= sizeof(xlen_bytes)) - <-> imm @ rs1 @ bool_bits(is_unsigned) @ size_bits(size) @ rd @ 0b0000011 if (word_width_bytes(size) < sizeof(xlen_bytes)) | (not_bool(is_unsigned) & word_width_bytes(size) <= sizeof(xlen_bytes)) +mapping clause encdec = LOAD(imm, rs1, rd, is_unsigned, size, false, false) if (word_width_bytes(size) < sizeof(xlen_bytes)) | (not(is_unsigned) & word_width_bytes(size) <= sizeof(xlen_bytes)) + <-> imm @ rs1 @ bool_bits(is_unsigned) @ size_bits(size) @ rd @ 0b0000011 if (word_width_bytes(size) < sizeof(xlen_bytes)) | (not(is_unsigned) & word_width_bytes(size) <= sizeof(xlen_bytes)) val extend_value : forall 'n, 0 < 'n <= xlen_bytes. (bool, MemoryOpResult(bits(8 * 'n))) -> MemoryOpResult(xlenbits) function extend_value(is_unsigned, value) = match (value) { @@ -789,7 +789,7 @@ mapping clause encdec = MRET() function clause execute MRET() = { if cur_privilege != Machine then { handle_illegal(); RETIRE_FAIL } - else if ~(ext_check_xret_priv (Machine)) + else if not(ext_check_xret_priv (Machine)) then { ext_fail_xret_priv(); RETIRE_FAIL } else { set_next_pc(exception_handler(cur_privilege, CTL_MRET(), PC)); @@ -808,12 +808,12 @@ mapping clause encdec = SRET() function clause execute SRET() = { let sret_illegal : bool = match cur_privilege { User => true, - Supervisor => ~ (haveSupMode ()) | mstatus.TSR() == 0b1, - Machine => ~ (haveSupMode ()) + Supervisor => not(haveSupMode ()) | mstatus.TSR() == 0b1, + Machine => not(haveSupMode ()) }; if sret_illegal then { handle_illegal(); RETIRE_FAIL } - else if ~(ext_check_xret_priv (Supervisor)) + else if not(ext_check_xret_priv (Supervisor)) then { ext_fail_xret_priv(); RETIRE_FAIL } else { set_next_pc(exception_handler(cur_privilege, CTL_SRET(), PC)); diff --git a/model/riscv_insts_next.sail b/model/riscv_insts_next.sail index 3673a050d..98147f417 100644 --- a/model/riscv_insts_next.sail +++ b/model/riscv_insts_next.sail @@ -75,10 +75,10 @@ mapping clause encdec = URET() <-> 0b0000000 @ 0b00010 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011 function clause execute URET() = { - if (~ (haveUsrMode()) | ~(sys_enable_next())) + if not(haveUsrMode()) | not(sys_enable_next()) then handle_illegal() - else if ~ (ext_check_xret_priv (User)) - then ext_fail_xret_priv () + else if not(ext_check_xret_priv(User)) + then ext_fail_xret_priv() else set_next_pc(exception_handler(cur_privilege, CTL_URET(), PC)); RETIRE_FAIL } diff --git a/model/riscv_insts_zbb.sail b/model/riscv_insts_zbb.sail index 7b9fa8921..311445c95 100644 --- a/model/riscv_insts_zbb.sail +++ b/model/riscv_insts_zbb.sail @@ -253,7 +253,7 @@ function clause execute (RISCV_CLZ(rs1, rd)) = { result : nat = 0; done : bool = false; foreach (i from (sizeof(xlen) - 1) downto 0) - if ~(done) then if rs1_val[i] == bitzero + if not(done) then if rs1_val[i] == bitzero then result = result + 1 else done = true; X(rd) = to_bits(sizeof(xlen), result); @@ -274,7 +274,7 @@ function clause execute (RISCV_CLZW(rs1, rd)) = { result : nat = 0; done : bool = false; foreach (i from 31 downto 0) - if ~(done) then if rs1_val[i] == bitzero + if not(done) then if rs1_val[i] == bitzero then result = result + 1 else done = true; X(rd) = to_bits(sizeof(xlen), result); @@ -295,7 +295,7 @@ function clause execute (RISCV_CTZ(rs1, rd)) = { result : nat = 0; done : bool = false; foreach (i from 0 to (sizeof(xlen) - 1)) - if ~(done) then if rs1_val[i] == bitzero + if not(done) then if rs1_val[i] == bitzero then result = result + 1 else done = true; X(rd) = to_bits(sizeof(xlen), result); @@ -316,7 +316,7 @@ function clause execute (RISCV_CTZW(rs1, rd)) = { result : nat = 0; done : bool = false; foreach (i from 0 to 31) - if ~(done) then if rs1_val[i] == bitzero + if not(done) then if rs1_val[i] == bitzero then result = result + 1 else done = true; X(rd) = to_bits(sizeof(xlen), result); diff --git a/model/riscv_insts_zicsr.sail b/model/riscv_insts_zicsr.sail index 518396f91..08c7a19a0 100644 --- a/model/riscv_insts_zicsr.sail +++ b/model/riscv_insts_zicsr.sail @@ -256,9 +256,9 @@ function clause execute CSR(csr, rs1, rd, is_imm, op) = { CSRRW => true, _ => if is_imm then unsigned(rs1_val) != 0 else unsigned(rs1) != 0 }; - if ~ (check_CSR(csr, cur_privilege, isWrite)) + if not(check_CSR(csr, cur_privilege, isWrite)) then { handle_illegal(); RETIRE_FAIL } - else if ~ (ext_check_CSR(csr, cur_privilege, isWrite)) + else if not(ext_check_CSR(csr, cur_privilege, isWrite)) then { ext_check_CSR_fail(); RETIRE_FAIL } else { let csr_val = readCSR(csr); /* could have side-effects, so technically shouldn't perform for CSRW[I] with rd == 0 */ diff --git a/model/riscv_jalr_seq.sail b/model/riscv_jalr_seq.sail index 78a95cce0..d115744de 100644 --- a/model/riscv_jalr_seq.sail +++ b/model/riscv_jalr_seq.sail @@ -84,7 +84,7 @@ function clause execute (RISCV_JALR(imm, rs1, rd)) = { }, Ext_ControlAddr_OK(addr) => { let target = [addr with 0 = bitzero]; /* clear addr[0] */ - if bit_to_bool(target[1]) & ~(haveRVC()) then { + if bit_to_bool(target[1]) & not(haveRVC()) then { handle_mem_exception(target, E_Fetch_Addr_Align()); RETIRE_FAIL } else { diff --git a/model/riscv_mem.sail b/model/riscv_mem.sail index bc8078124..ef5e5e978 100644 --- a/model/riscv_mem.sail +++ b/model/riscv_mem.sail @@ -142,7 +142,7 @@ function checked_mem_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType( /* PMP checks if enabled */ function pmp_mem_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(ext_access_type), p : Privilege, paddr : xlenbits, width : atom('n), aq : bool, rl : bool, res: bool, meta : bool) -> MemoryOpResult((bits(8 * 'n), mem_meta)) = - if (~ (plat_enable_pmp ())) + if not(plat_enable_pmp()) then checked_mem_read(t, paddr, width, aq, rl, res, meta) else { match pmpCheck(paddr, width, t, p) { @@ -188,7 +188,7 @@ $endif /* The most generic memory read operation */ function mem_read_priv_meta (typ, priv, paddr, width, aq, rl, res, meta) = { let result : MemoryOpResult((bits(8 * 'n), mem_meta)) = - if (aq | res) & (~ (is_aligned_addr(paddr, width))) + if (aq | res) & not(is_aligned_addr(paddr, width)) then MemException(E_Load_Addr_Align()) else match (aq, rl, res) { (false, true, false) => throw(Error_not_implemented("load.rl")), @@ -213,7 +213,7 @@ function mem_read (typ, paddr, width, aq, rel, res) = val mem_write_ea : forall 'n, 0 < 'n <= max_mem_access . (xlenbits, atom('n), bool, bool, bool) -> MemoryOpResult(unit) effect {eamem, escape} function mem_write_ea (addr, width, aq, rl, con) = { - if (rl | con) & (~ (is_aligned_addr(addr, width))) + if (rl | con) & not(is_aligned_addr(addr, width)) then MemException(E_SAMO_Addr_Align()) else match (aq, rl, con) { (false, false, false) => MemValue(write_ram_ea(Write_plain, addr, width)), @@ -267,7 +267,7 @@ function checked_mem_write forall 'n, 0 < 'n <= max_mem_access . (wk : write_kin /* PMP checks if enabled */ function pmp_mem_write forall 'n, 0 < 'n <= max_mem_access . (wk: write_kind, paddr : xlenbits, width : atom('n), data: bits(8 * 'n), typ: AccessType(ext_access_type), priv: Privilege, meta: mem_meta) -> MemoryOpResult(bool) = - if (~ (plat_enable_pmp ())) + if not(plat_enable_pmp()) then checked_mem_write(wk, paddr, width, data, meta) else { match pmpCheck(paddr, width, typ, priv) { @@ -286,7 +286,7 @@ function pmp_mem_write forall 'n, 0 < 'n <= max_mem_access . (wk: write_kind, pa val mem_write_value_priv_meta : forall 'n, 0 < 'n <= max_mem_access . (xlenbits, atom('n), bits(8 * 'n), AccessType(ext_access_type), Privilege, mem_meta, bool, bool, bool) -> MemoryOpResult(bool) effect {wmv, wmvt, rreg, wreg, escape} function mem_write_value_priv_meta (paddr, width, value, typ, priv, meta, aq, rl, con) = { rvfi_write(paddr, width, value, meta); - if (rl | con) & (~ (is_aligned_addr(paddr, width))) + if (rl | con) & not(is_aligned_addr(paddr, width)) then MemException(E_SAMO_Addr_Align()) else { let wk : write_kind = match (aq, rl, con) { diff --git a/model/riscv_step.sail b/model/riscv_step.sail index df53faeb0..8d19ebfa9 100644 --- a/model/riscv_step.sail +++ b/model/riscv_step.sail @@ -145,7 +145,7 @@ function loop () : unit -> unit = { let insns_per_tick = plat_insns_per_tick(); i : int = 0; step_no : int = 0; - while (~ (htif_done)) do { + while not(htif_done) do { let stepped = step(step_no); if stepped then step_no = step_no + 1; diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail index 1d401aeb2..668136776 100644 --- a/model/riscv_sys_control.sail +++ b/model/riscv_sys_control.sail @@ -166,11 +166,11 @@ function is_CSR_defined (csr : csreg, p : Privilege) -> bool = val check_CSR_access : (csrRW, priv_level, Privilege, bool) -> bool function check_CSR_access(csrrw, csrpr, p, isWrite) = - (~ (isWrite == true & csrrw == 0b11)) /* read/write */ + not(isWrite == true & csrrw == 0b11) /* read/write */ & (privLevel_to_bits(p) >=_u csrpr) /* privilege */ function check_TVM_SATP(csr : csreg, p : Privilege) -> bool = - ~ (csr == 0x180 & p == Supervisor & mstatus.TVM() == 0b1) + not(csr == 0x180 & p == Supervisor & mstatus.TVM() == 0b1) function check_Counteren(csr : csreg, p : Privilege) -> bool = match(csr, p) { @@ -178,9 +178,9 @@ function check_Counteren(csr : csreg, p : Privilege) -> bool = (0xC01, Supervisor) => mcounteren.TM() == 0b1, (0xC02, Supervisor) => mcounteren.IR() == 0b1, - (0xC00, User) => mcounteren.CY() == 0b1 & ((~ (haveSupMode())) | scounteren.CY() == 0b1), - (0xC01, User) => mcounteren.TM() == 0b1 & ((~ (haveSupMode())) | scounteren.TM() == 0b1), - (0xC02, User) => mcounteren.IR() == 0b1 & ((~ (haveSupMode())) | scounteren.IR() == 0b1), + (0xC00, User) => mcounteren.CY() == 0b1 & (not(haveSupMode()) | scounteren.CY() == 0b1), + (0xC01, User) => mcounteren.TM() == 0b1 & (not(haveSupMode()) | scounteren.TM() == 0b1), + (0xC02, User) => mcounteren.IR() == 0b1 & (not(haveSupMode()) | scounteren.IR() == 0b1), (_, _) => /* no HPM counters for now */ if 0xC03 <=_u csr & csr <=_u 0xC1F @@ -193,9 +193,9 @@ function check_Counteren(csr : csreg, p : Privilege) -> bool = * allowed in the current priv mode */ function check_seed_CSR (csr : csreg, p : Privilege, isWrite : bool) -> bool = { - if ~(csr == 0x015) then { + if not(csr == 0x015) then { true - } else if ~(isWrite) then { + } else if not(isWrite) then { /* Read-only access to the seed CSR is not allowed */ false } else { @@ -315,7 +315,7 @@ function getPendingSet(priv : Privilege) -> option((xlenbits, Privilege)) = { Ints_Empty() => None(), Ints_Pending(p) => let r = (p, Machine) in Some(r), Ints_Delegated(d) => - if (~ (haveSupMode())) then { + if not(haveSupMode()) then { if uIE then let r = (d, User) in Some(r) else None() } else { @@ -339,7 +339,7 @@ function dispatchInterrupt(priv : Privilege) -> option((InterruptType, Privilege /* If we don't have different privilege levels, we don't need to check delegation. * Absence of U-mode implies absence of S-mode. */ - if (~ (haveUsrMode())) | ((~ (haveSupMode())) & (~ (haveNExt()))) then { + if not(haveUsrMode()) | (not(haveSupMode()) & not(haveNExt())) then { assert(priv == Machine, "invalid current privilege"); let enabled_pending = mip.bits() & mie.bits(); match findPendingInterrupt(enabled_pending) { diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail index 04a6fe410..e1576ed6f 100644 --- a/model/riscv_sys_regs.sail +++ b/model/riscv_sys_regs.sail @@ -161,11 +161,11 @@ function legalize_misa(m : Misa, v : xlenbits) -> Misa = { let v = Mk_Misa(v); /* Suppress changing C if nextPC would become misaligned or an extension vetoes or C was disabled at boot (i.e. not supported). */ let m = - if (v.C() == 0b0 & (nextPC[1] == bitone | ext_veto_disable_C())) | ~(sys_enable_rvc()) + if (v.C() == 0b0 & (nextPC[1] == bitone | ext_veto_disable_C())) | not(sys_enable_rvc()) then m else update_C(m, v.C()); /* Handle updates for F/D. */ - if ~(sys_enable_fdext()) | (v.D() == 0b1 & v.F() == 0b0) + if not(sys_enable_fdext()) | (v.D() == 0b1 & v.F() == 0b0) then m else update_D(update_F(m, v.F()), v.D()) } @@ -316,13 +316,13 @@ function legalize_mstatus(o : Mstatus, v : xlenbits) -> Mstatus = { } else m; /* Hardwired to zero in the absence of 'U' or 'N'. */ - let m = if (~ (haveNExt())) then { + let m = if not(haveNExt()) then { let m = update_UPIE(m, 0b0); let m = update_UIE(m, 0b0); m } else m; - if (~ (haveUsrMode())) then { + if not(haveUsrMode()) then { let m = update_MPRV(m, 0b0); m } else m diff --git a/model/riscv_vmem_sv32.sail b/model/riscv_vmem_sv32.sail index 2b1784415..d2e86e342 100644 --- a/model/riscv_vmem_sv32.sail +++ b/model/riscv_vmem_sv32.sail @@ -197,7 +197,7 @@ function translate32(asid, ptb, vAddr, ac, priv, mxr, do_sum, level, ext_ptw) = match update_PTE_Bits(pteBits, ac, ext_pte) { None() => TR_Address(ent.pAddr | EXTZ(vAddr & ent.vAddrMask), ext_ptw), Some(pbits, ext) => { - if ~ (plat_enable_dirty_update ()) + if not(plat_enable_dirty_update()) then { /* pte needs dirty/accessed update but that is not enabled */ TR_Failure(PTW_PTE_Update(), ext_ptw) @@ -230,7 +230,7 @@ function translate32(asid, ptb, vAddr, ac, priv, mxr, do_sum, level, ext_ptw) = TR_Address(pAddr, ext_ptw) }, Some(pbits, ext) => - if ~ (plat_enable_dirty_update ()) + if not(plat_enable_dirty_update()) then { /* pte needs dirty/accessed update but that is not enabled */ TR_Failure(PTW_PTE_Update(), ext_ptw) diff --git a/model/riscv_vmem_sv39.sail b/model/riscv_vmem_sv39.sail index 31fbdea47..a6c64e17e 100644 --- a/model/riscv_vmem_sv39.sail +++ b/model/riscv_vmem_sv39.sail @@ -191,7 +191,7 @@ function translate39(asid, ptb, vAddr, ac, priv, mxr, do_sum, level, ext_ptw) = match update_PTE_Bits(pteBits, ac, ext_pte) { None() => TR_Address(ent.pAddr | EXTZ(vAddr & ent.vAddrMask), ext_ptw), Some(pbits, ext) => { - if ~ (plat_enable_dirty_update ()) + if not(plat_enable_dirty_update()) then { /* pte needs dirty/accessed update but that is not enabled */ TR_Failure(PTW_PTE_Update(), ext_ptw) @@ -224,7 +224,7 @@ function translate39(asid, ptb, vAddr, ac, priv, mxr, do_sum, level, ext_ptw) = TR_Address(pAddr, ext_ptw) }, Some(pbits, ext) => - if ~ (plat_enable_dirty_update ()) + if not(plat_enable_dirty_update()) then { /* pte needs dirty/accessed update but that is not enabled */ TR_Failure(PTW_PTE_Update(), ext_ptw) diff --git a/model/riscv_vmem_sv48.sail b/model/riscv_vmem_sv48.sail index 87a8669a6..57ebf8cac 100644 --- a/model/riscv_vmem_sv48.sail +++ b/model/riscv_vmem_sv48.sail @@ -188,7 +188,7 @@ function translate48(asid, ptb, vAddr, ac, priv, mxr, do_sum, level, ext_ptw) = TR_Address(pAddr, ext_ptw) }, Some(pbits, ext) => - if ~ (plat_enable_dirty_update ()) + if not(plat_enable_dirty_update()) then { /* pte needs dirty/accessed update but that is not enabled */ TR_Failure(PTW_PTE_Update(), ext_ptw) diff --git a/model/riscv_vmem_tlb.sail b/model/riscv_vmem_tlb.sail index a3e1c7e0c..69b495872 100644 --- a/model/riscv_vmem_tlb.sail +++ b/model/riscv_vmem_tlb.sail @@ -115,8 +115,8 @@ function flush_TLB_Entry(e, asid, addr) = { match(asid, addr) { ( None(), None()) => true, ( None(), Some(a)) => e.vAddr == (e.vMatchMask & a), - (Some(i), None()) => (e.asid == i) & (~ (e.global)), + (Some(i), None()) => (e.asid == i) & not(e.global), (Some(i), Some(a)) => ( (e.asid == i) & (e.vAddr == (a & e.vMatchMask)) - & (~ (e.global))) + & not(e.global)) } }