Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[rtl] switch assert to use LTL #736

Closed
wants to merge 1 commit into from
Closed

[rtl] switch assert to use LTL #736

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 5 additions & 3 deletions t1/src/Lane.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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._
Expand Down Expand Up @@ -691,7 +693,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
}
Expand Down Expand Up @@ -760,7 +762,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
Expand Down Expand Up @@ -850,7 +852,7 @@ class Lane(val parameter: LaneParameter) extends Module with SerializableModule[
queue.io.enq.bits.last := DontCare
queue.io.enq.bits.instructionIndex := port.enq.bits.instructionIndex
queue.io.enq.bits.mask := FillInterleaved(2, port.enq.bits.mask)
assert(queue.io.enq.ready || !port.enq.valid)
AssertProperty(BoolSequence(queue.io.enq.ready || !port.enq.valid))
port.enqRelease := queue.io.deq.fire
}

Expand Down
4 changes: 3 additions & 1 deletion t1/src/LaneFloat.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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}

Expand Down Expand Up @@ -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,
Expand Down
6 changes: 4 additions & 2 deletions t1/src/laneStage/LaneExecutionBridge.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -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) ||
Expand Down
4 changes: 3 additions & 1 deletion t1/src/laneStage/LaneStage1.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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}
Expand Down Expand Up @@ -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
Expand Down
7 changes: 5 additions & 2 deletions t1/src/laneStage/VrfReadPipe.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down
4 changes: 3 additions & 1 deletion t1/src/lsu/SimpleAccessUnit.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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._

/**
Expand Down Expand Up @@ -826,7 +828,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
Expand Down
5 changes: 3 additions & 2 deletions t1/src/lsu/StoreUnit.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 {
Expand Down Expand Up @@ -119,8 +121,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(_ || _)
Expand Down
7 changes: 4 additions & 3 deletions t1/src/vrf/VRF.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -388,8 +390,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 =>
Expand Down Expand Up @@ -429,7 +430,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
Expand Down