Fix PMB formal test by adding in the formal asserts trait

SpinalHDL · jdavidberger · Jan 1, 2025 · Jan 1, 2025 · Jan 2, 2025 · Jan 2, 2025
commit 59996920b83909c8c84ace10305fd0e13397c04a
diff --git a/core/src/main/scala/spinal/core/formal/Misc.scala b/core/src/main/scala/spinal/core/formal/Misc.scala
@@ -2,6 +2,8 @@ package spinal.core.formal
 
 import spinal.core.{Area, Bool, Component, assert, assume}
 
+import scala.collection.mutable
+
 object FormalDut{
   def apply[T <: Component](dut : T) = {
     val c = Component.current
@@ -29,8 +31,32 @@ trait WithFormalAsserts {
       assert(cond, Seq(msg:_*))
     }
   }
+
   def withFormalAsserts() : this.type = {
     formalAsserts()
     this
   }
 }
+
+object WithFormalAsserts {
+  def formalAssertsChildren(c: Component, useAssumes : Boolean = false): Unit = {
+    def apply(c : Component, walkSet : mutable.HashSet[Component]) : Unit = {
+      if (!walkSet.contains(c)) {
+
+        walkSet += c
+        c match {
+          case c: WithFormalAsserts => {
+            c.formalAsserts(useAssumes)
+          }
+          case _ => c.walkComponents(apply(_, walkSet))
+        }
+      }
+    }
+
+    c.addPrePopTask(() => {
+      val walkSet = new mutable.HashSet[Component]()
+      walkSet += c
+      c.walkComponents(apply(_, walkSet))
+    })
+  }
+}
diff --git a/tester/src/test/scala/spinal/tester/scalatest/FormalPipelinedMemoryBus.scala b/tester/src/test/scala/spinal/tester/scalatest/FormalPipelinedMemoryBus.scala
@@ -73,7 +73,7 @@ class PipelinedMemoryBusDecoderFormal(mappings: Seq[AddressMapping], pendingRspM
   }
 }
 
-class PipelinedMemoryBusInterconnectComponent(mappings: Seq[AddressMapping], pendingRspMax : Int, portCount : Int, rspRouteQueue : Boolean) extends Component {
+class PipelinedMemoryBusInterconnectComponent(mappings: Seq[AddressMapping], pendingRspMax : Int, portCount : Int, rspRouteQueue : Boolean) extends Component with WithFormalAsserts {
   val config = PipelinedMemoryBusConfig(32, 32)
 
   val io = new Bundle {
@@ -91,6 +91,12 @@ class PipelinedMemoryBusInterconnectComponent(mappings: Seq[AddressMapping], pen
   io.masters.foreach(master => {
     interconnect.addMaster(master, io.slaves)
   })
+
+
+  override def formalAsserts(implicit useAssumes: Boolean) = {
+    WithFormalAsserts.formalAssertsChildren(this, useAssumes)
+    new Area {}
+  }
 }
 
 class PipelinedMemoryBusInterconnectFormal(mappings: Seq[AddressMapping], pendingRspMax : Int, portCount : Int, rspRouteQueue : Boolean) extends Component {