From a94000bca066cbc0cd618e8315f15d9a37378a67 Mon Sep 17 00:00:00 2001 From: liuyic00 Date: Thu, 22 Aug 2024 11:02:06 +0800 Subject: [PATCH] feat: add ArbitraryRegFile in RVConfig --- .../checker/ArbitraryGenerater.scala | 22 +++++++++++++ .../rvspeccore/checker/ConnectHelper.scala | 13 ++++---- .../rvspeccore/checker/RandomHelper.scala | 17 ---------- src/main/scala/rvspeccore/core/RVConfig.scala | 7 ++++ .../scala/rvspeccore/core/RiscvCore.scala | 11 ++++--- .../checker/ArbitraryGeneraterSpec.scala | 32 +++++++++++++++++++ .../scala/rvspeccore/core/RVConfigSpec.scala | 4 ++- 7 files changed, 76 insertions(+), 30 deletions(-) create mode 100644 src/main/scala/rvspeccore/checker/ArbitraryGenerater.scala delete mode 100644 src/main/scala/rvspeccore/checker/RandomHelper.scala create mode 100644 src/test/scala/rvspeccore/checker/ArbitraryGeneraterSpec.scala diff --git a/src/main/scala/rvspeccore/checker/ArbitraryGenerater.scala b/src/main/scala/rvspeccore/checker/ArbitraryGenerater.scala new file mode 100644 index 0000000..541adcc --- /dev/null +++ b/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 + } +} diff --git a/src/main/scala/rvspeccore/checker/ConnectHelper.scala b/src/main/scala/rvspeccore/checker/ConnectHelper.scala index 8633ec3..604202d 100644 --- a/src/main/scala/rvspeccore/checker/ConnectHelper.scala +++ b/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 diff --git a/src/main/scala/rvspeccore/checker/RandomHelper.scala b/src/main/scala/rvspeccore/checker/RandomHelper.scala deleted file mode 100644 index 799fec8..0000000 --- a/src/main/scala/rvspeccore/checker/RandomHelper.scala +++ /dev/null @@ -1,17 +0,0 @@ -package rvspeccore.checker - -import chisel3._ -import chisel3.util._ - -import rvspeccore.core.spec - - -object GenerateArbitraryRegFile{ - def apply(implicit XLEN: Int): Vec[UInt] = { - val rf = Wire(Vec(32, UInt(XLEN.W))) - rf.map(_:= DontCare) - rf(0) := 0.U - rf - } -} - diff --git a/src/main/scala/rvspeccore/core/RVConfig.scala b/src/main/scala/rvspeccore/core/RVConfig.scala index 90eef18..2af4416 100644 --- a/src/main/scala/rvspeccore/core/RVConfig.scala +++ b/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") + } } diff --git a/src/main/scala/rvspeccore/core/RiscvCore.scala b/src/main/scala/rvspeccore/core/RiscvCore.scala index 6117de3..0c2f55f 100644 --- a/src/main/scala/rvspeccore/core/RiscvCore.scala +++ b/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() diff --git a/src/test/scala/rvspeccore/checker/ArbitraryGeneraterSpec.scala b/src/test/scala/rvspeccore/checker/ArbitraryGeneraterSpec.scala new file mode 100644 index 0000000..76cf16d --- /dev/null +++ b/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)) + } + } +} diff --git a/src/test/scala/rvspeccore/core/RVConfigSpec.scala b/src/test/scala/rvspeccore/core/RVConfigSpec.scala index 27d9d1b..3c0b928 100644 --- a/src/test/scala/rvspeccore/core/RVConfigSpec.scala +++ b/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) } }