maltese: re-enable logging

ucb-bar · Feb 12, 2022 · e6775ca · e6775ca
1 parent 6e57770
commit e6775ca
Showing 1 changed file with 9 additions and 11 deletions.
diff --git a/src/main/scala/chiseltest/formal/backends/Maltese.scala b/src/main/scala/chiseltest/formal/backends/Maltese.scala
@@ -4,20 +4,15 @@ package chiseltest.formal.backends
 
 import chiseltest.formal.backends.btor.BtormcModelChecker
 import chiseltest.formal.backends.smt._
-import chiseltest.formal.{
-  DoNotModelUndef,
-  DoNotOptimizeFormal,
-  EnableMultiClock,
-  FailedBoundedCheckException,
-  StutteringClockTransform
-}
+import chiseltest.formal._
 import firrtl._
 import firrtl.annotations._
 import firrtl.stage._
 import firrtl.backends.experimental.smt.random._
 import firrtl.backends.experimental.smt._
 import chiseltest.simulator._
 import firrtl.options.Dependency
+import logger.{LogLevel, LogLevelAnnotation, Logger}
 
 sealed trait FormalEngineAnnotation extends NoTargetAnnotation
 
@@ -84,14 +79,15 @@ private[chiseltest] object Maltese {
     modelUndef: Boolean,
     multiClock: Boolean
   ): CircuitState = {
+    val logLevel = Seq() // Seq(LogLevelAnnotation(LogLevel.Warn))
     if (!modelUndef && !multiClock) { CircuitState(circuit, annos) }
     else {
-      val res = firrtlPhase.transform(
+      val res = runFirrtlPhase(
         Seq(
           RunFirrtlTransformAnnotation(new LowFirrtlEmitter),
           new CurrentFirrtlStateAnnotation(Forms.LowForm),
           FirrtlCircuitAnnotation(circuit)
-        ) ++ annos ++
+        ) ++ annos ++ logLevel ++
           (if (modelUndef) DefRandomTreadleAnnos else List()) ++
           (if (multiClock) MultiClockAnnos else List())
       )
@@ -126,9 +122,9 @@ private[chiseltest] object Maltese {
   private case class SysInfo(sys: TransitionSystem, stateMap: Map[String, String], memDepths: Map[String, Int])
 
   private def toTransitionSystem(circuit: ir.Circuit, annos: AnnotationSeq): SysInfo = {
-    val logLevel = Seq() // Seq("-ll", "info")
+    val logLevel = Seq() // Seq(LogLevelAnnotation(LogLevel.Warn))
     val opts: AnnotationSeq = if (annos.contains(DoNotOptimizeFormal)) Seq() else Optimizations
-    val res = firrtlPhase.transform(
+    val res = runFirrtlPhase(
       Seq(
         RunFirrtlTransformAnnotation(Dependency(SMTLibEmitter)),
         new CurrentFirrtlStateAnnotation(Forms.LowForm),
@@ -152,6 +148,8 @@ private[chiseltest] object Maltese {
     sys.signals.count(_.lbl == IsBad) == 0
 
   private def firrtlPhase = new FirrtlPhase
+  private def runFirrtlPhase(annos: AnnotationSeq): AnnotationSeq =
+    Logger.makeScope(annos) { firrtlPhase.transform(annos) }
 
   private def makeCheckers(annos: AnnotationSeq, targetDir: os.Path): Seq[IsModelChecker] = {
     val engines = annos.collect { case a: FormalEngineAnnotation => a }