From af460b771b4f52c5ad35c78b9374c20de78598ba Mon Sep 17 00:00:00 2001
From: H Wang <haoyuanwang102@gmail.com>
Date: Thu, 14 Dec 2023 19:59:21 -0800
Subject: [PATCH] Bump FIRRTL to 1.5.6; Update dependencies; Add passes to
 accomodate FIRRTL changes

---
 build.sbt                                     |  6 +--
 project/build.properties                      |  2 +-
 src/main/scala/Compiler.scala                 | 12 ++++++
 .../scala/passes/RemoveFormalNCover.scala     | 42 +++++++++++++++++++
 .../resources/ReplacedRsvdKey_correct.fir     |  1 +
 5 files changed, 59 insertions(+), 4 deletions(-)
 create mode 100644 src/main/scala/passes/RemoveFormalNCover.scala

diff --git a/build.sbt b/build.sbt
index d6c7d3b6..6792d109 100644
--- a/build.sbt
+++ b/build.sbt
@@ -4,7 +4,7 @@ version := "0.8-SNAPSHOT"
 
 name := "essent"
 
-scalaVersion := "2.12.13"
+scalaVersion := "2.12.18"
 
 scalacOptions ++= Seq("-deprecation", "-unchecked")
 
@@ -12,9 +12,9 @@ libraryDependencies += "com.github.scopt" %% "scopt" % "3.7.1"
 
 libraryDependencies += "org.scalatest" %% "scalatest" % "3.2.0" % "test"
 
-libraryDependencies += "org.json4s" %% "json4s-native" % "3.6.9"
+libraryDependencies += "org.json4s" %% "json4s-native" % "3.6.12"
 
-libraryDependencies += "edu.berkeley.cs" %% "firrtl" % "1.4.3"
+libraryDependencies += "edu.berkeley.cs" %% "firrtl" % "1.5.6"
 
 
 // Assembly
diff --git a/project/build.properties b/project/build.properties
index 797e7ccf..c8fcab54 100644
--- a/project/build.properties
+++ b/project/build.properties
@@ -1 +1 @@
-sbt.version=1.3.10
+sbt.version=1.6.2
diff --git a/src/main/scala/Compiler.scala b/src/main/scala/Compiler.scala
index 9e6e60f4..ea12704f 100644
--- a/src/main/scala/Compiler.scala
+++ b/src/main/scala/Compiler.scala
@@ -304,7 +304,19 @@ class EssentEmitter(initialOpt: OptFlags, w: Writer, circuit: Circuit) extends L
 
 
 class EssentCompiler(opt: OptFlags) {
+
+  // VerilogMemDelays: compiling memory latencies to combinational-read memories with delay pipelines.
+  // This pass eliminates mems with read latency = 1 (introduced by CHIRRTL smem)
+  // and thus satisfy essent.pass.FactorMemReads (memHasRightParams)
+
+  // ConvertAsserts: Convert Verification IR (with op == Formal.Assert) into conventional print statement
+
   val readyForEssent: Seq[TransformDependency] =
+    Seq(
+      Dependency(firrtl.passes.memlib.VerilogMemDelays),
+      Dependency(essent.passes.RemoveFormalNCover),
+      Dependency(firrtl.transforms.formal.ConvertAsserts)
+    ) ++
     firrtl.stage.Forms.LowFormOptimized ++
     Seq(
 //      Dependency(essent.passes.LegacyInvalidNodesForConds),
diff --git a/src/main/scala/passes/RemoveFormalNCover.scala b/src/main/scala/passes/RemoveFormalNCover.scala
new file mode 100644
index 00000000..4c3af4ca
--- /dev/null
+++ b/src/main/scala/passes/RemoveFormalNCover.scala
@@ -0,0 +1,42 @@
+package essent.passes
+
+import firrtl.Mappers._
+import firrtl._
+import firrtl.ir._
+import firrtl.passes._
+
+
+object RemoveFormalNCover extends Pass {
+  def desc = "Removes FIRRTL formal and coverage (Assume, Cover) as they are not supported by ESSENT"
+
+  override def prerequisites = Seq.empty
+  override def optionalPrerequisites = Seq.empty
+  override def optionalPrerequisiteOf = firrtl.stage.Forms.LowFormOptimized
+  override def invalidates(a: Transform) = false
+
+  def removeUnsupported(s: Statement): Statement = s.map(removeUnsupported) match {
+    case Block(stmts) =>
+      val newStmts = stmts.filter{_ match {
+        case s: Verification => s.op match{
+          case Formal.Cover => false
+          case Formal.Assume => false
+          case _ => true
+        }
+        case _ => true
+      }}
+      newStmts.size match {
+        case 0 => EmptyStmt
+        case 1 => newStmts.head
+        case _ => Block(newStmts)
+      }
+    case sx => sx
+  }
+
+  private def onModule(m: DefModule): DefModule = {
+    m match {
+      case m: Module    => Module(m.info, m.name, m.ports, removeUnsupported(m.body))
+      case m: ExtModule => m
+    }
+  }
+  def run(c: Circuit): Circuit = Circuit(c.info, c.modules.map(onModule), c.main)
+}
diff --git a/src/test/resources/ReplacedRsvdKey_correct.fir b/src/test/resources/ReplacedRsvdKey_correct.fir
index e6f5bb05..325bcfef 100644
--- a/src/test/resources/ReplacedRsvdKey_correct.fir
+++ b/src/test/resources/ReplacedRsvdKey_correct.fir
@@ -1,3 +1,4 @@
+FIRRTL version 1.1.0
 circuit Testrsvd :
   module Break :
     input clk : Clock