Fix exception handle in branch insts and add ArbitraryRegFile (#23)

* fix: fix the exception handle in Branch insts

* feat: add GenerateArbitraryRegFile func and update to 1.3-SNAPSHOT

* feat: add ArbitraryRegFile in RVConfig

* refactor: rename functions

* ci: setup BtorMC in Test

---------

Co-authored-by: liuyic00 <[email protected]>

.github/workflows/Test.yml

@@ -15,5 +15,7 @@ jobs:
           java-version: [email protected]
       - name: Cache Scala
         uses: coursier/cache-action@v5
+      - name: Setup BtorMC
+        uses: SeddonShen/[email protected]
       - name: SBT Test
         run: sbt test

build.sbt

@@ -2,7 +2,7 @@
 lazy val useCHA: Boolean =
   sys.props.getOrElse("CHA", "false").toLowerCase == "true"
 
-ThisBuild / version      := { if (useCHA) "1.1-cha-SNAPSHOT" else "1.1-SNAPSHOT" }
+ThisBuild / version      := { if (useCHA) "1.3-cha-SNAPSHOT" else "1.3-SNAPSHOT" }
 ThisBuild / organization := "cn.ac.ios.tis"
 ThisBuild / scalaVersion := "2.12.17"
 // Use Scala2.13 with ChiselTest0.6.0 will cause efficiency issues in the

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 gen(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,6 +20,7 @@ object ConnectCheckerResult extends ConnectHelper {
   val uniqueIdEvent: String = "ConnectCheckerResult_UniqueIdEvent"
   val uniqueIdDTLB: String  = "ConnectCheckerResult_UniqueIdDTLB"
   val uniqueIdITLB: String  = "ConnectCheckerResult_UniqueIdITLB"
+
   def setRegSource(regVec: Vec[UInt]) = {
     BoringUtils.addSource(regVec, uniqueIdReg)
   }
@@ -92,8 +93,13 @@ object ConnectCheckerResult extends ConnectHelper {
     event
   }
 
-  def setChecker(checker: CheckerWithResult, memDelay: Int = 0)(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)

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

@@ -8,6 +8,8 @@ import spec.instset.csr.CSR
 import spec.instset.csr.EventSig
 import spec.instset.csr.SatpStruct
 
+import rvspeccore.checker.ArbitraryRegFile
+
 abstract class BaseCore()(implicit val config: RVConfig) extends Module {
   implicit val XLEN: Int = config.XLEN
 
@@ -75,7 +77,10 @@ object State {
   def wireInit()(implicit XLEN: Int, config: RVConfig): State = {
     val state = Wire(new State)
 
-    state.reg := Seq.fill(32)(0.U(XLEN.W))
+    state.reg := {
+      if (config.formal.arbitraryRegFile) ArbitraryRegFile.gen
+      else Seq.fill(32)(0.U(XLEN.W))
+    }
     state.pc  := config.initValue.getOrElse("pc", "h8000_0000").U(XLEN.W)
     state.csr := CSR.wireInit()
 

src/main/scala/rvspeccore/core/spec/instset/IBase.scala

@@ -245,11 +245,55 @@ trait IBase extends BaseCore with CommonDecode with IBaseInsts with ExceptionSup
       }
     }
     // BLT[U]
-    when(BLT(inst))  { decodeB; when(now.reg(rs1).asSInt < now.reg(rs2).asSInt) { global_data.setpc := true.B; next.pc := now.pc + imm } }
-    when(BLTU(inst)) { decodeB; when(now.reg(rs1) < now.reg(rs2)) { global_data.setpc := true.B; next.pc := now.pc + imm } }
+    when(BLT(inst))  {
+      decodeB;
+      when(now.reg(rs1).asSInt < now.reg(rs2).asSInt) {
+        when(addrAligned(getfetchSize(), now.pc + imm)){
+          global_data.setpc := true.B;
+          next.pc := now.pc + imm
+        }.otherwise {
+          next.csr.mtval := now.pc + imm;
+          raiseException(MExceptionCode.instructionAddressMisaligned)
+        }
+      }
+    }
+    when(BLTU(inst)) {
+      decodeB;
+      when(now.reg(rs1) < now.reg(rs2)) {
+        when(addrAligned(getfetchSize(), now.pc + imm)){
+          global_data.setpc := true.B;
+          next.pc := now.pc + imm
+        }.otherwise {
+          next.csr.mtval := now.pc + imm;
+          raiseException(MExceptionCode.instructionAddressMisaligned)
+        }
+      }
+    }
     // BGE[U]
-    when(BGE(inst))  { decodeB; when(now.reg(rs1).asSInt >= now.reg(rs2).asSInt) { global_data.setpc := true.B; next.pc := now.pc + imm } }
-    when(BGEU(inst)) { decodeB; when(now.reg(rs1) >= now.reg(rs2)) { global_data.setpc := true.B; next.pc := now.pc + imm } }
+    when(BGE(inst))  {
+      decodeB;
+      when(now.reg(rs1).asSInt >= now.reg(rs2).asSInt) {
+        when(addrAligned(getfetchSize(), now.pc + imm)){
+          global_data.setpc := true.B;
+          next.pc := now.pc + imm
+        }.otherwise {
+          next.csr.mtval := now.pc + imm;
+          raiseException(MExceptionCode.instructionAddressMisaligned)
+        }
+      }
+    }
+    when(BGEU(inst)) {
+      decodeB;
+      when(now.reg(rs1) >= now.reg(rs2)) {
+        when(addrAligned(getfetchSize(), now.pc + imm)){
+          global_data.setpc := true.B;
+          next.pc := now.pc + imm
+        }.otherwise {
+          next.csr.mtval := now.pc + imm;
+          raiseException(MExceptionCode.instructionAddressMisaligned)
+        }
+      }
+    }
     // - 2.6 Load and Store Instructions
     // LOAD
     // TODO: LBU and LHU ?

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.gen
+  ArbitraryRegFile.init
+
+  if (hasBug) {
+    // this assertion should fail because the rf(1) is arbitrary, could be not 0.U
+    // will print a "Assertion failed"
+    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] {
+      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)
   }
 }