From 9cdd445ff3eede44a07b26f055c5d8387ebf03a7 Mon Sep 17 00:00:00 2001 From: Jiuyang Liu Date: Thu, 22 Aug 2024 01:40:28 +0800 Subject: [PATCH] [rtl] switch assert to use LTL --- t1/src/Lane.scala | 6 ++++-- t1/src/LaneFloat.scala | 4 +++- t1/src/laneStage/LaneExecutionBridge.scala | 6 ++++-- t1/src/laneStage/LaneStage1.scala | 4 +++- t1/src/laneStage/VrfReadPipe.scala | 7 +++++-- t1/src/lsu/SimpleAccessUnit.scala | 4 +++- t1/src/lsu/StoreUnit.scala | 5 +++-- t1/src/vrf/VRF.scala | 7 ++++--- 8 files changed, 29 insertions(+), 14 deletions(-) diff --git a/t1/src/Lane.scala b/t1/src/Lane.scala index bcefeddcc..959fb4108 100644 --- a/t1/src/Lane.scala +++ b/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 diff --git a/t1/src/LaneFloat.scala b/t1/src/LaneFloat.scala index 29e72d91e..f44b480c9 100644 --- a/t1/src/LaneFloat.scala +++ b/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, diff --git a/t1/src/laneStage/LaneExecutionBridge.scala b/t1/src/laneStage/LaneExecutionBridge.scala index cf3cf1c9d..e1ecbcdcc 100644 --- a/t1/src/laneStage/LaneExecutionBridge.scala +++ b/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) || diff --git a/t1/src/laneStage/LaneStage1.scala b/t1/src/laneStage/LaneStage1.scala index e7acab62f..7759cb55e 100644 --- a/t1/src/laneStage/LaneStage1.scala +++ b/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 diff --git a/t1/src/laneStage/VrfReadPipe.scala b/t1/src/laneStage/VrfReadPipe.scala index e7c3b304c..54f8afb88 100644 --- a/t1/src/laneStage/VrfReadPipe.scala +++ b/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,7 +69,7 @@ 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 @@ -74,7 +77,7 @@ class VrfReadPipe(parameter: LaneParameter, arbitrate: Boolean = false) extends 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 diff --git a/t1/src/lsu/SimpleAccessUnit.scala b/t1/src/lsu/SimpleAccessUnit.scala index 51516e6d1..68e7346f0 100644 --- a/t1/src/lsu/SimpleAccessUnit.scala +++ b/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 diff --git a/t1/src/lsu/StoreUnit.scala b/t1/src/lsu/StoreUnit.scala index 96c1cf26c..2841411ec 100644 --- a/t1/src/lsu/StoreUnit.scala +++ b/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(_ || _) diff --git a/t1/src/vrf/VRF.scala b/t1/src/vrf/VRF.scala index 9a39fd638..cbea686da 100644 --- a/t1/src/vrf/VRF.scala +++ b/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