Bump T1 dependencies and switch to Layer API + LTL API

ipemu/src/TestBench.scala

@@ -27,6 +27,7 @@ class TestBench(generator: SerializableModuleGenerator[T1, T1Parameter])
     extends RawModule
     with ImplicitClock
     with ImplicitReset {
+  layer.enable(layers.Verification)
   val omInstance: Instance[TestBenchOM] = Instantiate(new TestBenchOM)
   val omType:     ClassType = omInstance.toDefinition.getClassType
   @public

nix/t1/_sources/generated.json

@@ -41,7 +41,7 @@
     },
     "chisel": {
         "cargoLocks": null,
-        "date": "2024-08-12",
+        "date": "2024-08-14",
         "extract": null,
         "name": "chisel",
         "passthru": null,
@@ -53,11 +53,11 @@
             "name": null,
             "owner": "chipsalliance",
             "repo": "chisel",
-            "rev": "1d50b782cab542ca8c1822a59f25033e5adfc93f",
-            "sha256": "sha256-Yg8gCwOIYoBb/pehHVBJIzFIXp77qB+D5n4XQaceAtg=",
+            "rev": "af1ef0faad6d1e486d0d5fe8bc2db9ef632365d8",
+            "sha256": "sha256-PexRn7Ys16oEiZRfcr0DpQqLK5zyACKbnSudkxqJF8c=",
             "type": "github"
         },
-        "version": "1d50b782cab542ca8c1822a59f25033e5adfc93f"
+        "version": "af1ef0faad6d1e486d0d5fe8bc2db9ef632365d8"
     },
     "chisel-interface": {
         "cargoLocks": null,

nix/t1/_sources/generated.nix

@@ -27,15 +27,15 @@
   };
   chisel = {
     pname = "chisel";
-    version = "1d50b782cab542ca8c1822a59f25033e5adfc93f";
+    version = "af1ef0faad6d1e486d0d5fe8bc2db9ef632365d8";
     src = fetchFromGitHub {
       owner = "chipsalliance";
       repo = "chisel";
-      rev = "1d50b782cab542ca8c1822a59f25033e5adfc93f";
+      rev = "af1ef0faad6d1e486d0d5fe8bc2db9ef632365d8";
       fetchSubmodules = false;
-      sha256 = "sha256-Yg8gCwOIYoBb/pehHVBJIzFIXp77qB+D5n4XQaceAtg=";
+      sha256 = "sha256-PexRn7Ys16oEiZRfcr0DpQqLK5zyACKbnSudkxqJF8c=";
     };
-    date = "2024-08-12";
+    date = "2024-08-14";
   };
   chisel-interface = {
     pname = "chisel-interface";

nix/t1/rtl.nix

@@ -22,13 +22,11 @@ stdenvNoCC.mkDerivation {
     firtool ${mlirbc}/${mlirbc.elaborateTarget}-${mlirbc.elaborateConfig}-lowered.mlirbc \
       -o $out ${mfcArgs}
   '' + lib.optionalString fixupFilelist ''
-    # For ipemu, there are also some manually generated system verilog file for test bench.
-    # Those files are now recorded in a individual file list.
-    # However, verilator still expect on "filelist.f" file to record all the system verilog file.
-    # Below is a fix that concat them into one file to make verilator happy.
+    # FIXME: https://github.com/llvm/circt/pull/7543
     echo "Fixing generated filelist.f"
-    cp $out/filelist.f original.f
-    cat $out/firrtl_black_box_resource_files.f original.f > $out/filelist.f
+    pushd $out
+    find . -mindepth 1 -name '*.sv' -type f > $out/filelist.f
+    popd
   '';
 
   meta.description = "All the elaborated system verilog files for ${mlirbc.elaborateTarget} with ${mlirbc.elaborateConfig} config.";

nix/t1/verilated.nix

@@ -22,10 +22,12 @@ stdenv.mkDerivation {
     echo "[nix] running verilator"
     verilator \
       ${lib.optionalString enable-trace "--trace-fst"} \
+      --cc \
       --timing \
       --threads 8 \
       -O1 \
-      --cc TestBench
+      -F filelist.f \
+      --top TestBench
 
     echo "[nix] building verilated C lib"
 

t1/src/LaneFloat.scala

@@ -7,6 +7,8 @@ import chisel3.experimental.hierarchy.instantiable
 import chisel3.{UInt, _}
 import chisel3.experimental.{SerializableModule, SerializableModuleParameter}
 import chisel3.util._
+import chisel3.ltl._
+import chisel3.ltl.Sequence._
 import hardfloat._
 import org.chipsalliance.t1.rtl.decoder.{BoolField, Decoder}
 
@@ -162,7 +164,7 @@ class LaneFloat(val parameter: LaneFloatParam) extends VFUModule(parameter) with
   val hasNaN = raw0.isNaN ||  raw1.isNaN
   val differentZeros = compareModule.io.eq && (request.src(1)(31) ^ request.src(0)(31))
 
-  assert(!unitSeleOH(2) || (uop === "b0001".U || uop === "b0000".U || uop === "b0010".U || uop === "b0011".U || uop === "b0100".U || uop === "b0101".U || uop === "b1000".U || uop === "b1100".U))
+  AssertProperty(BoolSequence(!unitSeleOH(2) || (uop === "b0001".U || uop === "b0000".U || uop === "b0010".U || uop === "b0011".U || uop === "b0100".U || uop === "b0101".U || uop === "b1000".U || uop === "b1100".U)))
   compareResult := Mux(uop === BitPat("b1?00") && hasNaN ,compareNaN,
     Mux(uop === BitPat("b1?00"), Mux((!uop(2) && compareModule.io.lt) || (uop(2) && compareModule.io.gt) || (differentZeros && (uop(2) ^ request.src(1)(31))), request.src(1), request.src(0)),
      Mux(uop === "b0011".U, compareModule.io.lt || compareModule.io.eq,

t1/src/T1.scala

@@ -327,7 +327,7 @@ class T1Interface(parameter: T1Parameter) extends Record {
       "highBandwidthLoadStorePort" -> new AXI4RWIrrevocable(parameter.axi4BundleParameter),
       "indexedLoadStorePort" -> new AXI4RWIrrevocable(parameter.axi4BundleParameter.copy(dataWidth=32)),
       "om" -> Output(Property[AnyClassType]()),
-      "t1Probe" -> Output(Probe(new T1Probe(parameter))),
+      "t1Probe" -> Output(Probe(new T1Probe(parameter), layers.Verification)),
     ) 
   )
 }
@@ -1721,26 +1721,27 @@ class T1(val parameter: T1Parameter)
   // don't care有可能会导致先读后写失败
   maskUnitReadVec.foreach(_.bits.instructionIndex := slots.last.record.instructionIndex)
 
-  /**
-    * Probes
-    */
-  val probeWire = Wire(new T1Probe(parameter))
-  define(io.t1Probe, ProbeValue(probeWire))
-  probeWire.instructionCounter := instructionCounter
-  probeWire.instructionIssue := requestRegDequeue.fire
-  probeWire.issueTag := requestReg.bits.instructionIndex
-  probeWire.retireValid := retire
-  // maskUnitWrite maskUnitWriteReady
-  probeWire.writeQueueEnq.valid := maskUnitWrite.valid && maskUnitWriteReady
-  probeWire.writeQueueEnq.bits := maskUnitWrite.bits.instructionIndex
-  probeWire.writeQueueEnqMask := maskUnitWrite.bits.mask
-  probeWire.instructionValid := maskAnd(
-    !slots.last.state.sMaskUnitExecution && !slots.last.state.idle,
-    indexToOH(slots.last.record.instructionIndex, parameter.chainingSize * 2)).asUInt
-  probeWire.responseCounter := responseCounter
-  probeWire.laneProbes.zip(laneVec).foreach { case (p, l) => p := probe.read(l.laneProbe) }
-  probeWire.lsuProbe := probe.read(lsu.lsuProbe)
-
+  layer.block(layers.Verification) {
+    /**
+      * Probes
+      */
+    val probeWire = Wire(new T1Probe(parameter))
+    define(io.t1Probe, ProbeValue(probeWire))
+    probeWire.instructionCounter := instructionCounter
+    probeWire.instructionIssue := requestRegDequeue.fire
+    probeWire.issueTag := requestReg.bits.instructionIndex
+    probeWire.retireValid := retire
+    // maskUnitWrite maskUnitWriteReady
+    probeWire.writeQueueEnq.valid := maskUnitWrite.valid && maskUnitWriteReady
+    probeWire.writeQueueEnq.bits := maskUnitWrite.bits.instructionIndex
+    probeWire.writeQueueEnqMask := maskUnitWrite.bits.mask
+    probeWire.instructionValid := maskAnd(
+      !slots.last.state.sMaskUnitExecution && !slots.last.state.idle,
+      indexToOH(slots.last.record.instructionIndex, parameter.chainingSize * 2)).asUInt
+    probeWire.responseCounter := responseCounter
+    probeWire.laneProbes.zip(laneVec).foreach { case (p, l) => p := probe.read(l.laneProbe) }
+    probeWire.lsuProbe := probe.read(lsu.lsuProbe)
+  }
 
   // new V Request from core
   // val requestValidProbe: Bool = IO(Output(Probe(Bool())))

t1/src/laneStage/LaneExecutionBridge.scala

@@ -7,6 +7,8 @@ import chisel3._
 import chisel3.experimental.hierarchy.{instantiable, public}
 import chisel3.util._
 import chisel3.util.experimental.decode.DecodeBundle
+import chisel3.ltl._
+import chisel3.ltl.Sequence._
 import org.chipsalliance.t1.rtl.{CSRInterface, ExecutionUnitRecord, LaneParameter, SlotRequestToVFU, VFUResponseToSlot, cutUInt, getExecuteUnitTag}
 import org.chipsalliance.t1.rtl.decoder.Decoder
 
@@ -318,7 +320,7 @@ class LaneExecutionBridge(parameter: LaneParameter, isLastSlot: Boolean, slotInd
       flow = true
     )
   )
-  assert(!vfuRequest.fire || recordQueue.io.enq.ready)
+  AssertProperty(BoolSequence(!vfuRequest.fire || recordQueue.io.enq.ready))
   val enqNotExecute: Bool = executionRecord.decodeResult(Decoder.dontNeedExecuteInLane)
   recordQueueReadyForNoExecute := enqNotExecute && recordQueue.io.enq.ready
   recordQueue.io.enq.valid := executionRecordValid && (vfuRequest.ready || enqNotExecute)
@@ -552,7 +554,7 @@ class LaneExecutionBridge(parameter: LaneParameter, isLastSlot: Boolean, slotInd
       ((dataResponse.valid && reduceReady &&
         (!doubleExecutionInQueue || recordQueue.io.deq.bits.executeIndex)) ||
         recordNotExecute)) || reduceLastResponse
-  assert(!queue.io.enq.valid || queue.io.enq.ready)
+  AssertProperty(BoolSequence(!queue.io.enq.valid || queue.io.enq.ready))
   dequeue <> queue.io.deq
   updateMaskResult.foreach(_ :=
     (!recordQueue.io.deq.bits.sSendResponse.get && queue.io.enq.fire) ||

t1/src/laneStage/LaneStage1.scala

@@ -7,6 +7,8 @@ import chisel3._
 import chisel3.experimental.hierarchy.{Instance, Instantiate, instantiable, public}
 import chisel3.probe.{Probe, ProbeValue, define}
 import chisel3.util._
+import chisel3.ltl._
+import chisel3.ltl.Sequence._
 import chisel3.util.experimental.decode.DecodeBundle
 import org.chipsalliance.t1.rtl.decoder.Decoder
 import org.chipsalliance.t1.rtl.lane.{CrossReadUnit, LaneState, VrfReadPipe}
@@ -338,7 +340,7 @@ class LaneStage1(parameter: LaneParameter, isLastSlot: Boolean) extends Module {
 
     // data group
     dataGroupQueue.io.enq.valid := enqueue.fire && enqueue.bits.decodeResult(Decoder.crossRead)
-    assert(dataGroupQueue.io.enq.ready || !dataGroupQueue.io.enq.valid)
+    AssertProperty(BoolSequence(dataGroupQueue.io.enq.ready || !dataGroupQueue.io.enq.valid))
     dataGroupQueue.io.enq.bits := enqueue.bits.groupCounter
     dataGroupQueue.io.deq.ready := crossReadUnit.dataInputLSB.fire
     dequeue.bits.readBusDequeueGroup.get := crossReadUnitOp.get.currentGroup
@@ -385,43 +387,45 @@ class LaneStage1(parameter: LaneParameter, isLastSlot: Boolean) extends Module {
   stageValid := pipeQueue.io.deq.valid
   val stageFinish = !stageValid
 
+  // TODO: gather these logic into a Probe Bundle
   @public
-  val dequeueReadyProbe = IO(Output(Probe(Bool())))
+  val dequeueReadyProbe = IO(Output(Probe(Bool(), layers.Verification)))
   @public
-  val dequeueValidProbe = IO(Output(Probe(Bool())))
+  val dequeueValidProbe = IO(Output(Probe(Bool(), layers.Verification)))
   @public
-  val hasDataOccupiedProbe = IO(Output(Probe(Bool())))
+  val hasDataOccupiedProbe = IO(Output(Probe(Bool(), layers.Verification)))
   @public
-  val stageFinishProbe = IO(Output(Probe(Bool())))
+  val stageFinishProbe = IO(Output(Probe(Bool(), layers.Verification)))
   @public
-  val readFinishProbe = Option.when(isLastSlot)(IO(Output(Probe(Bool()))))
+  val readFinishProbe = Option.when(isLastSlot)(IO(Output(Probe(Bool(), layers.Verification))))
   @public
-  val sSendCrossReadResultLSBProbe = Option.when(isLastSlot)(IO(Output(Probe(Bool()))))
+  val sSendCrossReadResultLSBProbe = Option.when(isLastSlot)(IO(Output(Probe(Bool(), layers.Verification))))
   @public
-  val sSendCrossReadResultMSBProbe = Option.when(isLastSlot)(IO(Output(Probe(Bool()))))
+  val sSendCrossReadResultMSBProbe = Option.when(isLastSlot)(IO(Output(Probe(Bool(), layers.Verification))))
   @public
-  val wCrossReadLSBProbe = Option.when(isLastSlot)(IO(Output(Probe(Bool()))))
+  val wCrossReadLSBProbe = Option.when(isLastSlot)(IO(Output(Probe(Bool(), layers.Verification))))
   @public
-  val wCrossReadMSBProbe = Option.when(isLastSlot)(IO(Output(Probe(Bool()))))
+  val wCrossReadMSBProbe = Option.when(isLastSlot)(IO(Output(Probe(Bool(), layers.Verification))))
   @public
-  val vrfReadRequestProbe: Seq[(Bool, Bool)] = Seq.fill(3)((IO(Output(Probe(Bool()))),IO(Output(Probe(Bool())))))
-
-
-  define(dequeueReadyProbe, ProbeValue(dequeue.ready))
-  define(dequeueValidProbe, ProbeValue(dequeue.valid))
-  define(hasDataOccupiedProbe, ProbeValue(stageValid))
-  define(stageFinishProbe, ProbeValue(stageFinish))
-
-  if (isLastSlot) {
-    readFinishProbe.foreach(p => define(p, ProbeValue(dataQueueVs2.io.deq.valid)))
-    sSendCrossReadResultLSBProbe.foreach(p => define(p, ProbeValue(crossReadUnitOp.get.crossWriteState.sSendCrossReadResultLSB)))
-    sSendCrossReadResultMSBProbe.foreach(p => define(p, ProbeValue(crossReadUnitOp.get.crossWriteState.sSendCrossReadResultMSB)))
-    wCrossReadLSBProbe.foreach(p => define(p, ProbeValue(crossReadUnitOp.get.crossWriteState.wCrossReadLSB)))
-    wCrossReadMSBProbe.foreach(p => define(p, ProbeValue(crossReadUnitOp.get.crossWriteState.wCrossReadMSB)))
-  }
+  val vrfReadRequestProbe: Seq[(Bool, Bool)] = Seq.fill(3)((IO(Output(Probe(Bool(), layers.Verification))),IO(Output(Probe(Bool(), layers.Verification)))))
+
+  layer.block(layers.Verification) {
+    define(dequeueReadyProbe, ProbeValue(dequeue.ready))
+    define(dequeueValidProbe, ProbeValue(dequeue.valid))
+    define(hasDataOccupiedProbe, ProbeValue(stageValid))
+    define(stageFinishProbe, ProbeValue(stageFinish))
+
+    if (isLastSlot) {
+      readFinishProbe.foreach(p => define(p, ProbeValue(dataQueueVs2.io.deq.valid)))
+      sSendCrossReadResultLSBProbe.foreach(p => define(p, ProbeValue(crossReadUnitOp.get.crossWriteState.sSendCrossReadResultLSB)))
+      sSendCrossReadResultMSBProbe.foreach(p => define(p, ProbeValue(crossReadUnitOp.get.crossWriteState.sSendCrossReadResultMSB)))
+      wCrossReadLSBProbe.foreach(p => define(p, ProbeValue(crossReadUnitOp.get.crossWriteState.wCrossReadLSB)))
+      wCrossReadMSBProbe.foreach(p => define(p, ProbeValue(crossReadUnitOp.get.crossWriteState.wCrossReadMSB)))
+    }
 
-  vrfReadRequestProbe.zipWithIndex.foreach { case((ready, valid), i) =>
-    define(ready, ProbeValue(vrfReadRequest(i).ready))
-    define(valid, ProbeValue(vrfReadRequest(i).valid))
+    vrfReadRequestProbe.zipWithIndex.foreach { case ((ready, valid), i) =>
+      define(ready, ProbeValue(vrfReadRequest(i).ready))
+      define(valid, ProbeValue(vrfReadRequest(i).valid))
+    }
   }
 }

t1/src/laneStage/VrfReadPipe.scala

@@ -6,6 +6,9 @@ package org.chipsalliance.t1.rtl.lane
 import chisel3._
 import chisel3.experimental.hierarchy.{instantiable, public}
 import chisel3.util._
+import chisel3.ltl._
+import chisel3.ltl.Sequence._
+
 import org.chipsalliance.t1.rtl.{LaneParameter, VRFReadQueueEntry, VRFReadRequest}
 
 @instantiable
@@ -66,15 +69,15 @@ class VrfReadPipe(parameter: LaneParameter, arbitrate: Boolean = false) extends
 
   dataQueue.io.enq.valid := enqFirePipe.valid && enqFirePipe.bits
   dataQueue.io.enq.bits := vrfReadResult
-  assert(!dataQueue.io.enq.valid || dataQueue.io.enq.ready, "queue overflow")
+  AssertProperty(BoolSequence(!dataQueue.io.enq.valid || dataQueue.io.enq.ready))
   dequeue.valid := dataQueue.io.deq.valid
   dequeue.bits := dataQueue.io.deq.bits
   dataQueue.io.deq.ready := dequeue.ready
 
   contenderDataQueue.foreach { queue =>
     queue.io.enq.valid := enqFirePipe.valid && !enqFirePipe.bits
     queue.io.enq.bits := vrfReadResult
-    assert(!queue.io.enq.valid || queue.io.enq.ready, "queue overflow")
+    AssertProperty(BoolSequence(!queue.io.enq.valid || queue.io.enq.ready))
     contenderDequeue.get.valid := queue.io.deq.valid
     contenderDequeue.get.bits := queue.io.deq.bits
     queue.io.deq.ready := contenderDequeue.get.ready

t1/src/lsu/LSU.scala

@@ -246,9 +246,7 @@ class LSU(param: LSUParameter) extends Module {
   )
 
   @public
-  val lsuProbe = IO(Output(Probe(new LSUProbe(param))))
-  val probeWire = Wire(new LSUProbe(param))
-  define(lsuProbe, ProbeValue(probeWire))
+  val lsuProbe = IO(Output(Probe(new LSUProbe(param), layers.Verification)))
 
   // read vrf
   val otherTryReadVrf: UInt = Mux(otherUnit.vrfReadDataPorts.valid, otherUnit.status.targetLane, 0.U)
@@ -275,26 +273,31 @@ class LSU(param: LSUParameter) extends Module {
     write.io.enq.bits.data := Mux(otherTryToWrite(index), otherUnit.vrfWritePort.bits, loadUnit.vrfWritePort(index).bits)
     write.io.enq.bits.targetLane := (BigInt(1) << index).U
     loadUnit.vrfWritePort(index).ready := write.io.enq.ready && !otherTryToWrite(index)
+  }
 
-    // probes
-    probeWire.slots(index).dataVd := write.io.enq.bits.data.vd
-    probeWire.slots(index).dataOffset := write.io.enq.bits.data.offset
-    probeWire.slots(index).dataMask := write.io.enq.bits.data.mask
-    probeWire.slots(index).dataData := write.io.enq.bits.data.data
-    probeWire.slots(index).dataInstruction := write.io.enq.bits.data.instructionIndex
-    probeWire.slots(index).writeValid := write.io.enq.valid
-    probeWire.slots(index).targetLane := OHToUInt(write.io.enq.bits.targetLane)
+  layer.block(layers.Verification) {
+    val probeWire = Wire(new LSUProbe(param))
+    define(lsuProbe, ProbeValue(probeWire))
+    writeQueueVec.zipWithIndex.foreach { case (write, index) =>
+      probeWire.slots(index).dataVd := write.io.enq.bits.data.vd
+      probeWire.slots(index).dataOffset := write.io.enq.bits.data.offset
+      probeWire.slots(index).dataMask := write.io.enq.bits.data.mask
+      probeWire.slots(index).dataData := write.io.enq.bits.data.data
+      probeWire.slots(index).dataInstruction := write.io.enq.bits.data.instructionIndex
+      probeWire.slots(index).writeValid := write.io.enq.valid
+      probeWire.slots(index).targetLane := OHToUInt(write.io.enq.bits.targetLane)
+    }
+    probeWire.reqEnq := reqEnq.asUInt
+
+    probeWire.storeUnitProbe := probe.read(storeUnit.probe)
+    probeWire.otherUnitProbe := probe.read(otherUnit.probe)
+    probeWire.lsuInstructionValid :=
+      // The load unit becomes idle when it writes vrf for the last time.
+      maskAnd(!loadUnit.status.idle || VecInit(loadUnit.vrfWritePort.map(_.valid)).asUInt.orR,
+        indexToOH(loadUnit.status.instructionIndex, 2 * param.chainingSize)).asUInt |
+        maskAnd(!storeUnit.status.idle, indexToOH(storeUnit.status.instructionIndex, 2 * param.chainingSize)).asUInt |
+        maskAnd(!otherUnit.status.idle, indexToOH(otherUnit.status.instructionIndex, 2 * param.chainingSize)).asUInt
   }
-  probeWire.reqEnq := reqEnq.asUInt
-
-  probeWire.storeUnitProbe := probe.read(storeUnit.probe)
-  probeWire.otherUnitProbe := probe.read(otherUnit.probe)
-  probeWire.lsuInstructionValid :=
-    // The load unit becomes idle when it writes vrf for the last time.
-    maskAnd(!loadUnit.status.idle || VecInit(loadUnit.vrfWritePort.map(_.valid)).asUInt.orR,
-      indexToOH(loadUnit.status.instructionIndex, 2 * param.chainingSize)).asUInt |
-      maskAnd(!storeUnit.status.idle, indexToOH(storeUnit.status.instructionIndex, 2 * param.chainingSize)).asUInt |
-      maskAnd(!otherUnit.status.idle, indexToOH(otherUnit.status.instructionIndex, 2 * param.chainingSize)).asUInt
 
   vrfWritePort.zip(writeQueueVec).foreach { case (p, q) =>
     p.valid := q.io.deq.valid