diff --git a/src/main/scala/vexriscv/Services.scala b/src/main/scala/vexriscv/Services.scala
index 140c69b..f0ef713 100644
--- a/src/main/scala/vexriscv/Services.scala
+++ b/src/main/scala/vexriscv/Services.scala
@@ -50,6 +50,20 @@ trait PrivilegeService{
   def isSupervisor() : Bool
   def isMachine() : Bool
   def forceMachine() : Unit
+
+  def encodeBits() : Bits = {
+    val encoded = Bits(2 bits)
+
+    when(this.isUser()) {
+      encoded := "00"
+    }.elsewhen(this.isSupervisor()) {
+      encoded := "01"
+    }.otherwise {
+      encoded := "11"
+    }
+
+    encoded
+  }
 }
 
 case class PrivilegeServiceDefault() extends PrivilegeService{
diff --git a/src/main/scala/vexriscv/VexRiscv.scala b/src/main/scala/vexriscv/VexRiscv.scala
index ed7e37e..ebf2008 100644
--- a/src/main/scala/vexriscv/VexRiscv.scala
+++ b/src/main/scala/vexriscv/VexRiscv.scala
@@ -95,6 +95,7 @@ case class VexRiscvConfig(){
   object FORMAL_MEM_RDATA  extends Stageable(Bits(32 bits))
   object FORMAL_MEM_WDATA  extends Stageable(Bits(32 bits))
   object FORMAL_INSTRUCTION extends Stageable(Bits(32 bits))
+  object FORMAL_MODE       extends Stageable(Bits(2 bits))
 
 
   object Src1CtrlEnum extends SpinalEnum(binarySequential){
diff --git a/src/main/scala/vexriscv/plugin/Fetcher.scala b/src/main/scala/vexriscv/plugin/Fetcher.scala
index f793084..061be18 100644
--- a/src/main/scala/vexriscv/plugin/Fetcher.scala
+++ b/src/main/scala/vexriscv/plugin/Fetcher.scala
@@ -415,6 +415,8 @@ abstract class IBusFetcherImpl(val resetVector : BigInt,
         decode.arbitration.isValid clearWhen(forceNoDecodeCond)
       })
 
+      val privilegeService = pipeline.serviceElse(classOf[PrivilegeService], PrivilegeServiceDefault())
+
       //Formal verification signals generation, miss prediction stuff ?
       val formal = new Area {
         val raw = if(compressedGen) decompressor.raw else inputBeforeStage.rsp.inst
@@ -437,6 +439,11 @@ abstract class IBusFetcherImpl(val resetVector : BigInt,
             info.stage.output(FORMAL_PC_NEXT) := info.interface.payload
           }
         })
+
+        // Forward the current CPU "mode" (privilege level) from the fetch
+	// stage, which is where it can begin to affect the current
+	// execution (e.g., through PMP checks).
+        decode.insert(FORMAL_MODE) := privilegeService.encodeBits()
       }
     }
 
diff --git a/src/main/scala/vexriscv/plugin/FormalPlugin.scala b/src/main/scala/vexriscv/plugin/FormalPlugin.scala
index 2d70ebd..5b5e0d5 100644
--- a/src/main/scala/vexriscv/plugin/FormalPlugin.scala
+++ b/src/main/scala/vexriscv/plugin/FormalPlugin.scala
@@ -93,7 +93,7 @@ class FormalPlugin extends Plugin[VexRiscv]{
       rvfi.trap := False
       rvfi.halt := False
       rvfi.intr := False
-      rvfi.mode := 3
+      rvfi.mode := output(FORMAL_MODE)
       rvfi.ixl := 1
 //      rvfi.rs1.addr  := output(INSTRUCTION)(rs1Range).asUInt
 //      rvfi.rs2.addr  := output(INSTRUCTION)(rs2Range).asUInt