From ebdee1a353f9758139195b92629901fc818e312d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Kevin=20L=C3=A4ufer?= Date: Tue, 6 Dec 2022 14:01:02 -0500 Subject: [PATCH] wip --- .../chiseltest/formal/StutteringClockTransform.scala | 10 +++++++--- .../chiseltest/formal/multiclock/AsyncFifoTests.scala | 11 ++++++++--- 2 files changed, 15 insertions(+), 6 deletions(-) diff --git a/src/main/scala/chiseltest/formal/StutteringClockTransform.scala b/src/main/scala/chiseltest/formal/StutteringClockTransform.scala index 346e82518..7d9135c1a 100644 --- a/src/main/scala/chiseltest/formal/StutteringClockTransform.scala +++ b/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] diff --git a/src/test/scala/chiseltest/formal/multiclock/AsyncFifoTests.scala b/src/test/scala/chiseltest/formal/multiclock/AsyncFifoTests.scala index ee421f37a..f28d14a60 100644 --- a/src/test/scala/chiseltest/formal/multiclock/AsyncFifoTests.scala +++ b/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) + )) } }