From 40eb96716dcd6e7e4acc81fe0fb90e1294835021 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Kevin=20L=C3=A4ufer?= <laeufer@cs.berkeley.edu>
Date: Mon, 28 Aug 2023 12:00:39 -0400
Subject: [PATCH 01/12] add support for Chisel6 sequences

---
 .../ConvertCirctSequenceIntrinsics.scala      | 70 +++++++++++++++++++
 .../scala/chiseltest/simulator/Compiler.scala | 17 ++---
 .../chiseltest/tests/SequencesTests.scala     | 26 +++++++
 3 files changed, 102 insertions(+), 11 deletions(-)
 create mode 100644 src/main/scala/chiseltest/sequences/ConvertCirctSequenceIntrinsics.scala
 create mode 100644 src/test/scala/chiseltest/tests/SequencesTests.scala

diff --git a/src/main/scala/chiseltest/sequences/ConvertCirctSequenceIntrinsics.scala b/src/main/scala/chiseltest/sequences/ConvertCirctSequenceIntrinsics.scala
new file mode 100644
index 000000000..e95f8f418
--- /dev/null
+++ b/src/main/scala/chiseltest/sequences/ConvertCirctSequenceIntrinsics.scala
@@ -0,0 +1,70 @@
+package chiseltest.sequences
+
+import firrtl2._
+import firrtl2.options.Dependency
+import firrtl2.passes.ExpandWhensAndCheck
+import firrtl2.stage.Forms
+import firrtl2.transforms.DedupModules
+import scala.collection.mutable
+
+
+/** Replaces circt sequence intrinsics with a synthesizable version. */
+object ConvertCirctSequenceIntrinsics extends Transform {
+  override def invalidates(a: Transform) = false
+  override def prerequisites = Forms.Resolved
+  // this should run before we remove whens and deduplication
+  override def optionalPrerequisiteOf = Seq(
+    Dependency[ExpandWhensAndCheck], Dependency[DedupModules]
+  )
+
+  private val Intrinsics = Set(
+    "circt_has_been_reset",
+    "circt_ltl_disable",
+    "circt_ltl_clock",
+    // Assume, Assert, Cover
+    "circt_verif_assert",
+    "circt_verif_assume",
+    "circt_verif_cover"
+  )
+
+  private def findIntrinsicMapping(circuit: ir.Circuit): Map[String, String] =
+    circuit.modules.collect{ case e: ir.ExtModule if Intrinsics.contains(e.defname) => e.name -> e.defname }.toMap
+
+  override protected def execute(state: CircuitState): CircuitState = {
+    // scan ext modules to see if there are any CIRCT intrinsics handled by this pass
+    val intrinsics = findIntrinsicMapping(state.circuit)
+    if (intrinsics.isEmpty) { // early exit / nothing to do
+      return state
+    }
+
+    // remove intrinsics ext modules
+    val withoutIntrinsicsModules = state.circuit.modules.filter {
+      case e: ir.ExtModule if Intrinsics.contains(e.defname) => false
+      case _ => true
+    }
+
+    // replace intrinsics in modules
+    val modules = withoutIntrinsicsModules.map {
+      case m : ir.Module => onModule(m, intrinsics)
+      case other => other
+    }
+
+    val circuit = state.circuit.copy(modules = modules)
+
+    // TODO
+    println(circuit.serialize)
+    state.copy(circuit = circuit)
+  }
+
+  private def onModule(m: ir.Module, intrinsics: Map[String, String]): ir.Module = {
+    // first we remove all instances of our intrinsics and build a netlist of them instead
+    m
+  }
+
+  private case class IntModule(name: String, kind: String, inputs: Map[String, ir.RefLikeExpression], outputs: Map[String, ir.RefLikeExpression])
+  private case class Ctx(intrinsics: Map[String, String])
+
+  private def onStmt(s: ir.Statement): ir.Statement = {
+    s
+  }
+}
diff --git a/src/main/scala/chiseltest/simulator/Compiler.scala b/src/main/scala/chiseltest/simulator/Compiler.scala
index 19b37e1ec..fabb08407 100644
--- a/src/main/scala/chiseltest/simulator/Compiler.scala
+++ b/src/main/scala/chiseltest/simulator/Compiler.scala
@@ -5,12 +5,13 @@ package chiseltest.simulator
 import chisel3.RawModule
 import firrtl2.{AnnotationSeq, EmittedCircuitAnnotation}
 import firrtl2.annotations.{Annotation, DeletedAnnotation}
-import firrtl2.options.TargetDirAnnotation
-import firrtl2.stage.{FirrtlCircuitAnnotation, FirrtlStage}
+import firrtl2.options.{Dependency, TargetDirAnnotation}
+import firrtl2.stage.{FirrtlCircuitAnnotation, FirrtlStage, RunFirrtlTransformAnnotation}
 import firrtl2.logger.{LogLevelAnnotation, Logger}
 
 private[chiseltest] object Compiler {
-
+  private val defaultPasses = Seq(Dependency(chiseltest.sequences.ConvertCirctSequenceIntrinsics))
+  private def defaultPassesAnnos = defaultPasses.map(p => RunFirrtlTransformAnnotation(p))
   def elaborate[M <: RawModule](
     gen:           () => M,
     annotationSeq: AnnotationSeq,
@@ -19,22 +20,16 @@ private[chiseltest] object Compiler {
     ChiselBridge.elaborate[M](gen, annotationSeq, chiselAnnos)
   def toLowFirrtl(state: firrtl2.CircuitState, annos: AnnotationSeq = List()): firrtl2.CircuitState = {
     requireTargetDir(state.annotations)
-    val inAnnos = annos ++: stateToAnnos(state)
+    val inAnnos = defaultPassesAnnos ++: annos ++: stateToAnnos(state)
     val res = firrtlStage.execute(Array("-E", "low"), inAnnos)
     annosToState(res)
   }
   def lowFirrtlToSystemVerilog(state: firrtl2.CircuitState, annos: AnnotationSeq = List()): firrtl2.CircuitState = {
     requireTargetDir(state.annotations)
-    val inAnnos = annos ++: stateToAnnos(state)
+    val inAnnos = defaultPassesAnnos ++: annos ++: stateToAnnos(state)
     val res = firrtlStage.execute(Array("--start-from", "low", "-E", "sverilog"), inAnnos)
     annosToState(res)
   }
-  def lowFirrtlToVerilog(state: firrtl2.CircuitState, annos: AnnotationSeq = List()): firrtl2.CircuitState = {
-    requireTargetDir(state.annotations)
-    val inAnnos = annos ++: stateToAnnos(state)
-    val res = firrtlStage.execute(Array("--start-from", "low", "-E", "verilog"), inAnnos)
-    annosToState(res)
-  }
   private def stateToAnnos(state: firrtl2.CircuitState): AnnotationSeq = {
     val annosWithoutCircuit = state.annotations.filterNot(_.isInstanceOf[FirrtlCircuitAnnotation])
     FirrtlCircuitAnnotation(state.circuit) +: annosWithoutCircuit
diff --git a/src/test/scala/chiseltest/tests/SequencesTests.scala b/src/test/scala/chiseltest/tests/SequencesTests.scala
new file mode 100644
index 000000000..c6770354d
--- /dev/null
+++ b/src/test/scala/chiseltest/tests/SequencesTests.scala
@@ -0,0 +1,26 @@
+package chiseltest.tests
+
+import org.scalatest.freespec.AnyFreeSpec
+import chiseltest._
+import chisel3._
+import chisel3.ltl._
+import chisel3.ltl.Sequence._
+
+
+class SimpleAssertionModule extends Module {
+  val a = IO(Input(Bool()))
+  AssertProperty(a)
+  AssumeProperty(a)
+  CoverProperty(a)
+}
+
+/** Make sure that chiselest works with Chisel sequence assertions. */
+class SequencesTests extends AnyFreeSpec with ChiselScalatestTester {
+  "simple assert / assume / cover properties should work" in {
+    test(new SimpleAssertionModule) { dut =>
+      dut.a.poke(true)
+      dut.clock.step()
+    }
+  }
+
+}

From 17c43bec05637596a2ec92b686f4e17ed4d6f0ff Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Kevin=20L=C3=A4ufer?= <laeufer@cs.berkeley.edu>
Date: Fri, 1 Sep 2023 16:03:45 -0400
Subject: [PATCH 02/12] wip : Sequence IR

---
 .../ConvertCirctSequenceIntrinsics.scala      | 14 +++++---
 src/main/scala/chiseltest/sequences/IR.scala  | 35 +++++++++++++++++++
 ...ests.scala => SequencePropertyTests.scala} |  1 -
 3 files changed, 44 insertions(+), 6 deletions(-)
 create mode 100644 src/main/scala/chiseltest/sequences/IR.scala
 rename src/test/scala/chiseltest/tests/{SequencesTests.scala => SequencePropertyTests.scala} (99%)

diff --git a/src/main/scala/chiseltest/sequences/ConvertCirctSequenceIntrinsics.scala b/src/main/scala/chiseltest/sequences/ConvertCirctSequenceIntrinsics.scala
index e95f8f418..adbaa38b6 100644
--- a/src/main/scala/chiseltest/sequences/ConvertCirctSequenceIntrinsics.scala
+++ b/src/main/scala/chiseltest/sequences/ConvertCirctSequenceIntrinsics.scala
@@ -7,14 +7,14 @@ import firrtl2.stage.Forms
 import firrtl2.transforms.DedupModules
 import scala.collection.mutable
 
-
 /** Replaces circt sequence intrinsics with a synthesizable version. */
 object ConvertCirctSequenceIntrinsics extends Transform {
   override def invalidates(a: Transform) = false
   override def prerequisites = Forms.Resolved
   // this should run before we remove whens and deduplication
   override def optionalPrerequisiteOf = Seq(
-    Dependency[ExpandWhensAndCheck], Dependency[DedupModules]
+    Dependency[ExpandWhensAndCheck],
+    Dependency[DedupModules]
   )
 
   private val Intrinsics = Set(
@@ -28,7 +28,7 @@ object ConvertCirctSequenceIntrinsics extends Transform {
   )
 
   private def findIntrinsicMapping(circuit: ir.Circuit): Map[String, String] =
-    circuit.modules.collect{ case e: ir.ExtModule if Intrinsics.contains(e.defname) => e.name -> e.defname }.toMap
+    circuit.modules.collect { case e: ir.ExtModule if Intrinsics.contains(e.defname) => e.name -> e.defname }.toMap
 
   override protected def execute(state: CircuitState): CircuitState = {
     // scan ext modules to see if there are any CIRCT intrinsics handled by this pass
@@ -45,7 +45,7 @@ object ConvertCirctSequenceIntrinsics extends Transform {
 
     // replace intrinsics in modules
     val modules = withoutIntrinsicsModules.map {
-      case m : ir.Module => onModule(m, intrinsics)
+      case m: ir.Module => onModule(m, intrinsics)
       case other => other
     }
 
@@ -61,7 +61,11 @@ object ConvertCirctSequenceIntrinsics extends Transform {
     m
   }
 
-  private case class IntModule(name: String, kind: String, inputs: Map[String, ir.RefLikeExpression], outputs: Map[String, ir.RefLikeExpression])
+  private case class IntModule(
+    name:    String,
+    kind:    String,
+    inputs:  Map[String, ir.RefLikeExpression],
+    outputs: Map[String, ir.RefLikeExpression])
   private case class Ctx(intrinsics: Map[String, String])
 
   private def onStmt(s: ir.Statement): ir.Statement = {
diff --git a/src/main/scala/chiseltest/sequences/IR.scala b/src/main/scala/chiseltest/sequences/IR.scala
new file mode 100644
index 000000000..c3a8be418
--- /dev/null
+++ b/src/main/scala/chiseltest/sequences/IR.scala
@@ -0,0 +1,35 @@
+// Copyright 2022-2023 The Regents of the University of California
+// released under BSD 3-Clause License
+// author: Kevin Laeufer <laeufer@cs.berkeley.edu>
+
+package chiseltest.sequences
+
+sealed trait BooleanExpr {}
+case class SymbolExpr(name: String) extends BooleanExpr
+case class NotExpr(e: BooleanExpr) extends BooleanExpr
+case class AndExpr(a: BooleanExpr, b: BooleanExpr) extends BooleanExpr
+case class OrExpr(a: BooleanExpr, b: BooleanExpr) extends BooleanExpr
+case object FalseExpr extends BooleanExpr
+case object TrueExpr extends BooleanExpr
+
+sealed trait Sequence {}
+
+case class SeqPred(predicate: BooleanExpr) extends Sequence
+case class SeqOr(s1: Sequence, s2: Sequence) extends Sequence
+case class SeqConcat(s1: Sequence, s2: Sequence) extends Sequence
+case class SeqIntersect(s1: Sequence, s2: Sequence) extends Sequence
+case class SeqNot(s1: Sequence) extends Sequence
+case class SeqImplies(s1: Sequence, p1: Property) extends Sequence
+case class SeqImpliesNext(s1: Sequence, p1: Property) extends Sequence
+case class SeqFuse(s1: Sequence, s2: Sequence) extends Sequence
+
+sealed trait Property {}
+
+case class PropSeq(s: Sequence) extends Property
+
+case class PropertyTop(
+  name:       String,
+  predicates: Seq[String], // boolean inputs
+  disableIff: BooleanExpr = FalseExpr
+  // TODO
+)
diff --git a/src/test/scala/chiseltest/tests/SequencesTests.scala b/src/test/scala/chiseltest/tests/SequencePropertyTests.scala
similarity index 99%
rename from src/test/scala/chiseltest/tests/SequencesTests.scala
rename to src/test/scala/chiseltest/tests/SequencePropertyTests.scala
index c6770354d..30d733d13 100644
--- a/src/test/scala/chiseltest/tests/SequencesTests.scala
+++ b/src/test/scala/chiseltest/tests/SequencePropertyTests.scala
@@ -6,7 +6,6 @@ import chisel3._
 import chisel3.ltl._
 import chisel3.ltl.Sequence._
 
-
 class SimpleAssertionModule extends Module {
   val a = IO(Input(Bool()))
   AssertProperty(a)

From 181fc330605ab645746ecb87aceb5009f1604faf Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Kevin=20L=C3=A4ufer?= <laeufer@cs.berkeley.edu>
Date: Tue, 5 Sep 2023 16:44:16 -0400
Subject: [PATCH 03/12] replace has been reset with an implementation and
 collect all other intrinsics

---
 .../ConvertCirctSequenceIntrinsics.scala      | 135 +++++++++++++++---
 1 file changed, 119 insertions(+), 16 deletions(-)

diff --git a/src/main/scala/chiseltest/sequences/ConvertCirctSequenceIntrinsics.scala b/src/main/scala/chiseltest/sequences/ConvertCirctSequenceIntrinsics.scala
index adbaa38b6..b705d6844 100644
--- a/src/main/scala/chiseltest/sequences/ConvertCirctSequenceIntrinsics.scala
+++ b/src/main/scala/chiseltest/sequences/ConvertCirctSequenceIntrinsics.scala
@@ -1,10 +1,12 @@
 package chiseltest.sequences
 
 import firrtl2._
+import firrtl2.annotations.{Annotation, CircuitTarget, PresetRegAnnotation}
 import firrtl2.options.Dependency
 import firrtl2.passes.ExpandWhensAndCheck
 import firrtl2.stage.Forms
 import firrtl2.transforms.DedupModules
+
 import scala.collection.mutable
 
 /** Replaces circt sequence intrinsics with a synthesizable version. */
@@ -17,10 +19,14 @@ object ConvertCirctSequenceIntrinsics extends Transform {
     Dependency[DedupModules]
   )
 
+  private val HasBeenReset = "circt_has_been_reset"
+  private val LtlDisable = "circt_ltl_disable"
+  private val LtlClock = "circt_ltl_clock"
+
   private val Intrinsics = Set(
-    "circt_has_been_reset",
-    "circt_ltl_disable",
-    "circt_ltl_clock",
+    HasBeenReset,
+    LtlDisable,
+    LtlClock,
     // Assume, Assert, Cover
     "circt_verif_assert",
     "circt_verif_assume",
@@ -44,8 +50,13 @@ object ConvertCirctSequenceIntrinsics extends Transform {
     }
 
     // replace intrinsics in modules
+    val c = CircuitTarget(state.circuit.main)
+    val newAnnos = mutable.ListBuffer[Annotation]()
     val modules = withoutIntrinsicsModules.map {
-      case m: ir.Module => onModule(m, intrinsics)
+      case m: ir.Module =>
+        val (mod, annos) = onModule(c, m, intrinsics)
+        newAnnos ++= annos
+        mod
       case other => other
     }
 
@@ -53,22 +64,114 @@ object ConvertCirctSequenceIntrinsics extends Transform {
 
     // TODO
     println(circuit.serialize)
-    state.copy(circuit = circuit)
+    state.copy(circuit = circuit, annotations = newAnnos.toSeq ++: state.annotations)
+  }
+
+  private def onModule(c: CircuitTarget, m: ir.Module, intrinsics: Map[String, String]): (ir.Module, AnnotationSeq) = {
+    println(m.serialize)
+    val ctx = Ctx(intrinsics, Namespace(m))
+    val body = onStmt(ctx)(m.body)
+    val newAnnos = ctx.presetRegs.toSeq.map(name => PresetRegAnnotation(c.module(m.name).ref(name)))
+    val finalModule = m.copy(body = body)
+    (finalModule, newAnnos)
+  }
+
+  private case class IntrinsicInstance(name: String, intrinsic: String, info: ir.Info)
+  private case class Ctx(
+    /** maps the name of a module to the intrinsic it represents */
+    moduleToIntrinsic: Map[String, String],
+    /** namespace of the current module */
+    namespace: Namespace,
+    /** maps the name of an instance to the intrinsic that its module represents */
+    instToIntrinsic: mutable.HashMap[String, IntrinsicInstance] = mutable.HashMap(),
+    /** keeps track of all inputs to a intrinsic instance */
+    inputs: mutable.HashMap[String, List[(String, ir.Expression)]] = mutable.HashMap(),
+    /** Keeps track of any intrinsic outputs that we have generated. Currently only used for `HasBeenReset` */
+    outputs: mutable.HashMap[(String, String), ir.Expression] = mutable.HashMap(),
+    /** Keeps track of registers that need to be preset annotated (to implement HasBeenReset) */
+    presetRegs: mutable.ListBuffer[String] = mutable.ListBuffer(),
+    /** Avoids duplicate has_been_reset trackers. */
+    hasBeenResetCache: mutable.HashMap[(String, String), ir.Expression] = mutable.HashMap()) {
+    def isIntrinsicMod(module: String): Boolean = moduleToIntrinsic.contains(module)
+
+    def isIntrinsicInst(module: String): Boolean = instToIntrinsic.contains(module)
+  }
+
+  private def onStmt(ctx: Ctx)(s: ir.Statement): ir.Statement = s.mapExpr(onExpr(ctx)) match {
+    // connecting an intrinsic input
+    case ir.Connect(_, ir.SubField(ir.Reference(instIn, _, _, _), portIn, _, _), expr) if ctx.isIntrinsicInst(instIn) =>
+      expr match {
+        case ir.SubField(ir.Reference(instOut, _, _, _), portOut, _, _) if ctx.isIntrinsicInst(instOut) =>
+          connectIntrinsics(ctx, instIn, portIn, instOut, portOut)
+        case other =>
+          val old = ctx.inputs.getOrElse(instIn, List())
+          ctx.inputs(instIn) = (portIn, expr) +: old
+          if (ctx.instToIntrinsic(instIn).intrinsic == HasBeenReset) {
+            onHasBeenResetInput(ctx, instIn)
+          } else {
+            ir.EmptyStmt
+          }
+      }
+    // connect an intrinsic output
+    case ir.Connect(_, loc, ir.SubField(ir.Reference(inst, _, _, _), port, _, _)) if ctx.isIntrinsicInst(inst) =>
+      throw new NotImplementedError(
+        s"Unexpected intrinsic output which is not directly connected to an intrinsic input!: ${s.serialize}"
+      )
+    case ir.DefInstance(info, name, module, _) if ctx.isIntrinsicMod(module) =>
+      ctx.instToIntrinsic(name) = IntrinsicInstance(name, ctx.moduleToIntrinsic(module), info)
+      ir.EmptyStmt
+    case other => other.mapStmt(onStmt(ctx))
+  }
+
+  private def connectIntrinsics(ctx: Ctx, instIn: String, portIn: String, instOut: String, portOut: String)
+    : ir.Statement = {
+    println(s"TODO: ${instIn}.$portIn <= ${instOut}.$portOut")
+    ir.EmptyStmt
+  }
+
+  private def onHasBeenResetInput(ctx: Ctx, inst: String): ir.Statement = {
+    val inputs = ctx.inputs(inst)
+    val (clock, reset) = (inputs.find(_._1 == "clock").map(_._2), inputs.find(_._1 == "reset").map(_._2))
+    (clock, reset) match {
+      case (Some(clockExpr), Some(resetExpr)) =>
+        val key = (clockExpr.serialize, resetExpr.serialize)
+        val (stmt, output) = ctx.hasBeenResetCache.get(key) match {
+          case Some(output) => (ir.EmptyStmt, output)
+          case None         =>
+            // generate has been reset
+            val (stmt, output) = buildHasBeenReset(ctx, inst, clockExpr, resetExpr)
+            ctx.hasBeenResetCache(key) = output
+            (stmt, output)
+        }
+        ctx.outputs((inst, "out")) = output
+        stmt
+
+      case _ => ir.EmptyStmt
+    }
   }
 
-  private def onModule(m: ir.Module, intrinsics: Map[String, String]): ir.Module = {
-    // first we remove all instances of our intrinsics and build a netlist of them instead
-    m
+  private def buildHasBeenReset(ctx: Ctx, inst: String, clock: ir.Expression, reset: ir.Expression)
+    : (ir.Statement, ir.Expression) = {
+    val instanceInfo = ctx.instToIntrinsic(inst)
+    val info = instanceInfo.info
+    val regName = ctx.namespace.newName("has_been_reset_reg")
+    val outName = ctx.namespace.newName("has_been_reset")
+    // register starts out as false
+    val reg = ir.DefRegister(info, regName, Utils.BoolType, clock, Utils.False(), Utils.False())
+    val regRef = ir.Reference(reg).copy(flow = SinkFlow)
+    ctx.presetRegs.addOne(regName)
+    // when reset becomes true, we set out register to 1
+    val update = ir.Conditionally(info, reset, ir.Connect(info, regRef, Utils.True()), ir.EmptyStmt)
+    // the output indicates whether the circuits _has been reset_ **and** that reset is not currently active
+    val outExpr = Utils.and(regRef.copy(flow = SourceFlow), Utils.not(reset))
+    val outNode = ir.DefNode(info, outName, outExpr)
+    (ir.Block(Seq(reg, update, outNode)), ir.Reference(outNode).copy(flow = SourceFlow))
   }
 
-  private case class IntModule(
-    name:    String,
-    kind:    String,
-    inputs:  Map[String, ir.RefLikeExpression],
-    outputs: Map[String, ir.RefLikeExpression])
-  private case class Ctx(intrinsics: Map[String, String])
+  private def onExpr(ctx: Ctx)(e: ir.Expression): ir.Expression = e match {
+    case ref @ ir.SubField(ir.Reference(inst, _, _, _), port, _, _) =>
+      ctx.outputs.getOrElse((inst, port), ref)
+    case other => other.mapExpr(onExpr(ctx))
 
-  private def onStmt(s: ir.Statement): ir.Statement = {
-    s
   }
 }

From 9344c24845958d6be8680031bb3a9ae4dcf1f9bf Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Kevin=20L=C3=A4ufer?= <laeufer@cs.berkeley.edu>
Date: Tue, 5 Sep 2023 17:09:30 -0400
Subject: [PATCH 04/12] wip: convert intrinsics

---
 .../ConvertCirctSequenceIntrinsics.scala      | 36 ++++++++++++++-----
 src/main/scala/chiseltest/sequences/IR.scala  | 10 +++---
 2 files changed, 33 insertions(+), 13 deletions(-)

diff --git a/src/main/scala/chiseltest/sequences/ConvertCirctSequenceIntrinsics.scala b/src/main/scala/chiseltest/sequences/ConvertCirctSequenceIntrinsics.scala
index b705d6844..9d936fc1d 100644
--- a/src/main/scala/chiseltest/sequences/ConvertCirctSequenceIntrinsics.scala
+++ b/src/main/scala/chiseltest/sequences/ConvertCirctSequenceIntrinsics.scala
@@ -22,16 +22,14 @@ object ConvertCirctSequenceIntrinsics extends Transform {
   private val HasBeenReset = "circt_has_been_reset"
   private val LtlDisable = "circt_ltl_disable"
   private val LtlClock = "circt_ltl_clock"
+  // Assume, Assert, Cover
+  private val VerifOps = Set("circt_verif_assert", "circt_verif_assume", "circt_verif_cover")
 
   private val Intrinsics = Set(
     HasBeenReset,
     LtlDisable,
-    LtlClock,
-    // Assume, Assert, Cover
-    "circt_verif_assert",
-    "circt_verif_assume",
-    "circt_verif_cover"
-  )
+    LtlClock
+  ) | VerifOps
 
   private def findIntrinsicMapping(circuit: ir.Circuit): Map[String, String] =
     circuit.modules.collect { case e: ir.ExtModule if Intrinsics.contains(e.defname) => e.name -> e.defname }.toMap
@@ -88,6 +86,8 @@ object ConvertCirctSequenceIntrinsics extends Transform {
     inputs: mutable.HashMap[String, List[(String, ir.Expression)]] = mutable.HashMap(),
     /** Keeps track of any intrinsic outputs that we have generated. Currently only used for `HasBeenReset` */
     outputs: mutable.HashMap[(String, String), ir.Expression] = mutable.HashMap(),
+    /** Maps intrinsic instance name to IR Node */
+    nodes: mutable.HashMap[String, Node] = mutable.HashMap(),
     /** Keeps track of registers that need to be preset annotated (to implement HasBeenReset) */
     presetRegs: mutable.ListBuffer[String] = mutable.ListBuffer(),
     /** Avoids duplicate has_been_reset trackers. */
@@ -104,9 +104,13 @@ object ConvertCirctSequenceIntrinsics extends Transform {
         case ir.SubField(ir.Reference(instOut, _, _, _), portOut, _, _) if ctx.isIntrinsicInst(instOut) =>
           connectIntrinsics(ctx, instIn, portIn, instOut, portOut)
         case other =>
+          // remember all inputs
           val old = ctx.inputs.getOrElse(instIn, List())
-          ctx.inputs(instIn) = (portIn, expr) +: old
-          if (ctx.instToIntrinsic(instIn).intrinsic == HasBeenReset) {
+          ctx.inputs(instIn) = (portIn, other) +: old
+
+          // for some intrinsics, connecting inputs triggers an action
+          val intrinsicName = ctx.instToIntrinsic(instIn).intrinsic
+          if (intrinsicName == HasBeenReset) {
             onHasBeenResetInput(ctx, instIn)
           } else {
             ir.EmptyStmt
@@ -125,7 +129,21 @@ object ConvertCirctSequenceIntrinsics extends Transform {
 
   private def connectIntrinsics(ctx: Ctx, instIn: String, portIn: String, instOut: String, portOut: String)
     : ir.Statement = {
-    println(s"TODO: ${instIn}.$portIn <= ${instOut}.$portOut")
+    val intrinsicName = ctx.instToIntrinsic(instIn).intrinsic
+    // take action according to the intrinsic
+    if (VerifOps.contains(intrinsicName)) {
+      onVerificationOp(ctx, instIn)
+    } else {
+      println(s"TODO: ${instIn}.$portIn <= ${instOut}.$portOut")
+      ir.EmptyStmt
+    }
+  }
+
+  private def onVerificationOp(ctx: Ctx, inst: String): ir.Statement = {
+    // there should be exactly one input
+    val (inputName, input) = ctx.inputs(inst).head
+    assert(inputName == "property")
+
     ir.EmptyStmt
   }
 
diff --git a/src/main/scala/chiseltest/sequences/IR.scala b/src/main/scala/chiseltest/sequences/IR.scala
index c3a8be418..e789498d2 100644
--- a/src/main/scala/chiseltest/sequences/IR.scala
+++ b/src/main/scala/chiseltest/sequences/IR.scala
@@ -4,7 +4,9 @@
 
 package chiseltest.sequences
 
-sealed trait BooleanExpr {}
+sealed trait Node {}
+
+sealed trait BooleanExpr extends Node {}
 case class SymbolExpr(name: String) extends BooleanExpr
 case class NotExpr(e: BooleanExpr) extends BooleanExpr
 case class AndExpr(a: BooleanExpr, b: BooleanExpr) extends BooleanExpr
@@ -12,7 +14,7 @@ case class OrExpr(a: BooleanExpr, b: BooleanExpr) extends BooleanExpr
 case object FalseExpr extends BooleanExpr
 case object TrueExpr extends BooleanExpr
 
-sealed trait Sequence {}
+sealed trait Sequence extends Node {}
 
 case class SeqPred(predicate: BooleanExpr) extends Sequence
 case class SeqOr(s1: Sequence, s2: Sequence) extends Sequence
@@ -23,7 +25,7 @@ case class SeqImplies(s1: Sequence, p1: Property) extends Sequence
 case class SeqImpliesNext(s1: Sequence, p1: Property) extends Sequence
 case class SeqFuse(s1: Sequence, s2: Sequence) extends Sequence
 
-sealed trait Property {}
+sealed trait Property extends Node {}
 
 case class PropSeq(s: Sequence) extends Property
 
@@ -32,4 +34,4 @@ case class PropertyTop(
   predicates: Seq[String], // boolean inputs
   disableIff: BooleanExpr = FalseExpr
   // TODO
-)
+) extends Node

From 98867816256a0f153950c3e9de45d2053bfe5a20 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Kevin=20L=C3=A4ufer?= <laeufer@cs.berkeley.edu>
Date: Tue, 5 Sep 2023 22:03:10 -0400
Subject: [PATCH 05/12] wip: sequence assertion backends

---
 .../scala/chiseltest/sequences/Backend.scala  |  23 ++
 .../ConvertCirctSequenceIntrinsics.scala      | 100 ++++++-
 .../chiseltest/sequences/FsmBackend.scala     | 280 ++++++++++++++++++
 src/main/scala/chiseltest/sequences/IR.scala  |  17 +-
 4 files changed, 402 insertions(+), 18 deletions(-)
 create mode 100644 src/main/scala/chiseltest/sequences/Backend.scala
 create mode 100644 src/main/scala/chiseltest/sequences/FsmBackend.scala

diff --git a/src/main/scala/chiseltest/sequences/Backend.scala b/src/main/scala/chiseltest/sequences/Backend.scala
new file mode 100644
index 000000000..04738cf6d
--- /dev/null
+++ b/src/main/scala/chiseltest/sequences/Backend.scala
@@ -0,0 +1,23 @@
+// Copyright 2022-2023 The Regents of the University of California
+// released under BSD 3-Clause License
+// author: Kevin Laeufer <laeufer@cs.berkeley.edu>
+
+package chiseltest.sequences
+
+import firrtl2._
+
+trait Backend {
+  def generate(skeleton: ir.Module, prop: PropertyTop): Seq[ir.DefModule]
+}
+
+object Backend {
+
+  /** Builds the common skeleton module and then calls the backend to fill in the implementation */
+  def generate(backend: Backend, prop: PropertyTop): Seq[ir.DefModule] = {
+    val ports = Seq(
+      ir.Port(ir.NoInfo, "clock", ir.Input, ir.ClockType)
+    ) ++ prop.predicates.map(name => ir.Port(ir.NoInfo, name, ir.Input, Utils.BoolType))
+    val skeleton = ir.Module(ir.NoInfo, prop.name, ports, ir.EmptyStmt)
+    backend.generate(skeleton, prop)
+  }
+}
diff --git a/src/main/scala/chiseltest/sequences/ConvertCirctSequenceIntrinsics.scala b/src/main/scala/chiseltest/sequences/ConvertCirctSequenceIntrinsics.scala
index 9d936fc1d..a275a9ca8 100644
--- a/src/main/scala/chiseltest/sequences/ConvertCirctSequenceIntrinsics.scala
+++ b/src/main/scala/chiseltest/sequences/ConvertCirctSequenceIntrinsics.scala
@@ -1,3 +1,7 @@
+// Copyright 2022-2023 The Regents of the University of California
+// released under BSD 3-Clause License
+// author: Kevin Laeufer <laeufer@cs.berkeley.edu>
+
 package chiseltest.sequences
 
 import firrtl2._
@@ -19,6 +23,8 @@ object ConvertCirctSequenceIntrinsics extends Transform {
     Dependency[DedupModules]
   )
 
+  private val CurrentBackend: Backend = FsmBackend
+
   private val HasBeenReset = "circt_has_been_reset"
   private val LtlDisable = "circt_ltl_disable"
   private val LtlClock = "circt_ltl_clock"
@@ -82,12 +88,12 @@ object ConvertCirctSequenceIntrinsics extends Transform {
     namespace: Namespace,
     /** maps the name of an instance to the intrinsic that its module represents */
     instToIntrinsic: mutable.HashMap[String, IntrinsicInstance] = mutable.HashMap(),
-    /** keeps track of all inputs to a intrinsic instance */
-    inputs: mutable.HashMap[String, List[(String, ir.Expression)]] = mutable.HashMap(),
+    /** keeps track of all inputs to intrinsic instances that are regular firrtl expressions */
+    exprInputs: mutable.HashMap[(String, String), ir.Expression] = mutable.HashMap(),
+    /** keeps track of all inputs to intrinsic instances that are sequence IR Nodes */
+    nodeInputs: mutable.HashMap[(String, String), (Node, PropertyEnv)] = mutable.HashMap(),
     /** Keeps track of any intrinsic outputs that we have generated. Currently only used for `HasBeenReset` */
     outputs: mutable.HashMap[(String, String), ir.Expression] = mutable.HashMap(),
-    /** Maps intrinsic instance name to IR Node */
-    nodes: mutable.HashMap[String, Node] = mutable.HashMap(),
     /** Keeps track of registers that need to be preset annotated (to implement HasBeenReset) */
     presetRegs: mutable.ListBuffer[String] = mutable.ListBuffer(),
     /** Avoids duplicate has_been_reset trackers. */
@@ -95,6 +101,17 @@ object ConvertCirctSequenceIntrinsics extends Transform {
     def isIntrinsicMod(module: String): Boolean = moduleToIntrinsic.contains(module)
 
     def isIntrinsicInst(module: String): Boolean = instToIntrinsic.contains(module)
+
+    private def getNode(inst: String, port: String): (Node, PropertyEnv) =
+      nodeInputs.getOrElse((inst, port), NodeUtils.asBooleanExpr(exprInputs((inst, port))))
+    def getBoolean(inst: String, port: String): (BooleanExpr, PropertyEnv) = {
+      val (node, env) = getNode(inst, port)
+      (NodeUtils.asBooleanExpr(node).get, env)
+    }
+    def getPropertyTop(inst: String, port: String): (PropertyTop, PropertyEnv) = {
+      val (node, env) = getNode(inst, port)
+      (NodeUtils.asPropertyTop(node, env), env)
+    }
   }
 
   private def onStmt(ctx: Ctx)(s: ir.Statement): ir.Statement = s.mapExpr(onExpr(ctx)) match {
@@ -105,8 +122,7 @@ object ConvertCirctSequenceIntrinsics extends Transform {
           connectIntrinsics(ctx, instIn, portIn, instOut, portOut)
         case other =>
           // remember all inputs
-          val old = ctx.inputs.getOrElse(instIn, List())
-          ctx.inputs(instIn) = (portIn, other) +: old
+          ctx.exprInputs((instIn, portIn)) = other
 
           // for some intrinsics, connecting inputs triggers an action
           val intrinsicName = ctx.instToIntrinsic(instIn).intrinsic
@@ -129,27 +145,45 @@ object ConvertCirctSequenceIntrinsics extends Transform {
 
   private def connectIntrinsics(ctx: Ctx, instIn: String, portIn: String, instOut: String, portOut: String)
     : ir.Statement = {
-    val intrinsicName = ctx.instToIntrinsic(instIn).intrinsic
+    // convert output intrinsic
+    val (outNode, outEnv) = intrinsicToNode(ctx, instOut, portOut)
+    ctx.nodeInputs((instIn, portIn)) = (outNode, outEnv)
+
     // take action according to the intrinsic
+    val intrinsicName = ctx.instToIntrinsic(instIn).intrinsic
     if (VerifOps.contains(intrinsicName)) {
       onVerificationOp(ctx, instIn)
     } else {
-      println(s"TODO: ${instIn}.$portIn <= ${instOut}.$portOut")
       ir.EmptyStmt
     }
   }
 
+  private def intrinsicToNode(ctx: Ctx, inst: String, outPort: String): (Node, PropertyEnv) = {
+    val intrinsicName = ctx.instToIntrinsic(inst).intrinsic
+    intrinsicName match {
+      case LtlDisable =>
+        val (in, inEnv) = ctx.getPropertyTop(inst, "in")
+        val (condition, condEnv) = ctx.getBoolean(inst, "condition")
+        val combinedEnv = inEnv.union(condEnv)
+        (in.copy(predicates = combinedEnv.getPredicateInputs, disableIff = condition), combinedEnv)
+      case LtlClock =>
+        val (in, inEnv) = ctx.getPropertyTop(inst, "in")
+        val clock = ctx.exprInputs((inst, "clock"))
+        (in, inEnv.copy(preds = inEnv.preds ++ Map("clock" -> clock)))
+      case other => throw new NotImplementedError(s"TODO: convert $other intrinsic!")
+    }
+  }
+
   private def onVerificationOp(ctx: Ctx, inst: String): ir.Statement = {
-    // there should be exactly one input
-    val (inputName, input) = ctx.inputs(inst).head
-    assert(inputName == "property")
+    val (prop, propEnv) = ctx.getPropertyTop(inst, "property")
+    val modules = Backend.generate(CurrentBackend, prop)
+    throw new NotImplementedError("TODO: verification op")
 
     ir.EmptyStmt
   }
 
   private def onHasBeenResetInput(ctx: Ctx, inst: String): ir.Statement = {
-    val inputs = ctx.inputs(inst)
-    val (clock, reset) = (inputs.find(_._1 == "clock").map(_._2), inputs.find(_._1 == "reset").map(_._2))
+    val (clock, reset) = (ctx.exprInputs.get((inst, "clock")), ctx.exprInputs.get((inst, "reset")))
     (clock, reset) match {
       case (Some(clockExpr), Some(resetExpr)) =>
         val key = (clockExpr.serialize, resetExpr.serialize)
@@ -193,3 +227,43 @@ object ConvertCirctSequenceIntrinsics extends Transform {
 
   }
 }
+
+case class PropertyEnv(preds: Map[String, ir.Expression]) {
+  def getPredicateInputs: Seq[String] = preds.keys.toSeq.sorted
+  def union(other: PropertyEnv): PropertyEnv = PropertyEnv(preds ++ other.preds)
+}
+
+private object NodeUtils {
+  private def sanitizeRefName(name: String): String =
+    name.replace('.', '_').replace('[', '_').replace(']', '_')
+
+  def asBooleanExpr(expr: ir.Expression): (BooleanExpr, PropertyEnv) = expr match {
+    case ref: ir.RefLikeExpression =>
+      val name = sanitizeRefName(ref.serialize) // TODO: ensure name is unique!
+      (SymbolExpr(name), PropertyEnv(Map(name -> ref)))
+    case other => {
+      other
+      ???
+    }
+  }
+  def asBooleanExpr(node: Node): Option[BooleanExpr] = node match {
+    case expr: BooleanExpr => Some(expr)
+    case _ => None
+  }
+  def asSequence(node: Node): Option[Sequence] = node match {
+    case expr:     BooleanExpr => Some(SeqPred(expr))
+    case sequence: Sequence    => Some(sequence)
+    case _ => None
+  }
+  def asProperty(node: Node): Option[Property] = node match {
+    case expr:     BooleanExpr => Some(PropSeq(SeqPred(expr)))
+    case sequence: Sequence    => Some(PropSeq(sequence))
+    case property: Property    => Some(property)
+    case _ => None
+  }
+  def asPropertyTop(node: Node, env: PropertyEnv): PropertyTop = node match {
+    case top: PropertyTop => top
+    case other => PropertyTop(asProperty(other).get, predicates = env.getPredicateInputs)
+  }
+
+}
diff --git a/src/main/scala/chiseltest/sequences/FsmBackend.scala b/src/main/scala/chiseltest/sequences/FsmBackend.scala
new file mode 100644
index 000000000..0d69e24c0
--- /dev/null
+++ b/src/main/scala/chiseltest/sequences/FsmBackend.scala
@@ -0,0 +1,280 @@
+// Copyright 2022-2023 The Regents of the University of California
+// released under BSD 3-Clause License
+// author: Kevin Laeufer <laeufer@cs.berkeley.edu>
+
+package chiseltest.sequences
+import firrtl2.ir
+import chisel3._
+import chisel3.util._
+import chiseltest.simulator.Compiler
+
+/** Uses Chisel to generate FSMs that implement the Sequence Property */
+object FsmBackend extends Backend {
+  override def generate(skeleton: ir.Module, prop: PropertyTop): Seq[ir.DefModule] = {
+    val (state, _) = Compiler.elaborate(
+      () => new PropertyFsmAutomaton(prop.predicates, { pred => compileAlways(pred, prop.prop) }),
+      Seq(),
+      Seq()
+    )
+    state.circuit.modules
+  }
+
+  private def compileAlways(pred: Map[String, Bool], p: Property): Bool = {
+    val n = runtime(p)
+    val props = Seq.fill(n)(comp(pred, p))
+    AssertAlwaysModule(props)
+  }
+
+  private def comp(pred: Map[String, Bool], p: Property): PropertyFsmIO = {
+    p match {
+      case PropSeq(s) => PropSeqModule(comp(pred, s))
+    }
+  }
+
+  private def comp(pred: Map[String, Bool], s: Sequence): SequenceIO = {
+    s match {
+      case SeqPred(predicate)     => SeqExprModule(comp(pred, predicate))
+      case SeqConcat(s1, s2)      => SeqConcatModule(comp(pred, s1), comp(pred, s2))
+      case SeqImpliesNext(s1, p1) => SeqImpliesNextModule(comp(pred, s1), comp(pred, p1))
+    }
+  }
+
+  private def comp(pred: Map[String, Bool], e: BooleanExpr): Bool = e match {
+    case SymbolExpr(name) => pred(name)
+    case NotExpr(e)       => !comp(pred, e)
+    case AndExpr(a, b)    => comp(pred, a) && comp(pred, b)
+    case OrExpr(a, b)     => comp(pred, a) || comp(pred, b)
+  }
+
+  /** calculates an upper bound for the property runtime in cycles */
+  private def runtime(p: Property): Int = {
+    p match {
+      case PropSeq(s) => runtime(s)
+    }
+  }
+
+  /** calculates an upper bound for the sequence runtime in cycles */
+  private def runtime(s: Sequence): Int = {
+    s match {
+      case SeqPred(_)             => 1
+      case SeqOr(s1, s2)          => runtime(s1).max(runtime(s2))
+      case SeqFuse(s1, s2)        => runtime(s1) + runtime(s2) - 1
+      case SeqConcat(s1, s2)      => runtime(s1) + runtime(s2)
+      case SeqImpliesNext(s1, p1) => runtime(s1) + runtime(p1) // TODO: is this correct?
+    }
+  }
+}
+
+class PropertyFsmAutomaton(preds: Seq[String], compile: Map[String, Bool] => Bool)
+    extends Module
+    with RequireAsyncReset {
+  val predicates = preds.map { name =>
+    name -> IO(Input(Bool())).suggestName(name)
+  }
+  val fail = compile(predicates.toMap)
+}
+
+object SeqRes extends ChiselEnum {
+  val SeqFail, SeqPending, SeqHold, SeqHoldStrong = Value
+}
+
+class SequenceIO extends Bundle {
+
+  /** is the FSM active this cycle? */
+  val advance = Input(Bool())
+
+  /** indicates that the FSM has not finished yet */
+  val running = Output(Bool())
+
+  /** current result (only valid if advance is true) */
+  val status = Output(SeqRes())
+}
+
+object PropRes extends ChiselEnum {
+  val PropTrue, PropUndetermined, PropFalse, PropVacuous = Value
+}
+
+class PropertyFsmIO extends Bundle {
+
+  /** is the FSM active this cycle? */
+  val advance = Input(Bool())
+
+  /** only valid if advance is true */
+  val status = Output(PropRes())
+}
+
+/** converts a boolean signal to the sequence I/O */
+class SeqExprModule extends Module {
+  val io = IO(new SequenceIO)
+  val predicate = IO(Input(Bool()))
+  // holds iff the predicate is true
+  io.status := Mux(predicate, SeqRes.SeqHoldStrong, SeqRes.SeqFail)
+  // no FSM state, so never running
+  io.running := false.B
+}
+
+object SeqExprModule {
+  def apply(predicate: Bool): SequenceIO = {
+    val mod = Module(new SeqExprModule).suggestName("seq_expr")
+    mod.predicate := predicate
+    mod.io
+  }
+}
+
+/** concatenates two sequences */
+class SeqConcatModule extends Module {
+  import SeqRes._
+
+  val io = IO(new SequenceIO)
+  val seq1 = IO(Flipped(new SequenceIO)); seq1.advance := false.B
+  val seq2 = IO(Flipped(new SequenceIO)); seq2.advance := false.B
+
+  // keep track of which sequence is running
+  val run1 = RegInit(false.B)
+  val run2 = RegInit(false.B)
+
+  // running if either of the sub-sequences runs
+  io.running := run1 || run2
+
+  // we run sequence 1 if we are in the starting state or if run1 is true
+  val shouldRunSeq1 = run1 || (!run1 && !run2)
+  when(io.advance) {
+    // advance sequence 1
+    when(shouldRunSeq1) {
+      seq1.advance := true.B
+      val r = seq1.status
+      // we fail if the sub-sequence fails
+      io.status := Mux(r === SeqFail, SeqFail, SeqPending)
+      // we continue with sequence one if it hold or is pending
+      run1 := r.isOneOf(SeqPending, SeqHold)
+      // we stop executing sequence 1 and switch to sequence 2 in the next cycle
+      run2 := r.isOneOf(SeqHoldStrong)
+    }.otherwise {
+      seq2.advance := true.B
+      val r2 = seq2.status
+      // since we already checked sequence 1 we can just relay the status
+      io.status := r2
+      // continue executing if sequence 2 is not finished
+      run2 := r2.isOneOf(SeqPending, SeqHold)
+    }
+  }.otherwise {
+    io.status := DontCare
+  }
+}
+
+object SeqConcatModule {
+  def apply(s1: SequenceIO, s2: SequenceIO): SequenceIO = {
+    val mod = Module(new SeqConcatModule).suggestName("seq_concat")
+    mod.seq1 <> s1
+    mod.seq2 <> s2
+    mod.io
+  }
+}
+
+object SeqImpliesNextModule {
+  def apply(o: SequenceIO, o1: PropertyFsmIO): SequenceIO = ???
+}
+
+/** converts a sequence I/O into a property I/O */
+class PropSeqModule extends Module {
+  val seq = IO(Flipped(new SequenceIO))
+  val io = IO(new PropertyFsmIO)
+  // advance is just connected
+  seq.advance := io.advance
+
+  when(seq.status.isOneOf(SeqRes.SeqHold, SeqRes.SeqHoldStrong)) {
+    io.status := PropRes.PropTrue
+  }.elsewhen(seq.status.isOneOf(SeqRes.SeqPending)) {
+    io.status := PropRes.PropUndetermined
+  }.elsewhen(seq.status.isOneOf(SeqRes.SeqFail)) {
+    io.status := PropRes.PropFalse
+  }.otherwise {
+    // assert(false.B, "should not get here")
+    io.status := DontCare
+  }
+}
+
+object PropSeqModule {
+  def apply(s: SequenceIO): PropertyFsmIO = {
+    val mod = Module(new PropSeqModule).suggestName("prop_seq")
+    mod.seq <> s
+    mod.io
+  }
+}
+
+/** assert a property from the start of reset
+  * @note:
+  *   this is not an always assert, it will only check the property once!
+  */
+class AssertPropModule(desc: String) extends Module {
+  val propertyIO = IO(Flipped(new PropertyFsmIO))
+
+  // the assertion is active starting at reset
+  val going = RegInit(true.B)
+  propertyIO.advance := false.B
+
+  // only advance when reset is false and we are still going
+  when(going && !reset.asBool) {
+    propertyIO.advance := true.B
+    // continue advancing the property while the result is still undetermined
+    going := propertyIO.status === PropRes.PropUndetermined
+    // if the property returns false, this assertion fails
+    assert(propertyIO.status =/= PropRes.PropFalse, desc)
+  }
+}
+
+object AssertPropModule {
+  def apply(p: PropertyFsmIO, desc: String): Unit = {
+    val mod = Module(new AssertPropModule(desc)).suggestName("assert_prop")
+    mod.propertyIO <> p
+  }
+}
+
+object findFirstInactive {
+
+  /** return one-hot encoded list with the index of the first active reg turned on */
+  def apply(active: UInt): UInt = {
+    val activeList = active.asBools
+    val cases = activeList.reverse.zipWithIndex.map { case (a, i) =>
+      !a -> (1 << (activeList.length - i - 1)).U
+    }
+
+    MuxCase(1.U, cases)
+  }
+}
+
+class AssertAlwaysModule(n: Int) extends Module {
+  import PropRes._
+
+  val props = IO(Vec(n, Flipped(new PropertyFsmIO)))
+  val fail = IO(Output(Bool()))
+
+  val active = RegInit(0.U(n.W))
+
+  // pick a free property (as a one-hot)
+  val newProp = findFirstInactive(active)
+
+  // properties that are active in this cycle
+  val nowActive = active | newProp
+
+  // advance all active properties
+  props.zip(nowActive.asBools).foreach { case (prop, active) =>
+    prop.advance := active
+  }
+
+  // find out which properties will need to be run next cycle
+  val stillRunning = Cat(props.map(p => p.status === PropUndetermined)) // TODO: reverse?
+  active := stillRunning & nowActive
+
+  // none of the properties that we advance should be false
+  val propFailed = Cat(props.map(p => p.status === PropFalse)) // TODO: reverse?
+  fail := (propFailed & nowActive) =/= 0.U
+}
+
+object AssertAlwaysModule {
+  def apply(props: Seq[PropertyFsmIO]): Bool = {
+    val mod = Module(new AssertAlwaysModule(props.length))
+    mod.props.zip(props).foreach { case (a, b) => a <> b }
+    mod.fail
+  }
+}
diff --git a/src/main/scala/chiseltest/sequences/IR.scala b/src/main/scala/chiseltest/sequences/IR.scala
index e789498d2..dfb409a27 100644
--- a/src/main/scala/chiseltest/sequences/IR.scala
+++ b/src/main/scala/chiseltest/sequences/IR.scala
@@ -29,9 +29,16 @@ sealed trait Property extends Node {}
 
 case class PropSeq(s: Sequence) extends Property
 
+sealed trait VerificationOp
+case object AssertOp extends VerificationOp
+case object AssumeOp extends VerificationOp
+case object CoverOp extends VerificationOp
+case object NoOp extends VerificationOp
+
 case class PropertyTop(
-  name:       String,
-  predicates: Seq[String], // boolean inputs
-  disableIff: BooleanExpr = FalseExpr
-  // TODO
-) extends Node
+  prop:       Property,
+  name:       String = "",
+  predicates: Seq[String] = Seq(), // boolean inputs
+  disableIff: BooleanExpr = FalseExpr,
+  op:         VerificationOp = NoOp)
+    extends Node

From f93bdba5a5bedbd0c3564d6e2766278822a6c56f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Kevin=20L=C3=A4ufer?= <laeufer@cs.berkeley.edu>
Date: Wed, 6 Sep 2023 15:16:29 -0400
Subject: [PATCH 06/12] fsm backend almost working

---
 .../chiseltest/formal/annotateAsPreset.scala  |  0
 .../scala/chiseltest/sequences/Backend.scala  | 11 ++-
 .../ConvertCirctSequenceIntrinsics.scala      | 69 ++++++++++++++-----
 .../chiseltest/sequences/FsmBackend.scala     | 54 ++++++++++++---
 .../sequences/HighFirrtlFlatten.scala         | 43 ++++++++++++
 src/main/scala/chiseltest/sequences/IR.scala  |  9 +++
 .../chiseltest/sequences/PrefixModules.scala  | 51 ++++++++++++++
 7 files changed, 208 insertions(+), 29 deletions(-)
 rename src/{test => main}/scala/chiseltest/formal/annotateAsPreset.scala (100%)
 create mode 100644 src/main/scala/chiseltest/sequences/HighFirrtlFlatten.scala
 create mode 100644 src/main/scala/chiseltest/sequences/PrefixModules.scala

diff --git a/src/test/scala/chiseltest/formal/annotateAsPreset.scala b/src/main/scala/chiseltest/formal/annotateAsPreset.scala
similarity index 100%
rename from src/test/scala/chiseltest/formal/annotateAsPreset.scala
rename to src/main/scala/chiseltest/formal/annotateAsPreset.scala
diff --git a/src/main/scala/chiseltest/sequences/Backend.scala b/src/main/scala/chiseltest/sequences/Backend.scala
index 04738cf6d..b7fb79b32 100644
--- a/src/main/scala/chiseltest/sequences/Backend.scala
+++ b/src/main/scala/chiseltest/sequences/Backend.scala
@@ -5,19 +5,24 @@
 package chiseltest.sequences
 
 import firrtl2._
+import firrtl2.annotations.CircuitTarget
 
 trait Backend {
-  def generate(skeleton: ir.Module, prop: PropertyTop): Seq[ir.DefModule]
+  def generate(skeleton: ir.Module, moduleNames: Seq[String], prop: PropertyTop): CircuitState
 }
 
 object Backend {
 
   /** Builds the common skeleton module and then calls the backend to fill in the implementation */
-  def generate(backend: Backend, prop: PropertyTop): Seq[ir.DefModule] = {
+  def generate(backend: Backend, main: String, moduleNames: Seq[String], prop: PropertyTop): CircuitState = {
     val ports = Seq(
       ir.Port(ir.NoInfo, "clock", ir.Input, ir.ClockType)
     ) ++ prop.predicates.map(name => ir.Port(ir.NoInfo, name, ir.Input, Utils.BoolType))
     val skeleton = ir.Module(ir.NoInfo, prop.name, ports, ir.EmptyStmt)
-    backend.generate(skeleton, prop)
+    val state = backend.generate(skeleton, moduleNames, prop)
+    // rename annotations according to the new circuit name
+    val renames = RenameMap(Map(CircuitTarget(state.circuit.main) -> Seq(CircuitTarget(main))))
+    val annos = state.annotations.flatMap(_.update(renames))
+    state.copy(annotations = annos)
   }
 }
diff --git a/src/main/scala/chiseltest/sequences/ConvertCirctSequenceIntrinsics.scala b/src/main/scala/chiseltest/sequences/ConvertCirctSequenceIntrinsics.scala
index a275a9ca8..bd6d29c9d 100644
--- a/src/main/scala/chiseltest/sequences/ConvertCirctSequenceIntrinsics.scala
+++ b/src/main/scala/chiseltest/sequences/ConvertCirctSequenceIntrinsics.scala
@@ -5,12 +5,13 @@
 package chiseltest.sequences
 
 import firrtl2._
-import firrtl2.annotations.{Annotation, CircuitTarget, PresetRegAnnotation}
+import firrtl2.annotations.{Annotation, CircuitTarget, ModuleTarget, PresetRegAnnotation}
 import firrtl2.options.Dependency
 import firrtl2.passes.ExpandWhensAndCheck
 import firrtl2.stage.Forms
 import firrtl2.transforms.DedupModules
 
+import javax.management.RuntimeErrorException
 import scala.collection.mutable
 
 /** Replaces circt sequence intrinsics with a synthesizable version. */
@@ -29,7 +30,10 @@ object ConvertCirctSequenceIntrinsics extends Transform {
   private val LtlDisable = "circt_ltl_disable"
   private val LtlClock = "circt_ltl_clock"
   // Assume, Assert, Cover
-  private val VerifOps = Set("circt_verif_assert", "circt_verif_assume", "circt_verif_cover")
+  private val VerifAssert = "circt_verif_assert"
+  private val VerifAssume = "circt_verif_assume"
+  private val VerifCover = "circt_verif_cover"
+  private val VerifOps = Set(VerifAssert, VerifAssume, VerifCover)
 
   private val Intrinsics = Set(
     HasBeenReset,
@@ -56,12 +60,15 @@ object ConvertCirctSequenceIntrinsics extends Transform {
     // replace intrinsics in modules
     val c = CircuitTarget(state.circuit.main)
     val newAnnos = mutable.ListBuffer[Annotation]()
-    val modules = withoutIntrinsicsModules.map {
+    var moduleNames = state.circuit.modules.map(_.name)
+    val modules = withoutIntrinsicsModules.flatMap {
       case m: ir.Module =>
-        val (mod, annos) = onModule(c, m, intrinsics)
+        val (mod, mods, annos) = onModule(c, m, intrinsics, moduleNames)
         newAnnos ++= annos
-        mod
-      case other => other
+        // update module names
+        moduleNames = moduleNames ++ mods.map(_.name)
+        mod +: mods
+      case other => Seq(other)
     }
 
     val circuit = state.circuit.copy(modules = modules)
@@ -71,21 +78,28 @@ object ConvertCirctSequenceIntrinsics extends Transform {
     state.copy(circuit = circuit, annotations = newAnnos.toSeq ++: state.annotations)
   }
 
-  private def onModule(c: CircuitTarget, m: ir.Module, intrinsics: Map[String, String]): (ir.Module, AnnotationSeq) = {
+  private def onModule(c: CircuitTarget, m: ir.Module, intrinsics: Map[String, String], moduleNames: Seq[String])
+    : (ir.Module, Seq[ir.DefModule], AnnotationSeq) = {
     println(m.serialize)
-    val ctx = Ctx(intrinsics, Namespace(m))
+    val ctx = Ctx(moduleNames, c.module(m.name), intrinsics, Namespace(m))
     val body = onStmt(ctx)(m.body)
-    val newAnnos = ctx.presetRegs.toSeq.map(name => PresetRegAnnotation(c.module(m.name).ref(name)))
     val finalModule = m.copy(body = body)
-    (finalModule, newAnnos)
+    (finalModule, ctx.newModules.toSeq, ctx.newAnnos.toSeq)
   }
 
   private case class IntrinsicInstance(name: String, intrinsic: String, info: ir.Info)
   private case class Ctx(
+    /** allows us to generate new modules that do not have name conflicts */
+    moduleNames: Seq[String],
+    module:      ModuleTarget,
     /** maps the name of a module to the intrinsic it represents */
     moduleToIntrinsic: Map[String, String],
     /** namespace of the current module */
     namespace: Namespace,
+    /** collect modules that implement sequences */
+    newModules: mutable.ListBuffer[ir.DefModule] = mutable.ListBuffer(),
+    /** collect annotations used to implement sequences */
+    newAnnos: mutable.ListBuffer[Annotation] = mutable.ListBuffer(),
     /** maps the name of an instance to the intrinsic that its module represents */
     instToIntrinsic: mutable.HashMap[String, IntrinsicInstance] = mutable.HashMap(),
     /** keeps track of all inputs to intrinsic instances that are regular firrtl expressions */
@@ -94,8 +108,6 @@ object ConvertCirctSequenceIntrinsics extends Transform {
     nodeInputs: mutable.HashMap[(String, String), (Node, PropertyEnv)] = mutable.HashMap(),
     /** Keeps track of any intrinsic outputs that we have generated. Currently only used for `HasBeenReset` */
     outputs: mutable.HashMap[(String, String), ir.Expression] = mutable.HashMap(),
-    /** Keeps track of registers that need to be preset annotated (to implement HasBeenReset) */
-    presetRegs: mutable.ListBuffer[String] = mutable.ListBuffer(),
     /** Avoids duplicate has_been_reset trackers. */
     hasBeenResetCache: mutable.HashMap[(String, String), ir.Expression] = mutable.HashMap()) {
     def isIntrinsicMod(module: String): Boolean = moduleToIntrinsic.contains(module)
@@ -152,7 +164,7 @@ object ConvertCirctSequenceIntrinsics extends Transform {
     // take action according to the intrinsic
     val intrinsicName = ctx.instToIntrinsic(instIn).intrinsic
     if (VerifOps.contains(intrinsicName)) {
-      onVerificationOp(ctx, instIn)
+      onVerificationOp(ctx, instIn, intrinsicName)
     } else {
       ir.EmptyStmt
     }
@@ -174,12 +186,33 @@ object ConvertCirctSequenceIntrinsics extends Transform {
     }
   }
 
-  private def onVerificationOp(ctx: Ctx, inst: String): ir.Statement = {
+  private def onVerificationOp(ctx: Ctx, inst: String, intrinsicName: String): ir.Statement = {
+    val info = ctx.instToIntrinsic(inst).info
     val (prop, propEnv) = ctx.getPropertyTop(inst, "property")
-    val modules = Backend.generate(CurrentBackend, prop)
-    throw new NotImplementedError("TODO: verification op")
+    val op = intrinsicName match {
+      case VerifAssert => AssertOp
+      case VerifAssume => AssumeOp
+      case VerifCover  => CoverOp
+      case _           => throw new RuntimeException(s"Unexpected intrinsic: $intrinsicName")
+    }
+
+    // generate implementation and add to context
+    val moduleNames = ctx.moduleNames ++ ctx.newModules.map(_.name)
+    val state = Backend.generate(CurrentBackend, ctx.module.circuit, moduleNames, prop.copy(op = op))
+    ctx.newModules.addAll(state.circuit.modules)
+    ctx.newAnnos.addAll(state.annotations)
+
+    // instantiate the main verification module
+    val instanceName = ctx.namespace.newName(prop.name + "_" + opToString(op))
+    val main = state.circuit.modules.find(_.name == state.circuit.main).get
+    val instance = ir.DefInstance(info, instanceName, state.circuit.main, Utils.module_type(main))
+    val instanceRef = ir.Reference(instance)
+    val connects = main.ports.map { case ir.Port(_, name, direction, tpe) =>
+      assert(direction == ir.Input)
+      ir.Connect(info, ir.SubField(instanceRef, name, tpe = tpe), propEnv.preds(name))
+    }
 
-    ir.EmptyStmt
+    ir.Block(instance +: connects)
   }
 
   private def onHasBeenResetInput(ctx: Ctx, inst: String): ir.Statement = {
@@ -211,7 +244,7 @@ object ConvertCirctSequenceIntrinsics extends Transform {
     // register starts out as false
     val reg = ir.DefRegister(info, regName, Utils.BoolType, clock, Utils.False(), Utils.False())
     val regRef = ir.Reference(reg).copy(flow = SinkFlow)
-    ctx.presetRegs.addOne(regName)
+    ctx.newAnnos.addOne(PresetRegAnnotation(ctx.module.ref(regName)))
     // when reset becomes true, we set out register to 1
     val update = ir.Conditionally(info, reset, ir.Connect(info, regRef, Utils.True()), ir.EmptyStmt)
     // the output indicates whether the circuits _has been reset_ **and** that reset is not currently active
diff --git a/src/main/scala/chiseltest/sequences/FsmBackend.scala b/src/main/scala/chiseltest/sequences/FsmBackend.scala
index 0d69e24c0..a90493f9c 100644
--- a/src/main/scala/chiseltest/sequences/FsmBackend.scala
+++ b/src/main/scala/chiseltest/sequences/FsmBackend.scala
@@ -3,20 +3,42 @@
 // author: Kevin Laeufer <laeufer@cs.berkeley.edu>
 
 package chiseltest.sequences
-import firrtl2.ir
+import firrtl2.{ir, CircuitState}
 import chisel3._
 import chisel3.util._
+import chiseltest.formal.annotateAsPreset
 import chiseltest.simulator.Compiler
+import firrtl2.options.Dependency
+import firrtl2.stage.Forms
 
 /** Uses Chisel to generate FSMs that implement the Sequence Property */
 object FsmBackend extends Backend {
-  override def generate(skeleton: ir.Module, prop: PropertyTop): Seq[ir.DefModule] = {
+  private val compiler = new firrtl2.stage.transforms.Compiler(Dependency(PrefixModules) +: Forms.Resolved)
+
+  override def generate(skeleton: ir.Module, moduleNames: Seq[String], prop: PropertyTop): CircuitState = {
     val (state, _) = Compiler.elaborate(
-      () => new PropertyFsmAutomaton(prop.predicates, { pred => compileAlways(pred, prop.prop) }),
+      () => new PropertyFsmAutomaton(prop.predicates, prop.op, { pred => compileAlways(pred, prop.prop) }),
       Seq(),
       Seq()
     )
-    state.circuit.modules
+    // add a unique prefix to all modules and make sure that they are type checked before returning them
+    val prefix = genUniquePrefix(moduleNames, prop.name) + "_"
+    val annos = GlobalPrefixAnnotation(prefix) +: state.annotations
+    compiler.transform(state.copy(annotations = annos))
+  }
+
+  private def genUniquePrefix(names: Seq[String], prefix: String): String = {
+    var res = prefix
+    val filteredNames = names.distinct.filter(_.startsWith(prefix))
+    var collisions = filteredNames
+    var count = 0
+    while (collisions.nonEmpty) {
+      res = if (prefix.nonEmpty) { s"${prefix}_$count" }
+      else { count.toString }
+      count += 1
+      collisions = filteredNames.filter(_.startsWith(res))
+    }
+    res
   }
 
   private def compileAlways(pred: Map[String, Bool], p: Property): Bool = {
@@ -65,13 +87,29 @@ object FsmBackend extends Backend {
   }
 }
 
-class PropertyFsmAutomaton(preds: Seq[String], compile: Map[String, Bool] => Bool)
-    extends Module
-    with RequireAsyncReset {
+class PropertyFsmAutomaton(preds: Seq[String], op: VerificationOp, compile: Map[String, Bool] => Bool)
+    extends RawModule {
+  // the clock is provided by the outside
+  val clock = IO(Input(Clock()))
+
+  // all reset values are taken on at the start of simulation
+  val reset = Wire(AsyncReset())
+  annotateAsPreset(reset.toTarget)
+
   val predicates = preds.map { name =>
     name -> IO(Input(Bool())).suggestName(name)
   }
-  val fail = compile(predicates.toMap)
+  val fail = withClockAndReset(clock, reset) { compile(predicates.toMap) }
+
+  val noReset = false.B.asAsyncReset
+  withClockAndReset(clock, noReset) {
+    op match {
+      case AssertOp => assert(!fail)
+      case AssumeOp => assume(!fail)
+      case CoverOp  => cover(fail)
+      case NoOp => throw new RuntimeException("Verification op should have been set by the code invoking the backend!")
+    }
+  }
 }
 
 object SeqRes extends ChiselEnum {
diff --git a/src/main/scala/chiseltest/sequences/HighFirrtlFlatten.scala b/src/main/scala/chiseltest/sequences/HighFirrtlFlatten.scala
new file mode 100644
index 000000000..16eab9e35
--- /dev/null
+++ b/src/main/scala/chiseltest/sequences/HighFirrtlFlatten.scala
@@ -0,0 +1,43 @@
+// Copyright 2023 The Regents of the University of California
+// released under BSD 3-Clause License
+// author: Kevin Laeufer <laeufer@cs.berkeley.edu>
+
+package chiseltest.sequences
+
+import firrtl2._
+import firrtl2.analyses.InstanceKeyGraph
+import firrtl2.stage.Forms
+
+/** Inlines all modules in the circuit into the top. Works on High Firrtl. warn: Currently does not rename any
+  * annotations!
+  */
+object HighFirrtlFlatten extends Transform {
+  override def prerequisites = Forms.Resolved
+  override def invalidates(a: Transform) = false
+  override protected def execute(state: CircuitState): CircuitState = {
+    val iGraph = InstanceKeyGraph(state.circuit)
+    val hasChildren = iGraph.getChildInstances.filter(_._2.nonEmpty).map(_._1).toSet
+    // we visit modules from bottom to top and skip any that do not have children
+    val inlineOrder = iGraph.moduleOrder.reverse.filter(m => hasChildren(m.name)).map(_.asInstanceOf[ir.Module])
+
+    var modules = state.circuit.modules.collect { case m: ir.Module => m.name -> m }.toMap
+    inlineOrder.foreach { mod =>
+      val inlined = inlineModule(modules.get)(mod)
+      modules = modules + (inlined.name -> inlined)
+    }
+    assert(modules.size == 1)
+
+    val circuit = state.circuit.copy(modules = Seq(modules.head._2))
+    state.copy(circuit = circuit)
+  }
+
+  private def inlineModule(getModule: String => Option[ir.Module])(m: ir.Module): ir.Module = {
+    ???
+
+  }
+
+  private def onStmt(namespace: Namespace, getModule: String => Option[ir.Module])(s: ir.Statement): ir.Statement = {
+    ???
+  }
+
+}
diff --git a/src/main/scala/chiseltest/sequences/IR.scala b/src/main/scala/chiseltest/sequences/IR.scala
index dfb409a27..b200cd033 100644
--- a/src/main/scala/chiseltest/sequences/IR.scala
+++ b/src/main/scala/chiseltest/sequences/IR.scala
@@ -35,6 +35,15 @@ case object AssumeOp extends VerificationOp
 case object CoverOp extends VerificationOp
 case object NoOp extends VerificationOp
 
+object opToString {
+  def apply(op: VerificationOp): String = op match {
+    case AssertOp => "assert"
+    case AssumeOp => "assume"
+    case CoverOp  => "cover"
+    case NoOp     => "no"
+  }
+}
+
 case class PropertyTop(
   prop:       Property,
   name:       String = "",
diff --git a/src/main/scala/chiseltest/sequences/PrefixModules.scala b/src/main/scala/chiseltest/sequences/PrefixModules.scala
new file mode 100644
index 000000000..fe3fe5379
--- /dev/null
+++ b/src/main/scala/chiseltest/sequences/PrefixModules.scala
@@ -0,0 +1,51 @@
+// Copyright 2022-2023 The Regents of the University of California
+// released under BSD 3-Clause License
+// author: Kevin Laeufer <laeufer@cs.berkeley.edu>
+
+package chiseltest.sequences
+
+import firrtl2._
+import firrtl2.annotations.{CircuitTarget, NoTargetAnnotation}
+import firrtl2.stage.Forms
+
+private case class GlobalPrefixAnnotation(prefix: String) extends NoTargetAnnotation
+
+/** Simple pass that prefixes _all_ modules in a circuit. */
+private object PrefixModules extends Transform {
+  override def prerequisites = Forms.Resolved
+  override protected def execute(state: CircuitState): CircuitState = {
+    val prefixes = state.annotations.collect { case GlobalPrefixAnnotation(p) => p }.distinct
+    if (prefixes.isEmpty) {
+      return state
+    }
+    assert(!(prefixes.length > 1))
+    run(prefixes.head, state)
+  }
+
+  private def run(prefix: String, state: CircuitState): CircuitState = {
+    val renames = recordRenames(prefix, state.circuit)
+    val modules = state.circuit.modules.map(onModule(prefix))
+    val circuit = state.circuit.copy(modules = modules, main = prefix + state.circuit.main)
+    state.copy(circuit = circuit, renames = Some(renames))
+  }
+
+  private def recordRenames(prefix: String, circuit: ir.Circuit): RenameMap = {
+    val oldC = CircuitTarget(circuit.main)
+    val newC = CircuitTarget(prefix + circuit.main)
+    val renames = Seq(oldC -> Seq(newC)) ++ circuit.modules.map(_.name).map { name =>
+      oldC.module(name) -> Seq(newC.module(prefix + name))
+    }
+    RenameMap(renames.toMap)
+  }
+
+  private def onModule(prefix: String)(m: ir.DefModule): ir.DefModule = m match {
+    case mod: ir.Module    => mod.copy(name = prefix + mod.name).mapStmt(onStmt(prefix))
+    case e:   ir.ExtModule => e.copy(name = prefix + e.name)
+  }
+
+  private def onStmt(prefix: String)(s: ir.Statement): ir.Statement = s match {
+    case d: ir.DefInstance => d.copy(module = prefix + d.module)
+    case other => other.mapStmt(onStmt(prefix))
+  }
+
+}

From 8149205b1802284061ccb47f2d66dc57bd702876 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Kevin=20L=C3=A4ufer?= <laeufer@cs.berkeley.edu>
Date: Wed, 6 Sep 2023 15:27:52 -0400
Subject: [PATCH 07/12] generating code now

---
 .../ConvertCirctSequenceIntrinsics.scala      |  8 ++-----
 .../chiseltest/sequences/FsmBackend.scala     |  5 ++--
 .../tests/SequencePropertyTests.scala         | 24 ++++++++++++++-----
 3 files changed, 23 insertions(+), 14 deletions(-)

diff --git a/src/main/scala/chiseltest/sequences/ConvertCirctSequenceIntrinsics.scala b/src/main/scala/chiseltest/sequences/ConvertCirctSequenceIntrinsics.scala
index bd6d29c9d..1230127e2 100644
--- a/src/main/scala/chiseltest/sequences/ConvertCirctSequenceIntrinsics.scala
+++ b/src/main/scala/chiseltest/sequences/ConvertCirctSequenceIntrinsics.scala
@@ -72,15 +72,11 @@ object ConvertCirctSequenceIntrinsics extends Transform {
     }
 
     val circuit = state.circuit.copy(modules = modules)
-
-    // TODO
-    println(circuit.serialize)
     state.copy(circuit = circuit, annotations = newAnnos.toSeq ++: state.annotations)
   }
 
   private def onModule(c: CircuitTarget, m: ir.Module, intrinsics: Map[String, String], moduleNames: Seq[String])
     : (ir.Module, Seq[ir.DefModule], AnnotationSeq) = {
-    println(m.serialize)
     val ctx = Ctx(moduleNames, c.module(m.name), intrinsics, Namespace(m))
     val body = onStmt(ctx)(m.body)
     val finalModule = m.copy(body = body)
@@ -206,10 +202,10 @@ object ConvertCirctSequenceIntrinsics extends Transform {
     val instanceName = ctx.namespace.newName(prop.name + "_" + opToString(op))
     val main = state.circuit.modules.find(_.name == state.circuit.main).get
     val instance = ir.DefInstance(info, instanceName, state.circuit.main, Utils.module_type(main))
-    val instanceRef = ir.Reference(instance)
+    val instanceRef = ir.Reference(instance).copy(flow = SourceFlow)
     val connects = main.ports.map { case ir.Port(_, name, direction, tpe) =>
       assert(direction == ir.Input)
-      ir.Connect(info, ir.SubField(instanceRef, name, tpe = tpe), propEnv.preds(name))
+      ir.Connect(info, ir.SubField(instanceRef, name, tpe = tpe, flow = SinkFlow), propEnv.preds(name))
     }
 
     ir.Block(instance +: connects)
diff --git a/src/main/scala/chiseltest/sequences/FsmBackend.scala b/src/main/scala/chiseltest/sequences/FsmBackend.scala
index a90493f9c..64e27e374 100644
--- a/src/main/scala/chiseltest/sequences/FsmBackend.scala
+++ b/src/main/scala/chiseltest/sequences/FsmBackend.scala
@@ -22,7 +22,8 @@ object FsmBackend extends Backend {
       Seq()
     )
     // add a unique prefix to all modules and make sure that they are type checked before returning them
-    val prefix = genUniquePrefix(moduleNames, prop.name) + "_"
+    val prefixSeed = if (prop.name.isEmpty) "P" else prop.name // ensure that prefix seed is non-empty
+    val prefix = genUniquePrefix(moduleNames, prefixSeed) + "_"
     val annos = GlobalPrefixAnnotation(prefix) +: state.annotations
     compiler.transform(state.copy(annotations = annos))
   }
@@ -93,7 +94,7 @@ class PropertyFsmAutomaton(preds: Seq[String], op: VerificationOp, compile: Map[
   val clock = IO(Input(Clock()))
 
   // all reset values are taken on at the start of simulation
-  val reset = Wire(AsyncReset())
+  val reset = WireInit(0.B.asAsyncReset)
   annotateAsPreset(reset.toTarget)
 
   val predicates = preds.map { name =>
diff --git a/src/test/scala/chiseltest/tests/SequencePropertyTests.scala b/src/test/scala/chiseltest/tests/SequencePropertyTests.scala
index 30d733d13..3ad5ff128 100644
--- a/src/test/scala/chiseltest/tests/SequencePropertyTests.scala
+++ b/src/test/scala/chiseltest/tests/SequencePropertyTests.scala
@@ -6,17 +6,29 @@ import chisel3._
 import chisel3.ltl._
 import chisel3.ltl.Sequence._
 
-class SimpleAssertionModule extends Module {
+class UnarySequenceModule(impl: Bool => Unit) extends Module {
   val a = IO(Input(Bool()))
-  AssertProperty(a)
-  AssumeProperty(a)
-  CoverProperty(a)
+  impl(a)
 }
 
 /** Make sure that chiselest works with Chisel sequence assertions. */
 class SequencesTests extends AnyFreeSpec with ChiselScalatestTester {
-  "simple assert / assume / cover properties should work" in {
-    test(new SimpleAssertionModule) { dut =>
+  "simple assert properties should work" in {
+    test(new UnarySequenceModule(a => AssertProperty(a))) { dut =>
+      dut.a.poke(true)
+      dut.clock.step()
+    }
+  }
+
+  "simple assume properties should work" in {
+    test(new UnarySequenceModule(a => AssertProperty(a))) { dut =>
+      dut.a.poke(true)
+      dut.clock.step()
+    }
+  }
+
+  "simple cover properties should work" in {
+    test(new UnarySequenceModule(a => CoverProperty(a))) { dut =>
       dut.a.poke(true)
       dut.clock.step()
     }

From 95f1d729be33b0ee61f2f2626ff59a8f7f9252a3 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Kevin=20L=C3=A4ufer?= <laeufer@cs.berkeley.edu>
Date: Wed, 6 Sep 2023 16:25:36 -0400
Subject: [PATCH 08/12] create backend package for sequences

---
 .../ConvertCirctSequenceIntrinsics.scala      |  1 +
 .../sequences/backends/FsmBackend.scala       | 89 +++++++++++++++++++
 .../PropertyFsmAutomaton.scala}               | 84 +----------------
 .../tests/SequencePropertyTests.scala         |  3 +-
 4 files changed, 94 insertions(+), 83 deletions(-)
 create mode 100644 src/main/scala/chiseltest/sequences/backends/FsmBackend.scala
 rename src/main/scala/chiseltest/sequences/{FsmBackend.scala => backends/PropertyFsmAutomaton.scala} (69%)

diff --git a/src/main/scala/chiseltest/sequences/ConvertCirctSequenceIntrinsics.scala b/src/main/scala/chiseltest/sequences/ConvertCirctSequenceIntrinsics.scala
index 1230127e2..2943b3c47 100644
--- a/src/main/scala/chiseltest/sequences/ConvertCirctSequenceIntrinsics.scala
+++ b/src/main/scala/chiseltest/sequences/ConvertCirctSequenceIntrinsics.scala
@@ -4,6 +4,7 @@
 
 package chiseltest.sequences
 
+import chiseltest.sequences.backends.FsmBackend
 import firrtl2._
 import firrtl2.annotations.{Annotation, CircuitTarget, ModuleTarget, PresetRegAnnotation}
 import firrtl2.options.Dependency
diff --git a/src/main/scala/chiseltest/sequences/backends/FsmBackend.scala b/src/main/scala/chiseltest/sequences/backends/FsmBackend.scala
new file mode 100644
index 000000000..094c2111e
--- /dev/null
+++ b/src/main/scala/chiseltest/sequences/backends/FsmBackend.scala
@@ -0,0 +1,89 @@
+// Copyright 2022-2023 The Regents of the University of California
+// released under BSD 3-Clause License
+// author: Kevin Laeufer <laeufer@cs.berkeley.edu>
+
+package chiseltest.sequences.backends
+
+import chisel3._
+import chiseltest.sequences._
+import chiseltest.simulator.Compiler
+import firrtl2.options.Dependency
+import firrtl2.stage.Forms
+import firrtl2.{ir, CircuitState}
+
+/** Uses Chisel to generate FSMs that implement the Sequence Property */
+object FsmBackend extends Backend {
+  private val compiler = new firrtl2.stage.transforms.Compiler(Dependency(PrefixModules) +: Forms.Resolved)
+
+  override def generate(skeleton: ir.Module, moduleNames: Seq[String], prop: PropertyTop): CircuitState = {
+    val (state, _) = Compiler.elaborate(
+      () => new PropertyFsmAutomaton(prop.predicates, prop.op, { pred => compileAlways(pred, prop.prop) }),
+      Seq(),
+      Seq()
+    )
+    // add a unique prefix to all modules and make sure that they are type checked before returning them
+    val prefixSeed = if (prop.name.isEmpty) "P" else prop.name // ensure that prefix seed is non-empty
+    val prefix = genUniquePrefix(moduleNames, prefixSeed) + "_"
+    val annos = GlobalPrefixAnnotation(prefix) +: state.annotations
+    compiler.transform(state.copy(annotations = annos))
+  }
+
+  private def genUniquePrefix(names: Seq[String], prefix: String): String = {
+    var res = prefix
+    val filteredNames = names.distinct.filter(_.startsWith(prefix))
+    var collisions = filteredNames
+    var count = 0
+    while (collisions.nonEmpty) {
+      res = if (prefix.nonEmpty) { s"${prefix}_$count" }
+      else { count.toString }
+      count += 1
+      collisions = filteredNames.filter(_.startsWith(res))
+    }
+    res
+  }
+
+  private def compileAlways(pred: Map[String, Bool], p: Property): Bool = {
+    val n = runtime(p)
+    val props = Seq.fill(n)(comp(pred, p))
+    AssertAlwaysModule(props)
+  }
+
+  private def comp(pred: Map[String, Bool], p: Property): PropertyFsmIO = {
+    p match {
+      case PropSeq(s) => PropSeqModule(comp(pred, s))
+    }
+  }
+
+  private def comp(pred: Map[String, Bool], s: Sequence): SequenceIO = {
+    s match {
+      case SeqPred(predicate)     => SeqExprModule(comp(pred, predicate))
+      case SeqConcat(s1, s2)      => SeqConcatModule(comp(pred, s1), comp(pred, s2))
+      case SeqImpliesNext(s1, p1) => SeqImpliesNextModule(comp(pred, s1), comp(pred, p1))
+    }
+  }
+
+  private def comp(pred: Map[String, Bool], e: BooleanExpr): Bool = e match {
+    case SymbolExpr(name) => pred(name)
+    case NotExpr(e)       => !comp(pred, e)
+    case AndExpr(a, b)    => comp(pred, a) && comp(pred, b)
+    case OrExpr(a, b)     => comp(pred, a) || comp(pred, b)
+  }
+
+  /** calculates an upper bound for the property runtime in cycles */
+  private def runtime(p: Property): Int = {
+    p match {
+      case PropSeq(s) => runtime(s)
+    }
+  }
+
+  /** calculates an upper bound for the sequence runtime in cycles */
+  private def runtime(s: Sequence): Int = {
+    s match {
+      case SeqPred(_)             => 1
+      case SeqOr(s1, s2)          => runtime(s1).max(runtime(s2))
+      case SeqFuse(s1, s2)        => runtime(s1) + runtime(s2) - 1
+      case SeqConcat(s1, s2)      => runtime(s1) + runtime(s2)
+      case SeqImpliesNext(s1, p1) => runtime(s1) + runtime(p1) // TODO: is this correct?
+    }
+  }
+}
diff --git a/src/main/scala/chiseltest/sequences/FsmBackend.scala b/src/main/scala/chiseltest/sequences/backends/PropertyFsmAutomaton.scala
similarity index 69%
rename from src/main/scala/chiseltest/sequences/FsmBackend.scala
rename to src/main/scala/chiseltest/sequences/backends/PropertyFsmAutomaton.scala
index 64e27e374..fd4946940 100644
--- a/src/main/scala/chiseltest/sequences/FsmBackend.scala
+++ b/src/main/scala/chiseltest/sequences/backends/PropertyFsmAutomaton.scala
@@ -1,92 +1,12 @@
 // Copyright 2022-2023 The Regents of the University of California
 // released under BSD 3-Clause License
 // author: Kevin Laeufer <laeufer@cs.berkeley.edu>
+package chiseltest.sequences.backends
 
-package chiseltest.sequences
-import firrtl2.{ir, CircuitState}
 import chisel3._
 import chisel3.util._
 import chiseltest.formal.annotateAsPreset
-import chiseltest.simulator.Compiler
-import firrtl2.options.Dependency
-import firrtl2.stage.Forms
-
-/** Uses Chisel to generate FSMs that implement the Sequence Property */
-object FsmBackend extends Backend {
-  private val compiler = new firrtl2.stage.transforms.Compiler(Dependency(PrefixModules) +: Forms.Resolved)
-
-  override def generate(skeleton: ir.Module, moduleNames: Seq[String], prop: PropertyTop): CircuitState = {
-    val (state, _) = Compiler.elaborate(
-      () => new PropertyFsmAutomaton(prop.predicates, prop.op, { pred => compileAlways(pred, prop.prop) }),
-      Seq(),
-      Seq()
-    )
-    // add a unique prefix to all modules and make sure that they are type checked before returning them
-    val prefixSeed = if (prop.name.isEmpty) "P" else prop.name // ensure that prefix seed is non-empty
-    val prefix = genUniquePrefix(moduleNames, prefixSeed) + "_"
-    val annos = GlobalPrefixAnnotation(prefix) +: state.annotations
-    compiler.transform(state.copy(annotations = annos))
-  }
-
-  private def genUniquePrefix(names: Seq[String], prefix: String): String = {
-    var res = prefix
-    val filteredNames = names.distinct.filter(_.startsWith(prefix))
-    var collisions = filteredNames
-    var count = 0
-    while (collisions.nonEmpty) {
-      res = if (prefix.nonEmpty) { s"${prefix}_$count" }
-      else { count.toString }
-      count += 1
-      collisions = filteredNames.filter(_.startsWith(res))
-    }
-    res
-  }
-
-  private def compileAlways(pred: Map[String, Bool], p: Property): Bool = {
-    val n = runtime(p)
-    val props = Seq.fill(n)(comp(pred, p))
-    AssertAlwaysModule(props)
-  }
-
-  private def comp(pred: Map[String, Bool], p: Property): PropertyFsmIO = {
-    p match {
-      case PropSeq(s) => PropSeqModule(comp(pred, s))
-    }
-  }
-
-  private def comp(pred: Map[String, Bool], s: Sequence): SequenceIO = {
-    s match {
-      case SeqPred(predicate)     => SeqExprModule(comp(pred, predicate))
-      case SeqConcat(s1, s2)      => SeqConcatModule(comp(pred, s1), comp(pred, s2))
-      case SeqImpliesNext(s1, p1) => SeqImpliesNextModule(comp(pred, s1), comp(pred, p1))
-    }
-  }
-
-  private def comp(pred: Map[String, Bool], e: BooleanExpr): Bool = e match {
-    case SymbolExpr(name) => pred(name)
-    case NotExpr(e)       => !comp(pred, e)
-    case AndExpr(a, b)    => comp(pred, a) && comp(pred, b)
-    case OrExpr(a, b)     => comp(pred, a) || comp(pred, b)
-  }
-
-  /** calculates an upper bound for the property runtime in cycles */
-  private def runtime(p: Property): Int = {
-    p match {
-      case PropSeq(s) => runtime(s)
-    }
-  }
-
-  /** calculates an upper bound for the sequence runtime in cycles */
-  private def runtime(s: Sequence): Int = {
-    s match {
-      case SeqPred(_)             => 1
-      case SeqOr(s1, s2)          => runtime(s1).max(runtime(s2))
-      case SeqFuse(s1, s2)        => runtime(s1) + runtime(s2) - 1
-      case SeqConcat(s1, s2)      => runtime(s1) + runtime(s2)
-      case SeqImpliesNext(s1, p1) => runtime(s1) + runtime(p1) // TODO: is this correct?
-    }
-  }
-}
+import chiseltest.sequences.{AssertOp, AssumeOp, CoverOp, NoOp, VerificationOp}
 
 class PropertyFsmAutomaton(preds: Seq[String], op: VerificationOp, compile: Map[String, Bool] => Bool)
     extends RawModule {
diff --git a/src/test/scala/chiseltest/tests/SequencePropertyTests.scala b/src/test/scala/chiseltest/tests/SequencePropertyTests.scala
index 3ad5ff128..b46f43e26 100644
--- a/src/test/scala/chiseltest/tests/SequencePropertyTests.scala
+++ b/src/test/scala/chiseltest/tests/SequencePropertyTests.scala
@@ -14,7 +14,8 @@ class UnarySequenceModule(impl: Bool => Unit) extends Module {
 /** Make sure that chiselest works with Chisel sequence assertions. */
 class SequencesTests extends AnyFreeSpec with ChiselScalatestTester {
   "simple assert properties should work" in {
-    test(new UnarySequenceModule(a => AssertProperty(a))) { dut =>
+    val annos = Seq(VerilatorBackendAnnotation, WriteVcdAnnotation)
+    test(new UnarySequenceModule(a => AssertProperty(a, label = Some("assert_a")))).withAnnotations(annos) { dut =>
       dut.a.poke(true)
       dut.clock.step()
     }

From 7a5d8135c4981041948193fa29bf20cc7a20a657 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Kevin=20L=C3=A4ufer?= <laeufer@cs.berkeley.edu>
Date: Wed, 6 Sep 2023 16:36:54 -0400
Subject: [PATCH 09/12] get simple disable iff working

---
 .../sequences/backends/FsmBackend.scala       |  7 +-
 .../backends/PropertyFsmAutomaton.scala       | 70 ++++++++++---------
 2 files changed, 42 insertions(+), 35 deletions(-)

diff --git a/src/main/scala/chiseltest/sequences/backends/FsmBackend.scala b/src/main/scala/chiseltest/sequences/backends/FsmBackend.scala
index 094c2111e..e6d4c7f65 100644
--- a/src/main/scala/chiseltest/sequences/backends/FsmBackend.scala
+++ b/src/main/scala/chiseltest/sequences/backends/FsmBackend.scala
@@ -17,7 +17,8 @@ object FsmBackend extends Backend {
 
   override def generate(skeleton: ir.Module, moduleNames: Seq[String], prop: PropertyTop): CircuitState = {
     val (state, _) = Compiler.elaborate(
-      () => new PropertyFsmAutomaton(prop.predicates, prop.op, { pred => compileAlways(pred, prop.prop) }),
+      () =>
+        new PropertyFsmAutomaton(prop.predicates, prop.op, { pred => compileAlways(pred, prop.prop, prop.disableIff) }),
       Seq(),
       Seq()
     )
@@ -42,10 +43,10 @@ object FsmBackend extends Backend {
     res
   }
 
-  private def compileAlways(pred: Map[String, Bool], p: Property): Bool = {
+  private def compileAlways(pred: Map[String, Bool], p: Property, disableIff: BooleanExpr): Bool = {
     val n = runtime(p)
     val props = Seq.fill(n)(comp(pred, p))
-    AssertAlwaysModule(props)
+    AssertAlwaysModule(props, comp(pred, disableIff))
   }
 
   private def comp(pred: Map[String, Bool], p: Property): PropertyFsmIO = {
diff --git a/src/main/scala/chiseltest/sequences/backends/PropertyFsmAutomaton.scala b/src/main/scala/chiseltest/sequences/backends/PropertyFsmAutomaton.scala
index fd4946940..17c8addba 100644
--- a/src/main/scala/chiseltest/sequences/backends/PropertyFsmAutomaton.scala
+++ b/src/main/scala/chiseltest/sequences/backends/PropertyFsmAutomaton.scala
@@ -39,6 +39,9 @@ object SeqRes extends ChiselEnum {
 
 class SequenceIO extends Bundle {
 
+  /** disable checking and reset within one cycle */
+  val disable = Input(Bool())
+
   /** is the FSM active this cycle? */
   val advance = Input(Bool())
 
@@ -55,6 +58,9 @@ object PropRes extends ChiselEnum {
 
 class PropertyFsmIO extends Bundle {
 
+  /** disable checking and reset within one cycle */
+  val disable = Input(Bool())
+
   /** is the FSM active this cycle? */
   val advance = Input(Bool())
 
@@ -119,6 +125,14 @@ class SeqConcatModule extends Module {
   }.otherwise {
     io.status := DontCare
   }
+
+  when(io.disable) { // reset registers on disable
+    run1 := false.B
+    run2 := false.B
+  }
+  // propagate disable to sub-sequences
+  seq1.disable := io.disable
+  seq2.disable := io.disable
 }
 
 object SeqConcatModule {
@@ -140,6 +154,8 @@ class PropSeqModule extends Module {
   val io = IO(new PropertyFsmIO)
   // advance is just connected
   seq.advance := io.advance
+  // propagate disable
+  seq.disable := io.disable
 
   when(seq.status.isOneOf(SeqRes.SeqHold, SeqRes.SeqHoldStrong)) {
     io.status := PropRes.PropTrue
@@ -161,34 +177,6 @@ object PropSeqModule {
   }
 }
 
-/** assert a property from the start of reset
-  * @note:
-  *   this is not an always assert, it will only check the property once!
-  */
-class AssertPropModule(desc: String) extends Module {
-  val propertyIO = IO(Flipped(new PropertyFsmIO))
-
-  // the assertion is active starting at reset
-  val going = RegInit(true.B)
-  propertyIO.advance := false.B
-
-  // only advance when reset is false and we are still going
-  when(going && !reset.asBool) {
-    propertyIO.advance := true.B
-    // continue advancing the property while the result is still undetermined
-    going := propertyIO.status === PropRes.PropUndetermined
-    // if the property returns false, this assertion fails
-    assert(propertyIO.status =/= PropRes.PropFalse, desc)
-  }
-}
-
-object AssertPropModule {
-  def apply(p: PropertyFsmIO, desc: String): Unit = {
-    val mod = Module(new AssertPropModule(desc)).suggestName("assert_prop")
-    mod.propertyIO <> p
-  }
-}
-
 object findFirstInactive {
 
   /** return one-hot encoded list with the index of the first active reg turned on */
@@ -202,11 +190,22 @@ object findFirstInactive {
   }
 }
 
+class AssertAlwaysIO extends Bundle {
+
+  /** disable checking and reset within one cycle */
+  val disable = Input(Bool())
+
+  /** indicates that the assertion failed */
+  val fail = Output(Bool())
+}
+
 class AssertAlwaysModule(n: Int) extends Module {
   import PropRes._
 
+  val io = IO(new AssertAlwaysIO)
   val props = IO(Vec(n, Flipped(new PropertyFsmIO)))
-  val fail = IO(Output(Bool()))
+  // propagate disable
+  props.foreach(p => p.disable := io.disable)
 
   val active = RegInit(0.U(n.W))
 
@@ -227,13 +226,20 @@ class AssertAlwaysModule(n: Int) extends Module {
 
   // none of the properties that we advance should be false
   val propFailed = Cat(props.map(p => p.status === PropFalse)) // TODO: reverse?
-  fail := (propFailed & nowActive) =/= 0.U
+  val fail = (propFailed & nowActive) =/= 0.U
+  io.fail := fail && !io.disable
+
+  // reset registers on disable
+  when(io.disable) {
+    active := 0.U
+  }
 }
 
 object AssertAlwaysModule {
-  def apply(props: Seq[PropertyFsmIO]): Bool = {
+  def apply(props: Seq[PropertyFsmIO], disable: Bool): Bool = {
     val mod = Module(new AssertAlwaysModule(props.length))
     mod.props.zip(props).foreach { case (a, b) => a <> b }
-    mod.fail
+    mod.io.disable := disable
+    mod.io.fail
   }
 }

From c498f7456263b99fdf96c699c4a93af6e30e36e4 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Kevin=20L=C3=A4ufer?= <laeufer@cs.berkeley.edu>
Date: Wed, 6 Sep 2023 16:44:35 -0400
Subject: [PATCH 10/12] test to make sure assert fires in correct cycle

---
 src/main/scala/chiseltest/exceptions.scala    |  4 +-
 .../chiseltest/internal/GenericBackend.scala  | 11 ++--
 .../internal/HardwareTesterBackend.scala      |  5 +-
 .../internal/SingleThreadBackend.scala        |  8 +--
 .../sequences/SequencePropertyTests.scala     | 57 +++++++++++++++++++
 .../tests/SequencePropertyTests.scala         | 38 -------------
 6 files changed, 72 insertions(+), 51 deletions(-)
 create mode 100644 src/test/scala/chiseltest/sequences/SequencePropertyTests.scala
 delete mode 100644 src/test/scala/chiseltest/tests/SequencePropertyTests.scala

diff --git a/src/main/scala/chiseltest/exceptions.scala b/src/main/scala/chiseltest/exceptions.scala
index 6e593a3cc..01967be80 100644
--- a/src/main/scala/chiseltest/exceptions.scala
+++ b/src/main/scala/chiseltest/exceptions.scala
@@ -21,10 +21,10 @@ class TimeoutException(message: String)
 class TemporalParadox(message: String) extends Exception(message)
 
 /** Indicates that a Chisel `stop()` statement was triggered. */
-class StopException(message: String) extends Exception(message)
+class StopException(message: String, val cycles: Long) extends Exception(message)
 
 /** Indicates that a Chisel `assert(...)` or `assume(...)` statement has failed. */
-class ChiselAssertionError(message: String) extends Exception(message)
+class ChiselAssertionError(message: String, val cycles: Long) extends Exception(message)
 
 /** Indicates that a value used in a poke/expect is not a literal. It could be hardware or a DontCare which is only
   * allowed when using pokePartial/expectPartial.
diff --git a/src/main/scala/chiseltest/internal/GenericBackend.scala b/src/main/scala/chiseltest/internal/GenericBackend.scala
index 38ed49886..2a45182d7 100644
--- a/src/main/scala/chiseltest/internal/GenericBackend.scala
+++ b/src/main/scala/chiseltest/internal/GenericBackend.scala
@@ -146,13 +146,13 @@ class GenericBackend[T <: Module](
     tester.step() match {
       case StepOk => // all right
         stepCount += 1
-      case StepInterrupted(_, true, _) =>
+      case StepInterrupted(after, true, _) =>
         val msg = s"An assertion in ${dut.name} failed.\n" +
           "Please consult the standard output for more details."
-        throw new ChiselAssertionError(msg)
-      case StepInterrupted(_, false, _) =>
+        throw new ChiselAssertionError(msg, stepCount + after)
+      case StepInterrupted(after, false, _) =>
         val msg = s"A stop() statement was triggered in ${dut.name}."
-        throw new StopException(msg)
+        throw new StopException(msg, stepCount + after)
     }
   }
 
@@ -226,7 +226,8 @@ class GenericBackend[T <: Module](
       } catch {
         case e: TestApplicationException =>
           throw new ChiselAssertionError(
-            s"Simulator exited sooner than expected. See logs for more information about what is assumed to be a Chisel Assertion which failed."
+            s"Simulator exited sooner than expected. See logs for more information about what is assumed to be a Chisel Assertion which failed.",
+            stepCount
           )
       }
     }
diff --git a/src/main/scala/chiseltest/internal/HardwareTesterBackend.scala b/src/main/scala/chiseltest/internal/HardwareTesterBackend.scala
index 7f38cecc5..678253c0a 100644
--- a/src/main/scala/chiseltest/internal/HardwareTesterBackend.scala
+++ b/src/main/scala/chiseltest/internal/HardwareTesterBackend.scala
@@ -74,10 +74,11 @@ object HardwareTesterBackend {
       if (expectFail) {
         throw new StopException(
           "Expected an assertion failure, but encountered a stop instead " +
-            s"after ${i.after} cycles."
+            s"after ${i.after} cycles.",
+          i.after
         )
       } else {
-        throw new ChiselAssertionError(s"Unexpected assertion failure after ${i.after} cycles.")
+        throw new ChiselAssertionError(s"Unexpected assertion failure after ${i.after} cycles.", i.after)
       }
     }
   }
diff --git a/src/main/scala/chiseltest/internal/SingleThreadBackend.scala b/src/main/scala/chiseltest/internal/SingleThreadBackend.scala
index 0426a601b..6064fc7f3 100644
--- a/src/main/scala/chiseltest/internal/SingleThreadBackend.scala
+++ b/src/main/scala/chiseltest/internal/SingleThreadBackend.scala
@@ -90,13 +90,13 @@ class SingleThreadBackend[T <: Module](
         if (timeout > 0 && idleCycles == timeout) {
           throw new TimeoutException(s"timeout on $signal at $timeout idle cycles")
         }
-      case StepInterrupted(_, true, _) =>
+      case StepInterrupted(after, true, _) =>
         val msg = s"An assertion in ${dut.name} failed.\n" +
           "Please consult the standard output for more details."
-        throw new ChiselAssertionError(msg)
-      case StepInterrupted(_, false, _) =>
+        throw new ChiselAssertionError(msg, cycles + after)
+      case StepInterrupted(after, false, _) =>
         val msg = s"A stop() statement was triggered in ${dut.name}."
-        throw new StopException(msg)
+        throw new StopException(msg, cycles + after)
     }
   }
 
diff --git a/src/test/scala/chiseltest/sequences/SequencePropertyTests.scala b/src/test/scala/chiseltest/sequences/SequencePropertyTests.scala
new file mode 100644
index 000000000..9c8a4e84f
--- /dev/null
+++ b/src/test/scala/chiseltest/sequences/SequencePropertyTests.scala
@@ -0,0 +1,57 @@
+// Copyright 2023 The Regents of the University of California
+// released under BSD 3-Clause License
+// author: Kevin Laeufer <laeufer@cs.berkeley.edu>
+
+package chiseltest.sequences
+
+import chisel3._
+import chisel3.ltl.Sequence._
+import chisel3.ltl._
+import chiseltest._
+import org.scalatest.freespec.AnyFreeSpec
+
+class UnarySequenceModule(impl: Bool => Unit) extends Module {
+  val a = IO(Input(Bool()))
+  impl(a)
+}
+
+/** Make sure that chiselest works with Chisel sequence assertions. */
+class BasicTests extends AnyFreeSpec with ChiselScalatestTester {
+  "simple assert properties should work" in {
+    test(new UnarySequenceModule(a => AssertProperty(a, label = Some("assert_a")))) { dut =>
+      dut.a.poke(true)
+      dut.clock.step()
+    }
+  }
+
+  "simple assert should fail in correct cycle" in {
+    val e = intercept[ChiselAssertionError] {
+      test(new UnarySequenceModule(a => AssertProperty(a, label = Some("assert_a")))) { dut =>
+        dut.a.poke(true)
+        dut.clock.step()
+        // no matter how far we step, this should always hold
+        dut.clock.step(4)
+        // but if we poke false, it should fail on the next step
+        dut.a.poke(false)
+        dut.clock.step()
+      }
+    }
+    // one cycle for the implicit reset, plus the 1 + 4 cycles we stepped explicitly
+    assert(e.cycles == 1 + 1 + 4)
+  }
+
+  "simple assume properties should work" in {
+    test(new UnarySequenceModule(a => AssertProperty(a))) { dut =>
+      dut.a.poke(true)
+      dut.clock.step()
+    }
+  }
+
+  "simple cover properties should work" in {
+    test(new UnarySequenceModule(a => CoverProperty(a))) { dut =>
+      dut.a.poke(true)
+      dut.clock.step()
+    }
+  }
+
+}
diff --git a/src/test/scala/chiseltest/tests/SequencePropertyTests.scala b/src/test/scala/chiseltest/tests/SequencePropertyTests.scala
deleted file mode 100644
index b46f43e26..000000000
--- a/src/test/scala/chiseltest/tests/SequencePropertyTests.scala
+++ /dev/null
@@ -1,38 +0,0 @@
-package chiseltest.tests
-
-import org.scalatest.freespec.AnyFreeSpec
-import chiseltest._
-import chisel3._
-import chisel3.ltl._
-import chisel3.ltl.Sequence._
-
-class UnarySequenceModule(impl: Bool => Unit) extends Module {
-  val a = IO(Input(Bool()))
-  impl(a)
-}
-
-/** Make sure that chiselest works with Chisel sequence assertions. */
-class SequencesTests extends AnyFreeSpec with ChiselScalatestTester {
-  "simple assert properties should work" in {
-    val annos = Seq(VerilatorBackendAnnotation, WriteVcdAnnotation)
-    test(new UnarySequenceModule(a => AssertProperty(a, label = Some("assert_a")))).withAnnotations(annos) { dut =>
-      dut.a.poke(true)
-      dut.clock.step()
-    }
-  }
-
-  "simple assume properties should work" in {
-    test(new UnarySequenceModule(a => AssertProperty(a))) { dut =>
-      dut.a.poke(true)
-      dut.clock.step()
-    }
-  }
-
-  "simple cover properties should work" in {
-    test(new UnarySequenceModule(a => CoverProperty(a))) { dut =>
-      dut.a.poke(true)
-      dut.clock.step()
-    }
-  }
-
-}

From 6bfdaece44739248f4aa7a7dbbf1ae297726818d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Kevin=20L=C3=A4ufer?= <laeufer@cs.berkeley.edu>
Date: Wed, 6 Sep 2023 17:01:11 -0400
Subject: [PATCH 11/12] fix warning

---
 .../sequences/ConvertCirctSequenceIntrinsics.scala           | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

diff --git a/src/main/scala/chiseltest/sequences/ConvertCirctSequenceIntrinsics.scala b/src/main/scala/chiseltest/sequences/ConvertCirctSequenceIntrinsics.scala
index 2943b3c47..759524886 100644
--- a/src/main/scala/chiseltest/sequences/ConvertCirctSequenceIntrinsics.scala
+++ b/src/main/scala/chiseltest/sequences/ConvertCirctSequenceIntrinsics.scala
@@ -271,10 +271,7 @@ private object NodeUtils {
     case ref: ir.RefLikeExpression =>
       val name = sanitizeRefName(ref.serialize) // TODO: ensure name is unique!
       (SymbolExpr(name), PropertyEnv(Map(name -> ref)))
-    case other => {
-      other
-      ???
-    }
+    case other => throw new NotImplementedError(s"TODO: implement conversion for: $other")
   }
   def asBooleanExpr(node: Node): Option[BooleanExpr] = node match {
     case expr: BooleanExpr => Some(expr)

From a441234ce4685127d4fff29cb75ad8356ba64f37 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Kevin=20L=C3=A4ufer?= <laeufer@cs.berkeley.edu>
Date: Wed, 6 Sep 2023 17:09:31 -0400
Subject: [PATCH 12/12] fix more warnings

---
 .../scala/chiseltest/sequences/backends/FsmBackend.scala    | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/src/main/scala/chiseltest/sequences/backends/FsmBackend.scala b/src/main/scala/chiseltest/sequences/backends/FsmBackend.scala
index e6d4c7f65..11eff2813 100644
--- a/src/main/scala/chiseltest/sequences/backends/FsmBackend.scala
+++ b/src/main/scala/chiseltest/sequences/backends/FsmBackend.scala
@@ -52,6 +52,7 @@ object FsmBackend extends Backend {
   private def comp(pred: Map[String, Bool], p: Property): PropertyFsmIO = {
     p match {
       case PropSeq(s) => PropSeqModule(comp(pred, s))
+      case other      => throw new NotImplementedError(s"TODO: compile $other")
     }
   }
 
@@ -60,6 +61,7 @@ object FsmBackend extends Backend {
       case SeqPred(predicate)     => SeqExprModule(comp(pred, predicate))
       case SeqConcat(s1, s2)      => SeqConcatModule(comp(pred, s1), comp(pred, s2))
       case SeqImpliesNext(s1, p1) => SeqImpliesNextModule(comp(pred, s1), comp(pred, p1))
+      case other                  => throw new NotImplementedError(s"TODO: compile $other")
     }
   }
 
@@ -68,12 +70,15 @@ object FsmBackend extends Backend {
     case NotExpr(e)       => !comp(pred, e)
     case AndExpr(a, b)    => comp(pred, a) && comp(pred, b)
     case OrExpr(a, b)     => comp(pred, a) || comp(pred, b)
+    case FalseExpr        => false.B
+    case TrueExpr         => false.B
   }
 
   /** calculates an upper bound for the property runtime in cycles */
   private def runtime(p: Property): Int = {
     p match {
       case PropSeq(s) => runtime(s)
+      case other      => throw new NotImplementedError(s"TODO: calculate the runtime of $other")
     }
   }
 
@@ -85,6 +90,7 @@ object FsmBackend extends Backend {
       case SeqFuse(s1, s2)        => runtime(s1) + runtime(s2) - 1
       case SeqConcat(s1, s2)      => runtime(s1) + runtime(s2)
       case SeqImpliesNext(s1, p1) => runtime(s1) + runtime(p1) // TODO: is this correct?
+      case other                  => throw new NotImplementedError(s"TODO: calculate the runtime of $other")
     }
   }
 }