162 lines
5.4 KiB
Scala
162 lines
5.4 KiB
Scala
// See LICENSE.SiFive for license details.
|
|
|
|
package freechips.rocketchip.util.property
|
|
|
|
import Chisel._
|
|
import chisel3.internal.sourceinfo.{SourceInfo, SourceLine}
|
|
import chisel3.util.{ReadyValidIO}
|
|
|
|
sealed abstract class PropertyType(name: String) {
|
|
override def toString: String = name
|
|
}
|
|
|
|
object PropertyType {
|
|
object Assert extends PropertyType("Assert")
|
|
object Assume extends PropertyType("Assume")
|
|
object Cover extends PropertyType("Cover")
|
|
}
|
|
|
|
trait BasePropertyParameters {
|
|
val pType: PropertyType
|
|
val cond: Bool
|
|
val label: String
|
|
val message: String
|
|
}
|
|
|
|
case class CoverPropertyParameters(
|
|
cond: Bool,
|
|
label: String = "",
|
|
message: String = "") extends BasePropertyParameters {
|
|
val pType = PropertyType.Cover
|
|
}
|
|
|
|
abstract class BasePropertyLibrary {
|
|
def generateProperty(prop_param: BasePropertyParameters)(implicit sourceInfo: SourceInfo)
|
|
}
|
|
|
|
class DefaultPropertyLibrary extends BasePropertyLibrary {
|
|
def generateProperty(prop_param: BasePropertyParameters)(implicit sourceInfo: SourceInfo) {
|
|
// default is to do nothing
|
|
Unit
|
|
}
|
|
}
|
|
|
|
abstract class BaseProperty {
|
|
def generateProperties(): Seq[BasePropertyParameters]
|
|
}
|
|
|
|
case class CoverBoolean(cond: Bool, labels: Seq[String]) {
|
|
}
|
|
|
|
// CrossProperty.generateProperties() will generate Boolean crosses for the cond sequence
|
|
// E.g.
|
|
// Cond = [ [A1, A2, A3],
|
|
// [B2],
|
|
// [C1, C2] ]
|
|
// It will generate the following properties
|
|
// [ A1 && B2 && C1,
|
|
// A1 && B2 && C2,
|
|
// A2 && B2 && C1,
|
|
// A2 && B2 && C2,
|
|
// A3 && B2 && C1,
|
|
// A3 && B2 && C2 ]
|
|
// Each of the boolean expression (A1, A2, C1, etc.) have a label associated with it
|
|
// User can exclude a particular cross from being generated by adding it to the exclude list
|
|
// e.g.
|
|
// exclude = [ ["A1_label", "C2_Label"],
|
|
// ["A3_label", "B2_label"] ]
|
|
// will exclude all crosses with those labels, so the new cross list will be
|
|
// [ A1 && B2 && C1,
|
|
// A2 && B2 && C1,
|
|
// A2 && B2 && C2 ]
|
|
|
|
// Each boolean expression can be associated with more than one label
|
|
|
|
class CrossProperty(cond: Seq[Seq[CoverBoolean]], exclude: Seq[Seq[String]], message: String) extends BaseProperty {
|
|
def listProperties(c1: CoverBoolean, c2: Seq[CoverBoolean]): Seq[CoverBoolean] = {
|
|
if (c2.isEmpty) {
|
|
Seq(c1)
|
|
} else {
|
|
c2.map( (c: CoverBoolean) => {
|
|
new CoverBoolean(c1.cond && c.cond, c1.labels ++ c.labels)
|
|
})
|
|
}
|
|
}
|
|
|
|
def crossProperties(cond: Seq[Seq[CoverBoolean]]): Seq[CoverBoolean] = {
|
|
if (cond.isEmpty) {
|
|
Seq()
|
|
} else {
|
|
cond.head.map( (c1: CoverBoolean) => {
|
|
listProperties(c1, crossProperties(cond.tail))
|
|
}).reduce(_ ++ _)
|
|
}
|
|
}
|
|
def inSequence(search: Seq[String], find: Seq[String]): Boolean = {
|
|
if (find.isEmpty) {
|
|
true
|
|
} else {
|
|
find.map( (s:String) => {
|
|
search.contains(s)
|
|
}).reduce( _ && _ )
|
|
}
|
|
}
|
|
def SeqsinSequence(search: Seq[String], find: Seq[Seq[String]]): Boolean = {
|
|
if (find.isEmpty) {
|
|
false
|
|
} else {
|
|
find.map( (s: Seq[String]) => {
|
|
inSequence(search, s)
|
|
}).reduce (_ || _)
|
|
}
|
|
}
|
|
|
|
def generateProperties(): Seq[CoverPropertyParameters] = {
|
|
crossProperties(cond).map( (c: CoverBoolean) => {
|
|
if (!SeqsinSequence(c.labels, exclude)) {
|
|
new CoverPropertyParameters(
|
|
cond = c.cond,
|
|
label = c.labels.reduce( (s1: String, s2: String) => {s1 + "_" + s2} ),
|
|
message = message + " " + c.labels.map("<" + _ + ">").reduce ( (s1: String, s2: String) => { s1 + " X " + s2 }))
|
|
} else {
|
|
new CoverPropertyParameters(
|
|
cond = true.B,
|
|
label = c.labels.reduce( (s1: String, s2: String) => {s1 + "_" + s2} ) + "_EXCLUDE",
|
|
message = message + " " + c.labels.map("<" + _ + ">").reduce ( (s1: String, s2: String) => { s1 + " X " + s2 }))
|
|
}
|
|
})
|
|
}
|
|
|
|
}
|
|
|
|
// The implementation using a setable global is bad, but removes dependence on Parameters
|
|
// This change was made in anticipation of a proper cover library
|
|
object cover {
|
|
private var propLib: BasePropertyLibrary = new DefaultPropertyLibrary
|
|
def setPropLib(lib: BasePropertyLibrary): Unit = this.synchronized {
|
|
propLib = lib
|
|
}
|
|
def apply(cond: Bool)(implicit sourceInfo: SourceInfo): Unit = {
|
|
propLib.generateProperty(CoverPropertyParameters(cond))
|
|
}
|
|
def apply(cond: Bool, label: String)(implicit sourceInfo: SourceInfo): Unit = {
|
|
propLib.generateProperty(CoverPropertyParameters(cond, label))
|
|
}
|
|
def apply(cond: Bool, label: String, message: String)(implicit sourceInfo: SourceInfo): Unit = {
|
|
propLib.generateProperty(CoverPropertyParameters(cond, label, message))
|
|
}
|
|
def apply(prop: BaseProperty)(implicit sourceInfo: SourceInfo): Unit = {
|
|
prop.generateProperties().foreach( (pp: BasePropertyParameters) => {
|
|
if (pp.pType == PropertyType.Cover) {
|
|
propLib.generateProperty(CoverPropertyParameters(pp.cond, pp.label, pp.message))
|
|
}
|
|
})
|
|
}
|
|
def apply[T <: Data](rv: ReadyValidIO[T], label: String, message: String)(implicit sourceInfo: SourceInfo): Unit = {
|
|
apply( rv.valid && rv.ready, label + "_FIRE", message + ": valid and ready")
|
|
apply( rv.valid && !rv.ready, label + "_STALL", message + ": valid and not ready")
|
|
apply(!rv.valid && rv.ready, label + "_IDLE", message + ": not valid and ready")
|
|
apply(!rv.valid && !rv.ready, label + "_FULL", message + ": not valid and not ready")
|
|
}
|
|
}
|