feat: add ArbitraryRegFile in RVConfig

src/main/scala/rvspeccore/checker/ArbitraryGenerater.scala

@@ -0,0 +1,22 @@
+package rvspeccore.checker
+
+import chisel3._
+import chisel3.util._
+import chisel3.util.experimental.BoringUtils
+
+object ArbitraryRegFile {
+  val uniqueIdArbitraryRegFile = "ArbitraryRegFile"
+  def genSink(implicit XLEN: Int): Vec[UInt] = {
+    val initval = Wire(Vec(32, UInt(XLEN.W)))
+    initval := DontCare
+    BoringUtils.addSink(initval, uniqueIdArbitraryRegFile)
+    initval
+  }
+  def init(implicit XLEN: Int): Vec[UInt] = {
+    val rf = Wire(Vec(32, UInt(XLEN.W)))
+    rf.map(_ := DontCare)
+    rf(0) := 0.U
+    BoringUtils.addSource(rf, uniqueIdArbitraryRegFile)
+    rf
+  }
+}

src/main/scala/rvspeccore/checker/ConnectHelper.scala

@@ -20,11 +20,7 @@ object ConnectCheckerResult extends ConnectHelper {
   val uniqueIdEvent: String = "ConnectCheckerResult_UniqueIdEvent"
   val uniqueIdDTLB: String  = "ConnectCheckerResult_UniqueIdDTLB"
   val uniqueIdITLB: String  = "ConnectCheckerResult_UniqueIdITLB"
-  val uniqueIdRandom: String = "ConnectCheckerResult_UniqueIdRandom"
 
-  def setRandomTarget(randomVec: Vec[UInt]) = {
-    BoringUtils.addSink(randomVec, uniqueIdRandom)
-  }
   def setRegSource(regVec: Vec[UInt]) = {
     BoringUtils.addSource(regVec, uniqueIdReg)
   }
@@ -97,14 +93,17 @@ object ConnectCheckerResult extends ConnectHelper {
     event
   }
 
-  def setChecker(checker: CheckerWithResult, memDelay: Int = 0, init: Boolean = false)(implicit XLEN: Int, config: RVConfig) = {
+  def setChecker(
+      checker: CheckerWithResult,
+      memDelay: Int = 0
+  )(implicit XLEN: Int, config: RVConfig) = {
     // reg
+    if (config.formal.arbitraryRegFile) ArbitraryRegFile.init
+
     val regVec = Wire(Vec(32, UInt(XLEN.W)))
     regVec := DontCare
     BoringUtils.addSink(regVec, uniqueIdReg)
-    val initval = if(init) WireInit(VecInit(Seq.fill(32)(0.U(XLEN.W)))) else GenerateArbitraryRegFile(XLEN)
 
-    BoringUtils.addSource(initval, uniqueIdRandom)
     checker.io.result.reg := regVec
     checker.io.result.pc  := DontCare
 

src/main/scala/rvspeccore/core/RVConfig.scala

@@ -60,4 +60,11 @@ case class RVConfig(configs: (String, Any)*) {
     protected val raw       = cfgs.getOrElse("functions", Seq[String]()).asInstanceOf[Seq[String]]
     val privileged: Boolean = raw.contains("Privileged")
   }
+
+  // Formal
+  object formal {
+    protected val raw = cfgs.getOrElse("formal", Seq[String]()).asInstanceOf[Seq[String]]
+
+    val arbitraryRegFile: Boolean = raw.contains("ArbitraryRegFile")
+  }
 }

src/main/scala/rvspeccore/core/RiscvCore.scala

@@ -76,11 +76,12 @@ object State {
   def wireInit()(implicit XLEN: Int, config: RVConfig): State = {
     val state = Wire(new State)
 
-    val initval = Wire(Vec(32, UInt(XLEN.W)))
-    initval := DontCare
-    ConnectCheckerResult.setRandomTarget(initval)
-    state.reg := initval
-    // state.reg := Seq.fill(32)(0.U(XLEN.W))
+    state.reg := {
+      if (config.formal.arbitraryRegFile)
+        rvspeccore.checker.ArbitraryRegFile.genSink
+      else
+        Seq.fill(32)(0.U(XLEN.W))
+    }
     state.pc  := config.initValue.getOrElse("pc", "h8000_0000").U(XLEN.W)
     state.csr := CSR.wireInit()
 

src/test/scala/rvspeccore/checker/ArbitraryGeneraterSpec.scala

@@ -0,0 +1,32 @@
+package rvspeccore.checker
+
+import chisel3._
+import chiseltest._
+import chiseltest.formal._
+import org.scalatest.flatspec.AnyFlatSpec
+
+class TestArbitraryRegFileModule(hasBug: Boolean) extends Module {
+  implicit val XLEN: Int = 64
+  val io = IO(new Bundle {
+    val rf = Output(Vec(32, UInt(64.W)))
+  })
+  io.rf := ArbitraryRegFile.genSink
+  ArbitraryRegFile.init
+
+  if (hasBug)
+    assert(io.rf(1) === 0.U)
+  else
+    assert(io.rf(0) === 0.U)
+}
+
+class ArbitraryRegFileSpec extends AnyFlatSpec with Formal with ChiselScalatestTester {
+  behavior of "ArbitraryRegFile"
+  it should "be able to create arbitrary regFile init value" in {
+    verify(new TestArbitraryRegFileModule(false), Seq(BoundedCheck(2), BtormcEngineAnnotation))
+    assertThrows[chiseltest.formal.FailedBoundedCheckException] {
+      // fail because the rf(1) is Arbitrary, could be not 0.U
+      // this will print a "Assertion failed at ArbitraryGeneraterSpec.scala:17 assert(io.rf(1) === 0.U)"
+      verify(new TestArbitraryRegFileModule(true), Seq(BoundedCheck(2), BtormcEngineAnnotation))
+    }
+  }
+}

src/test/scala/rvspeccore/core/RVConfigSpec.scala

@@ -14,7 +14,8 @@ class RVConfigSpec extends AnyFlatSpec {
       "initValue" -> Map(
         "pc"    -> "h8000_0000",
         "mtvec" -> "h0000_01c0"
-      )
+      ),
+      "formal" -> Seq("ArbitraryRegFile")
     )
     assert(config.XLEN == 64)
     assert(config.extensions.I)
@@ -29,5 +30,6 @@ class RVConfigSpec extends AnyFlatSpec {
     assert(config.initValue("pc") == "h8000_0000")
     assert(config.initValue("mtvec") == "h0000_01c0")
     assert(config.functions.privileged)
+    assert(config.formal.arbitraryRegFile)
   }
 }