[gg] Put token irrevocability assertions on a switch

This commit is contained in:
David Biancolin 2019-11-04 16:10:48 -08:00
parent 2fd68cfd80
commit 099e9db408
4 changed files with 25 additions and 15 deletions

View File

@ -83,3 +83,8 @@ class F1ConfigWithSnapshot extends Config(new Config((site, here, up) => {
case EnableSnapshot => true
}) ++ new F1Config)
// Turns on all additional synthesizable debug features for checking the
// implementation of the simulator.
class HostDebugFeatures extends Config((site, here, up) => {
case GenerateTokenIrrevocabilityAssertions => true
})

View File

@ -3,7 +3,7 @@
package midas
package core
import freechips.rocketchip.config.Parameters
import freechips.rocketchip.config.{Parameters, Field}
import freechips.rocketchip.unittest._
import freechips.rocketchip.util.{DecoupledHelper}
import freechips.rocketchip.tilelink.LFSR64 // Better than chisel's
@ -15,6 +15,11 @@ import chisel3.experimental.{dontTouch, chiselName, MultiIOModule}
import strober.core.{TraceQueue, TraceMaxLen}
import midas.core.SimUtils.{ChLeafType}
// Generates stateful assertions on the ports of channels to check that token
// irrevocability constraints aren't be violated. Bridges that don not produce
// token streams irrevocably will introduce simulation non-determinism.
case object GenerateTokenIrrevocabilityAssertions extends Field[Boolean](false)
// For now use the convention that clock ratios are set with respect to the transformed RTL
trait IsRationalClockRatio {
def numerator: Int
@ -76,6 +81,8 @@ class PipeChannel[T <: ChLeafType](
}
}
if (p(GenerateTokenIrrevocabilityAssertions)) AssertTokenIrrevocable(io.in, None)
if (p(EnableSnapshot)) {
io.trace <> TraceQueue(tokens.io.deq, io.traceLen)
} else {
@ -85,7 +92,7 @@ class PipeChannel[T <: ChLeafType](
}
object AssertTokenIrrevocable {
def apply(rv: ReadyValidIO[_ <: Data], suggestedName: Option[String])(implicit p: Parameters): Unit = {
def apply(rv: ReadyValidIO[_ <: Data], suggestedName: Option[String]): Unit = {
val prefix = suggestedName match {
case Some(str) => str + ": "
case None => ""
@ -99,7 +106,7 @@ object AssertTokenIrrevocable {
s"${prefix}bits changed without handshake, violating irrevocability")
}
def apply(valid: Bool, bits: Data, ready: Bool, suggestedName: Option[String] = None)(implicit p: Parameters): Unit = {
def apply(valid: Bool, bits: Data, ready: Bool, suggestedName: Option[String] = None): Unit = {
val dummyMod = Module(new Module { val io = IO(Input(Decoupled(bits.cloneType))) })
dummyMod.io.valid := valid
dummyMod.io.bits := bits
@ -151,10 +158,10 @@ class SimReadyValidIO[T <: Data](gen: T) extends Bundle {
val rev = Flipped(new HostReadyValid)
override def cloneType = new SimReadyValidIO(gen).asInstanceOf[this.type]
def fwdIrrevocabilityAssertions(suggestedName: Option[String] = None)(implicit p: Parameters): Unit =
def generateFwdIrrevocabilityAssertions(suggestedName: Option[String] = None): Unit =
AssertTokenIrrevocable(fwd.hValid, Cat(target.valid, target.bits.asUInt), fwd.hReady, suggestedName)
def revIrrevocabilityAssertions(suggestedName: Option[String] = None)(implicit p: Parameters): Unit =
def generateRevIrrevocabilityAssertions(suggestedName: Option[String] = None): Unit =
AssertTokenIrrevocable(rev.hValid, target.ready, rev.hReady, suggestedName)
// Returns two directioned objects driven by this SimReadyValidIO hw instance
@ -280,6 +287,11 @@ class ReadyValidChannel[T <: Data](
deqFwdFired := Mux(targetFire, false.B, deqFwdFired || io.deq.fwd.hReady)
enqRevFired := Mux(targetFire, false.B, enqRevFired || io.enq.rev.hReady)
if (p(GenerateTokenIrrevocabilityAssertions)) {
io.enq.generateFwdIrrevocabilityAssertions()
io.deq.generateRevIrrevocabilityAssertions()
}
io.trace := DontCare
io.trace.bits.valid := false.B
io.trace.valid.valid := false.B

View File

@ -273,9 +273,6 @@ class SimWrapper(chAnnos: Seq[FAMEChannelConnectionAnnotation],
case None => channelPorts.elements(s"${chAnno.globalName}_source") <> channel.io.out
}
AssertTokenIrrevocable(channel.io.in, Some(s"${chAnno.globalName}_in"))
AssertTokenIrrevocable(channel.io.out, Some(s"${chAnno.globalName}_out"))
channel.io.trace.ready := DontCare
channel.io.traceLen := DontCare
channel
@ -339,11 +336,6 @@ class SimWrapper(chAnnos: Seq[FAMEChannelConnectionAnnotation],
})
bindRVChannelDeq(channel.io.deq, deqPortPair)
channel.io.enq.fwdIrrevocabilityAssertions(Some(strippedName))
channel.io.enq.revIrrevocabilityAssertions(Some(strippedName))
channel.io.deq.fwdIrrevocabilityAssertions(Some(strippedName))
channel.io.deq.revIrrevocabilityAssertions(Some(strippedName))
channel.io.trace := DontCare
channel.io.traceLen := DontCare
channel.io.targetReset.bits := false.B

View File

@ -24,12 +24,13 @@ abstract class TutorialSuite(
targetConfigProject = "firesim.midasexamples",
targetConfigs = targetConfigs,
platformConfigProject = "firesim.midasexamples",
platformConfigs = "DefaultF1Config")
platformConfigs = "HostDebugFeatures_DefaultF1Config")
val args = Seq(s"+tracelen=$tracelen") ++ simulationArgs
val commonMakeArgs = Seq(s"TARGET_PROJECT=midasexamples",
s"DESIGN=$targetName",
s"TARGET_CONFIG=${generatorArgs.targetConfigs}")
s"TARGET_CONFIG=${generatorArgs.targetConfigs}",
s"PLATFORM_CONFIG=${generatorArgs.platformConfigs}")
val targetTuple = generatorArgs.tupleName
def run(backend: String,