Add Cross Cover Property Library (#1149)

Add cover points related to memory error to I/D Cache

src/main/scala/rocket/DCache.scala

@@ -654,9 +654,9 @@ class DCacheModule(outer: DCache) extends HellaCacheModule(outer) {
     when (s2_read) { io.cpu.s2_xcpt.ae.ld := true }
   }
 
+  val s2_isSlavePortAccess = s2_req.phys
   if (usingDataScratchpad) {
     require(!usingVM) // therefore, req.phys means this is a slave-port access
-    val s2_isSlavePortAccess = s2_req.phys
     when (s2_isSlavePortAccess) {
       assert(!s2_valid || s2_hit_valid)
       io.cpu.s2_xcpt := 0.U.asTypeOf(io.cpu.s2_xcpt)
@@ -720,8 +720,10 @@ class DCacheModule(outer: DCache) extends HellaCacheModule(outer) {
   metaArb.io.in(5).bits.addr := Cat(io.cpu.req.bits.addr >> untagBits, flushCounter(idxBits-1, 0) << blockOffBits)
   metaArb.io.in(5).bits.way_en := ~UInt(0, nWays)
   metaArb.io.in(5).bits.data := metaArb.io.in(4).bits.data
+
   // Only flush D$ on FENCE.I if some cached executable regions are untracked.
-  if (!edge.manager.managers.forall(m => !m.supportsAcquireT || !m.executable || m.regionType >= RegionType.TRACKED)) {
+  val supports_flush = !edge.manager.managers.forall(m => !m.supportsAcquireT || !m.executable || m.regionType >= RegionType.TRACKED)
+  if (supports_flush) {
     when (tl_out_a.fire() && !s2_uncached) { flushed := false }
     when (flushing) {
       s1_victim_way := flushCounter >> log2Up(nSets)
@@ -757,13 +759,13 @@ class DCacheModule(outer: DCache) extends HellaCacheModule(outer) {
   io.cpu.perf.tlbMiss := io.ptw.req.fire()
 
   // report errors
-  {
   val (data_error, data_error_uncorrectable, data_error_addr) =
     if (usingDataScratchpad) (s2_valid_data_error, s2_data_error_uncorrectable, s2_req.addr) else {
       (tl_out_c.fire() && inWriteback && writeback_data_error,
         writeback_data_uncorrectable,
         tl_out_c.bits.address)
     }
+  {
     val error_addr =
       Mux(metaArb.io.in(1).valid, Cat(metaArb.io.in(1).bits.data.tag, metaArb.io.in(1).bits.addr(untagBits-1, idxLSB)),
           data_error_addr >> idxLSB) << idxLSB
@@ -797,4 +799,44 @@ class DCacheModule(outer: DCache) extends HellaCacheModule(outer) {
     cover(cond, s"DCACHE_$label", "MemorySystem;;" + desc)
   def ccoverNotScratchpad(cond: Bool, label: String, desc: String)(implicit sourceInfo: SourceInfo) =
     if (!usingDataScratchpad) ccover(cond, label, desc)
+
+  if (usingDataScratchpad) {
+    val data_error_cover = Seq(
+      CoverBoolean(!data_error, Seq("no_data_error")),
+      CoverBoolean(data_error && !data_error_uncorrectable, Seq("correctable_data_error")),
+      CoverBoolean(data_error && data_error_uncorrectable, Seq("uncorrectable_data_error")))
+    val request_source = Seq(
+      CoverBoolean(s2_isSlavePortAccess, Seq("from_TL")),
+      CoverBoolean(!s2_isSlavePortAccess, Seq("from_CPU")))
+
+    cover(new CrossProperty(
+      Seq(data_error_cover, request_source),
+      Seq(),
+      "MemorySystem;;Scratchpad Memory Bit Flip Cross Covers"))
+  } else {
+
+    val data_error_cover = Seq(CoverBoolean(s2_valid_data_error, Seq("data_error")))
+
+    val data_error_type = Seq(
+      CoverBoolean(!s2_data_error_uncorrectable, Seq("correctable")),
+      CoverBoolean(s2_data_error_uncorrectable, Seq("uncorrectable")))
+    val data_error_dirty = Seq(
+      CoverBoolean(!s2_victim_dirty, Seq("data_clean")),
+      CoverBoolean(s2_victim_dirty, Seq("data_dirty")))
+    val request_source = if (supports_flush) {
+        Seq(
+          CoverBoolean(!flushing, Seq("access")),
+          CoverBoolean(flushing, Seq("during_flush")))
+      } else {
+        Seq(CoverBoolean(true.B, Seq("never_flush")))
+      }
+    val tag_error_cover = Seq(
+      CoverBoolean( !metaArb.io.in(1).valid, Seq("no_tag_error")),
+      CoverBoolean( metaArb.io.in(1).valid && !s2_meta_error_uncorrectable, Seq("correctable_tag_error")),
+      CoverBoolean( metaArb.io.in(1).valid && s2_meta_error_uncorrectable, Seq("uncorrectable_tag_error")))
+    cover(new CrossProperty(
+      Seq(data_error_cover, data_error_type, data_error_dirty, request_source, tag_error_cover),
+      Seq(),
+      "MemorySystem;;Cache Memory Bit Flip Cross Covers"))
+  }
 }

src/main/scala/rocket/ICache.scala

@@ -241,17 +241,6 @@ class ICacheModule(outer: ICache) extends LazyModuleImp(outer)
     }
   }
 
-  // output signals
-  outer.icacheParams.latency match {
-    case 1 =>
-      require(tECC.isInstanceOf[IdentityCode])
-      require(dECC.isInstanceOf[IdentityCode])
-      require(outer.icacheParams.itimAddr.isEmpty)
-      io.resp.bits.data := Mux1H(s1_tag_hit, s1_dout)
-      io.resp.bits.ae := s1_tl_error.asUInt.orR
-      io.resp.valid := s1_valid && s1_hit
-
-    case 2 =>
   val s1_clk_en = s1_valid || s1_slaveValid
   val s2_tag_hit = RegEnable(s1_tag_hit, s1_clk_en)
   val s2_hit_way = OHToUInt(s2_tag_hit)
@@ -264,6 +253,24 @@ class ICacheModule(outer: ICache) extends LazyModuleImp(outer)
   val s2_data_decoded = dECC.decode(s2_way_mux)
   val s2_disparity = s2_tag_disparity || s2_data_decoded.error
   val s2_full_word_write = Wire(init = false.B)
+
+  val s1_scratchpad_hit = Mux(s1_slaveValid, lineInScratchpad(scratchpadLine(s1s3_slaveAddr)), addrInScratchpad(io.s1_paddr))
+  val s2_scratchpad_hit = RegEnable(s1_scratchpad_hit, s1_clk_en)
+  val s2_report_uncorrectable_error = s2_scratchpad_hit && s2_data_decoded.uncorrectable && (s2_valid || (s2_slaveValid && !s2_full_word_write))
+  val s2_error_addr = scratchpadBase.map(base => Mux(s2_scratchpad_hit, base + s2_scratchpad_word_addr, 0.U)).getOrElse(0.U)
+
+  // output signals
+  outer.icacheParams.latency match {
+    case 1 =>
+      require(tECC.isInstanceOf[IdentityCode])
+      require(dECC.isInstanceOf[IdentityCode])
+      require(outer.icacheParams.itimAddr.isEmpty)
+      io.resp.bits.data := Mux1H(s1_tag_hit, s1_dout)
+      io.resp.bits.ae := s1_tl_error.asUInt.orR
+      io.resp.valid := s1_valid && s1_hit
+
+    case 2 =>
+      // when some sort of memory bit error have occurred
       when (s2_valid && s2_disparity) { invalidate := true }
 
       io.resp.bits.data := s2_data_decoded.uncorrected
@@ -271,10 +278,6 @@ class ICacheModule(outer: ICache) extends LazyModuleImp(outer)
       io.resp.bits.replay := s2_disparity
       io.resp.valid := s2_valid && s2_hit
 
-      val s1_scratchpad_hit = Mux(s1_slaveValid, lineInScratchpad(scratchpadLine(s1s3_slaveAddr)), addrInScratchpad(io.s1_paddr))
-      val s2_scratchpad_hit = RegEnable(s1_scratchpad_hit, s1_clk_en)
-      val s2_report_uncorrectable_error = s2_scratchpad_hit && s2_data_decoded.uncorrectable && (s2_valid || (s2_slaveValid && !s2_full_word_write))
-      val s2_error_addr = scratchpadBase.map(base => Mux(s2_scratchpad_hit, base + s2_scratchpad_word_addr, 0.U)).getOrElse(0.U)
       io.errors.correctable.foreach { c =>
         c.valid := (s2_valid || s2_slaveValid) && s2_disparity && !s2_report_uncorrectable_error
         c.bits := s2_error_addr
@@ -404,4 +407,36 @@ class ICacheModule(outer: ICache) extends LazyModuleImp(outer)
 
   def ccover(cond: Bool, label: String, desc: String)(implicit sourceInfo: SourceInfo) =
     cover(cond, s"ICACHE_$label", "MemorySystem;;" + desc)
+
+  val mem_active_valid = Seq(CoverBoolean(s2_valid, Seq("mem_active")))
+  val data_error = Seq(
+    CoverBoolean(!s2_data_decoded.correctable && !s2_data_decoded.uncorrectable, Seq("no_data_error")),
+    CoverBoolean(s2_data_decoded.correctable, Seq("correctable_bit_error")),
+    CoverBoolean(s2_data_decoded.uncorrectable, Seq("uncorrectable_bit_error")))
+  val request_source = Seq(
+    CoverBoolean(!s2_slaveValid, Seq("from_CPU")),
+    CoverBoolean(s2_slaveValid, Seq("from_TL"))
+  )
+  val tag_error = Seq(
+    CoverBoolean(!s2_tag_disparity, Seq("no_tag_error")),
+    CoverBoolean(s2_tag_disparity, Seq("tag_error"))
+  )
+  val mem_mode = Seq(
+    CoverBoolean(s2_scratchpad_hit, Seq("ITIM_mode")),
+    CoverBoolean(!s2_scratchpad_hit, Seq("cache_mode"))
+  )
+
+  val error_cross_covers = new CrossProperty(
+    Seq(mem_active_valid, data_error, tag_error, request_source, mem_mode),
+    Seq(
+      // tag error cannot occur in ITIM mode
+      Seq("tag_error", "ITIM_mode"),
+      // tag is only parity check
+      Seq("tag_error", "uncorrectable_bit_error"),
+      // Can only respond to TL in ITIM mode
+      Seq("from_TL", "cache_mode")
+    ),
+    "MemorySystem;;Memory Bit Flip Cross Covers")
+
+  cover(error_cross_covers)
 }

src/main/scala/util/Property.scala

@@ -45,6 +45,94 @@ class DefaultPropertyLibrary extends BasePropertyLibrary {
   }
 }
 
+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 }))
+      }
+    })
+  }
+
+}
+
 object cover {
   def apply(cond: Bool)(implicit sourceInfo: SourceInfo, p: Parameters): Unit = {
     p(PropertyLibrary).generateProperty(CoverPropertyParameters(cond))
@@ -55,6 +143,13 @@ object cover {
   def apply(cond: Bool, label: String, message: String)(implicit sourceInfo: SourceInfo, p: Parameters): Unit = {
     p(PropertyLibrary).generateProperty(CoverPropertyParameters(cond, label, message))
   }
+  def apply(prop: BaseProperty)(implicit sourceInfo: SourceInfo, p: Parameters): Unit = {
+    prop.generateProperties().foreach( (pp: BasePropertyParameters) => {
+      if (pp.pType == PropertyType.Cover) {
+        p(PropertyLibrary).generateProperty(CoverPropertyParameters(pp.cond, pp.label, pp.message))
+      }
+    })
+  }
   def apply[T <: Data](rv: ReadyValidIO[T], label: String, message: String)(implicit sourceInfo: SourceInfo, p: Parameters): Unit = {
     apply( rv.valid &&  rv.ready, label + "_FIRE",  message + ": valid and ready")
     apply( rv.valid && !rv.ready, label + "_STALL", message + ": valid and not ready")