[rtl] switch assert to use LTL

t1/src/Lane.scala

@@ -6,6 +6,8 @@ package org.chipsalliance.t1.rtl
 import chisel3._
 import chisel3.experimental.hierarchy._
 import chisel3.experimental._
+import chisel3.ltl._
+import chisel3.ltl.Sequence._
 import chisel3.probe.{Probe, ProbeValue, define}
 import chisel3.properties.{AnyClassType, Class, ClassType, Path, Property}
 import chisel3.util._
@@ -689,7 +691,7 @@ class Lane(val parameter: LaneParameter) extends Module with SerializableModule[
         queue.io.enq.valid := readPort.enq.valid
         queue.io.enq.bits := readPort.enq.bits
         readPort.enqRelease := queue.io.deq.fire
-        assert(queue.io.enq.ready || !readPort.enq.valid)
+        AssertProperty(BoolSequence(queue.io.enq.ready || !readPort.enq.valid))
         // dequeue to cross read unit
         stage1.readBusDequeue.get(portIndex) <> queue.io.deq
       }
@@ -758,7 +760,7 @@ class Lane(val parameter: LaneParameter) extends Module with SerializableModule[
       UIntToOH(executionUnit.responseIndex(parameter.instructionIndexBits - 2, 0)),
       0.U(parameter.chainingSize.W)
     )
-    when(executionUnit.dequeue.valid)(assert(stage2.dequeue.valid))
+    AssertProperty(BoolSequence(!executionUnit.dequeue.valid || stage2.dequeue.valid))
     stage3.enqueue.valid := executionUnit.dequeue.valid
     executionUnit.dequeue.ready := stage3.enqueue.ready
     stage2.dequeue.ready := executionUnit.dequeue.fire

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/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

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/SimpleAccessUnit.scala

@@ -7,6 +7,8 @@ import chisel3._
 import chisel3.experimental.hierarchy.{instantiable, public}
 import chisel3.probe._
 import chisel3.util._
+import chisel3.ltl._
+import chisel3.ltl.Sequence._
 import org.chipsalliance.t1.rtl._
 
 /**
@@ -824,7 +826,7 @@ class SimpleAccessUnit(param: MSHRParam) extends Module  with LSUPublic {
   s1EnqQueue.io.enq.bits.readData := DontCare
   // pipe read data
   s1EnqDataQueue.io.enq.valid := vrfReadResults.valid
-  assert(s1EnqDataQueue.io.enq.ready || !vrfReadResults.valid, "read queue in simple access ")
+  AssertProperty(BoolSequence(s1EnqDataQueue.io.enq.ready || !vrfReadResults.valid))
   s1EnqDataQueue.io.enq.bits := vrfReadResults.bits
 
   s1Wire.address := s1EnqQueue.io.deq.bits.address

t1/src/lsu/StoreUnit.scala

@@ -7,6 +7,8 @@ import chisel3._
 import chisel3.experimental.hierarchy.{instantiable, public}
 import chisel3.util._
 import chisel3.probe._
+import chisel3.ltl._
+import chisel3.ltl.Sequence._
 import org.chipsalliance.t1.rtl.{EmptyBundle, VRFReadRequest, cutUInt, multiShifter}
 
 class cacheLineEnqueueBundle(param: MSHRParam) extends Bundle {
@@ -117,8 +119,7 @@ class StoreUnit(param: MSHRParam) extends StrideBase(param) with LSUPublic {
     // latency queue enq
     queue.io.enq.valid := readResultFire
     queue.io.enq.bits := vrfReadResults(laneIndex)
-    assert(!queue.io.enq.valid || queue.io.enq.ready)
-
+    AssertProperty(BoolSequence(!queue.io.enq.valid || queue.io.enq.ready))
     vrfReadQueueVec(laneIndex).io.enq <> queue.io.deq
     stageValid || RegNext(readPort.fire)
   }.reduce(_ || _)

t1/src/vrf/VRF.scala

@@ -8,6 +8,8 @@ import chisel3.experimental.hierarchy.{Instantiate, instantiable, public}
 import chisel3.experimental.{SerializableModule, SerializableModuleParameter}
 import chisel3.probe.{Probe, ProbeValue, define}
 import chisel3.util._
+import chisel3.ltl._
+import chisel3.ltl.Sequence._
 import org.chipsalliance.t1.rtl.{LSUWriteCheck, VRFReadPipe, VRFReadRequest, VRFWriteReport, VRFWriteRequest, ffo, instIndexL, instIndexLE, ohCheck}
 
 sealed trait RamType
@@ -391,8 +393,7 @@ class VRF(val parameter: VRFParam) extends Module with SerializableModule[VRFPar
         rf.readwritePorts.last.enable := ramWriteValid || firstReadPipe(bank).valid
         rf.readwritePorts.last.isWrite := ramWriteValid
         rf.readwritePorts.last.writeData := writeData
-        assert(!(writeValid && firstReadPipe(bank).valid), "port conflict")
-
+        AssertProperty(BoolSequence(!(writeValid && firstReadPipe(bank).valid)))
         readResultF(bank) := rf.readwritePorts.head.readData
         readResultS(bank) := DontCare
       case RamType.p0rp1w =>
@@ -432,7 +433,7 @@ class VRF(val parameter: VRFParam) extends Module with SerializableModule[VRFPar
         rf.readwritePorts.last.enable := ramWriteValid || secondReadPipe(bank).valid
         rf.readwritePorts.last.isWrite := ramWriteValid
         rf.readwritePorts.last.writeData := writeData
-        assert(!(writeValid && secondReadPipe(bank).valid), "port conflict")
+        AssertProperty(BoolSequence(!(writeValid && secondReadPipe(bank).valid)))
     }
 
     rf