From e182c4c8c7f21c24970e0a30684008d2307ff998 Mon Sep 17 00:00:00 2001
From: Ved Shanbhogue <ved@rivosinc.com>
Date: Thu, 11 Jan 2024 19:28:56 -0600
Subject: [PATCH] add missing pte checks

---
 model/riscv_pte.sail | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/model/riscv_pte.sail b/model/riscv_pte.sail
index 90345cc93..2690bb47c 100644
--- a/model/riscv_pte.sail
+++ b/model/riscv_pte.sail
@@ -106,7 +106,10 @@ function isPTEPtr(p : pteAttribs, ext : extPte) -> bool = {
 
 function isInvalidPTE(p : pteAttribs, ext : extPte) -> bool = {
   let a = Mk_PTE_Bits(p);
-  a.V() == 0b0 | (a.W() == 0b1 & a.R() == 0b0)
+  a.V() == 0b0                  |
+  (a.W() == 0b1 & a.R() == 0b0) |
+  (ext != 0b0000000000)         |
+  (isPTEPtr(p, ext) & (a.D() == 0b1 | a.A() == 0b1 | a.U() == 0b1))
 }
 
 union PTE_Check = {