Merge pull request #306 from lschuermann/dev/csr-plugin-formal-halt

CsrPlugin: insert FORMAL_HALT := False
SpinalHDL · Feb 27, 2023 · b29eb54 · b29eb54
2 parents c655abb + 49246e7
commit b29eb54
Showing 1 changed file with 4 additions and 0 deletions.
diff --git a/src/main/scala/vexriscv/plugin/CsrPlugin.scala b/src/main/scala/vexriscv/plugin/CsrPlugin.scala
@@ -670,6 +670,10 @@ class CsrPlugin(val config: CsrPluginConfig) extends Plugin[VexRiscv] with Excep
       }
     }
 
+    // The CSR plugin will invoke a trap handler on exception, which does not
+    // count as halt-state by the RVFI spec, and neither do other instructions
+    // such as `wfi`, etc. Hence statically drive the output:
+    pipeline.stages.head.insert(FORMAL_HALT) := False
 
     case class Xtvec() extends Bundle {
       val mode = Bits(2 bits)