From 9cd99455cfb18a2ceec994bba54efd89d5f8c549 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Kevin=20L=C3=A4ufer?= <laeufer@cs.berkeley.edu>
Date: Tue, 11 Jan 2022 18:02:05 -0800
Subject: [PATCH] maltese: re-enable logging

---
 .../chiseltest/formal/backends/Maltese.scala  | 20 +++++++++----------
 1 file changed, 9 insertions(+), 11 deletions(-)

diff --git a/src/main/scala/chiseltest/formal/backends/Maltese.scala b/src/main/scala/chiseltest/formal/backends/Maltese.scala
index aacbe7e36..cbe5c9753 100644
--- a/src/main/scala/chiseltest/formal/backends/Maltese.scala
+++ b/src/main/scala/chiseltest/formal/backends/Maltese.scala
@@ -4,13 +4,7 @@ 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._
@@ -18,6 +12,7 @@ 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 }