wip

src/main/scala/chiseltest/formal/StutteringClockTransform.scala

@@ -3,7 +3,7 @@
 
 package chiseltest.formal
 
-import firrtl._
+import firrtl.{options, _}
 import firrtl.annotations._
 import firrtl.backends.experimental.smt.FirrtlToTransitionSystem
 import firrtl.options.Dependency
@@ -51,8 +51,12 @@ object StutteringClockTransform extends Transform with DependencyAPIMigration {
     Dependency[firrtl.transforms.PropagatePresetAnnotations]
   override def invalidates(a: Transform): Boolean = false
 
-  // this pass needs to run *before* converting to a transition system
-  override def optionalPrerequisiteOf: Seq[TransformDependency] = Seq(Dependency(FirrtlToTransitionSystem))
+  override def optionalPrerequisiteOf: Seq[TransformDependency] = Seq(
+    // this pass needs to run *before* converting to a transition system
+    Dependency(FirrtlToTransitionSystem),
+    // this pass also needs to run before inlining as it assumes the standard module structure
+    Dependency[firrtl.passes.InlineInstances]
+  )
   // we need to be able to identify registers that are "preset"
   override def optionalPrerequisites: Seq[TransformDependency] = Seq(
     Dependency[PropagatePresetAnnotations]

src/test/scala/chiseltest/formal/multiclock/AsyncFifoTests.scala

@@ -7,14 +7,19 @@ import chisel3.util._
 import chiseltest._
 import chiseltest.experimental.observe
 import chiseltest.formal._
+import logger.{LogLevel, LogLevelAnnotation}
 import org.scalatest.flatspec.AnyFlatSpec
 
 class AsyncFifoTests extends AnyFlatSpec with ChiselScalatestTester with Formal with FormalBackendOption {
   behavior of "AsyncFifo"
 
-  // TODO: find out why wire persist when running stuttering clock transform
-  it should "pass a formal integrity test" taggedAs FormalTag ignore {
-    verify(new FifoTestWrapper(new AsyncFifo(UInt(8.W), 4)), Seq(BoundedCheck(4), DefaultBackend, EnableMultiClock))
+  it should "pass a formal integrity test" taggedAs FormalTag in {
+    verify(new FifoTestWrapper(new AsyncFifo(UInt(8.W), 4)), Seq(
+      BoundedCheck(4), DefaultBackend, EnableMultiClock,
+      // TODO: we currently do not model undef since the DefRandToRegisterPass doesn't deal well with multi-clock
+      DoNotModelUndef,
+      LogLevelAnnotation(LogLevel.Info)
+    ))
   }
 }