From 13d66b3ae429318d63e272c70a38f33556a7636d Mon Sep 17 00:00:00 2001
From: Leon Schuermann <leon@is.currently.online>
Date: Fri, 24 Feb 2023 16:08:39 -0500
Subject: [PATCH] Fetcher: insert FORMAL_MODE encoded from privilegeService

Previously, FORMAL_MODE would simply be hard-coded to "11", indicating
machine mode. However, that's not necessarily true when using the
CsrPlugin, which allows to switch the hart into either User or
optional Supervisor mode. Hence we create a FORMAL_MODE insert in the
fetch-phase (which is generally when the MPP register can take effect)
and generate `rvfi_mode` based on that insert.
---
 src/main/scala/vexriscv/Services.scala            | 14 ++++++++++++++
 src/main/scala/vexriscv/VexRiscv.scala            |  1 +
 src/main/scala/vexriscv/plugin/Fetcher.scala      |  7 +++++++
 src/main/scala/vexriscv/plugin/FormalPlugin.scala |  2 +-
 4 files changed, 23 insertions(+), 1 deletion(-)

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