Allow Side Effecting Statement to have Names (#2057)

* firrtl: add optional statement labels for stop, printf, assert, assume and cover

* test: parsing of statement labels

* ir: ensure that name is properly retained

* SymbolTable: add support for labled statements

* test: parsing statement labels

* test: lower types name collisions with named statements

* ignore empty names

* Inline: deal with named and unnamed statements

* RemoveWires: treat stop, printf and verification statements as "others"

* test: fix InlineInstance tests

* DeadCodeEliminations: statements are now als declarations

* CheckHighForm: ensure that statement names are not used as references

* CheckSpec: throw error if statement name collides

* add pass to automatically add missing statement names

* check: make sure that two statements cannot have the same name

* stmtLabel -> stmtName

* scalafmt

* add statement names to spec

* spec: meta data -> metadata

* EnsureStatementNames: explain naming algorithm

* remove returns

* better namespace use

* ir: add CanBeReferenced trait

* ir: add newline as jack requested

20 files changed, 434 insertions, 144 deletions

diff --git a/src/main/antlr4/FIRRTL.g4 b/src/main/antlr4/FIRRTL.g4
index 54ad8d0e..aa53f2f0 100644
--- a/src/main/antlr4/FIRRTL.g4
+++ b/src/main/antlr4/FIRRTL.g4
@@ -103,13 +103,17 @@ stmt
   | exp '<-' exp info?
   | exp 'is' 'invalid' info?
   | when
-  | 'stop(' exp exp intLit ')' info?
-  | 'printf(' exp exp StringLit ( exp)* ')' info?
+  | 'stop(' exp exp intLit ')' stmtName? info?
+  | 'printf(' exp exp StringLit ( exp)* ')' stmtName? info?
   | 'skip' info?
   | 'attach' '(' exp+ ')' info?
-  | 'assert' '(' exp exp exp StringLit ')' info?
-  | 'assume' '(' exp exp exp StringLit ')' info?
-  | 'cover' '(' exp exp exp StringLit ')' info?
+  | 'assert' '(' exp exp exp StringLit ')' stmtName? info?
+  | 'assume' '(' exp exp exp StringLit ')' stmtName? info?
+  | 'cover' '(' exp exp exp StringLit ')' stmtName? info?
+  ;
+
+stmtName
+  : ':' id
   ;
 
 memField
diff --git a/src/main/scala/firrtl/Namespace.scala b/src/main/scala/firrtl/Namespace.scala
index 25f4a805..a4b7bc7a 100644
--- a/src/main/scala/firrtl/Namespace.scala
+++ b/src/main/scala/firrtl/Namespace.scala
@@ -53,9 +53,11 @@ object Namespace {
     val namespace = new Namespace
 
     def buildNamespaceStmt(s: Statement): Seq[String] = s match {
-      case s: IsDeclaration => Seq(s.name)
-      case s: Conditionally => buildNamespaceStmt(s.conseq) ++ buildNamespaceStmt(s.alt)
-      case s: Block         => s.stmts.flatMap(buildNamespaceStmt)
+      // Empty names are allowed for backwards compatibility reasons and
+      // indicate that the entity has essentially no name.
+      case s: IsDeclaration if s.name.nonEmpty => Seq(s.name)
+      case s: Conditionally                    => buildNamespaceStmt(s.conseq) ++ buildNamespaceStmt(s.alt)
+      case s: Block                            => s.stmts.flatMap(buildNamespaceStmt)
       case _ => Nil
     }
     namespace.namespace ++= m.ports.map(_.name)
diff --git a/src/main/scala/firrtl/Visitor.scala b/src/main/scala/firrtl/Visitor.scala
index dadcac46..f1b3a5c2 100644
--- a/src/main/scala/firrtl/Visitor.scala
+++ b/src/main/scala/firrtl/Visitor.scala
@@ -318,6 +318,7 @@ class Visitor(infoMode: InfoMode) extends AbstractParseTreeVisitor[FirrtlNode] w
   private def visitStmt(ctx: StmtContext): Statement = {
     val ctx_exp = ctx.exp.asScala
     val info = visitInfo(Option(ctx.info), ctx)
+    def stmtName = Option(ctx.stmtName).map(_.id.getText).getOrElse("")
     ctx.getChild(0) match {
       case when: WhenContext => visitWhen(when)
       case term: TerminalNode =>
@@ -346,7 +347,8 @@ class Visitor(infoMode: InfoMode) extends AbstractParseTreeVisitor[FirrtlNode] w
           case "inst" => DefInstance(info, ctx.id(0).getText, ctx.id(1).getText)
           case "node" => DefNode(info, ctx.id(0).getText, visitExp(ctx_exp(0)))
 
-          case "stop("  => Stop(info, string2Int(ctx.intLit().getText), visitExp(ctx_exp(0)), visitExp(ctx_exp(1)))
+          case "stop(" =>
+            Stop(info, string2Int(ctx.intLit().getText), visitExp(ctx_exp(0)), visitExp(ctx_exp(1)), name = stmtName)
           case "attach" => Attach(info, ctx_exp.map(visitExp).toSeq)
           case "printf(" =>
             Print(
@@ -354,7 +356,8 @@ class Visitor(infoMode: InfoMode) extends AbstractParseTreeVisitor[FirrtlNode] w
               visitStringLit(ctx.StringLit),
               ctx_exp.drop(2).map(visitExp).toSeq,
               visitExp(ctx_exp(0)),
-              visitExp(ctx_exp(1))
+              visitExp(ctx_exp(1)),
+              name = stmtName
             )
           // formal
           case "assert" =>
@@ -364,7 +367,8 @@ class Visitor(infoMode: InfoMode) extends AbstractParseTreeVisitor[FirrtlNode] w
               visitExp(ctx_exp(0)),
               visitExp(ctx_exp(1)),
               visitExp(ctx_exp(2)),
-              visitStringLit(ctx.StringLit)
+              visitStringLit(ctx.StringLit),
+              name = stmtName
             )
           case "assume" =>
             Verification(
@@ -373,7 +377,8 @@ class Visitor(infoMode: InfoMode) extends AbstractParseTreeVisitor[FirrtlNode] w
               visitExp(ctx_exp(0)),
               visitExp(ctx_exp(1)),
               visitExp(ctx_exp(2)),
-              visitStringLit(ctx.StringLit)
+              visitStringLit(ctx.StringLit),
+              name = stmtName
             )
           case "cover" =>
             Verification(
@@ -382,7 +387,8 @@ class Visitor(infoMode: InfoMode) extends AbstractParseTreeVisitor[FirrtlNode] w
               visitExp(ctx_exp(0)),
               visitExp(ctx_exp(1)),
               visitExp(ctx_exp(2)),
-              visitStringLit(ctx.StringLit)
+              visitStringLit(ctx.StringLit),
+              name = stmtName
             )
           // end formal
           case "skip" => EmptyStmt
diff --git a/src/main/scala/firrtl/WIR.scala b/src/main/scala/firrtl/WIR.scala
index a0b85007..78536a36 100644
--- a/src/main/scala/firrtl/WIR.scala
+++ b/src/main/scala/firrtl/WIR.scala
@@ -119,6 +119,7 @@ case class WDefInstanceConnector(
   portCons: Seq[(Expression, Expression)])
     extends Statement
     with IsDeclaration
+    with CanBeReferenced
     with UseSerializer {
   def mapExpr(f: Expression => Expression): Statement =
     this.copy(portCons = portCons.map { case (e1, e2) => (f(e1), f(e2)) })
@@ -346,6 +347,7 @@ case class CDefMemory(
   readUnderWrite: ReadUnderWrite.Value = ReadUnderWrite.Undefined)
     extends Statement
     with HasInfo
+    with CanBeReferenced
     with UseSerializer {
   def mapExpr(f:       Expression => Expression): Statement = this
   def mapStmt(f:       Statement => Statement):   Statement = this
@@ -361,6 +363,7 @@ case class CDefMemory(
 case class CDefMPort(info: Info, name: String, tpe: Type, mem: String, exps: Seq[Expression], direction: MPortDir)
     extends Statement
     with HasInfo
+    with CanBeReferenced
     with UseSerializer {
   def mapExpr(f:       Expression => Expression): Statement = this.copy(exps = exps.map(f))
   def mapStmt(f:       Statement => Statement):   Statement = this
diff --git a/src/main/scala/firrtl/analyses/SymbolTable.scala b/src/main/scala/firrtl/analyses/SymbolTable.scala
index 3b304bc1..e4a53444 100644
--- a/src/main/scala/firrtl/analyses/SymbolTable.scala
+++ b/src/main/scala/firrtl/analyses/SymbolTable.scala
@@ -87,6 +87,10 @@ object SymbolTable {
     case d: DefNode     => table.declare(d)
     case d: DefWire     => table.declare(d)
     case d: DefRegister => table.declare(d)
+    // Matches named statements like printf, stop, assert, assume, cover if the name is not empty.
+    // Empty names are allowed for backwards compatibility reasons and
+    // indicate that the entity has essentially no name.
+    case s: IsDeclaration if s.name.nonEmpty => table.declare(s.name, UnknownType, firrtl.UnknownKind)
     case other => other.foreachStmt(scanStatement)
   }
 }
diff --git a/src/main/scala/firrtl/graph/DiGraph.scala b/src/main/scala/firrtl/graph/DiGraph.scala
index 9f6ffeb2..99bf8403 100644
--- a/src/main/scala/firrtl/graph/DiGraph.scala
+++ b/src/main/scala/firrtl/graph/DiGraph.scala
@@ -423,8 +423,7 @@ class DiGraph[T](private[graph] val edges: LinkedHashMap[T, LinkedHashSet[T]]) {
             rec(nextTab, nodex, nextMark + " ", acc)
         }
     }
-    this.findSources
-      .toList // Convert LinkedHashSet to List to avoid determinism issues
+    this.findSources.toList // Convert LinkedHashSet to List to avoid determinism issues
       .sortBy(_.toString) // Make order deterministic
       .foldLeft(Nil: List[String]) {
         case (acc, root) => rec("", root, "", acc)
diff --git a/src/main/scala/firrtl/ir/IR.scala b/src/main/scala/firrtl/ir/IR.scala
index 1b564d42..9c3d6186 100644
--- a/src/main/scala/firrtl/ir/IR.scala
+++ b/src/main/scala/firrtl/ir/IR.scala
@@ -4,7 +4,7 @@ package firrtl
 package ir
 
 import Utils.{dec2string, trim}
-import dataclass.data
+import dataclass.{data, since}
 import firrtl.constraint.{Constraint, IsKnown, IsVar}
 import org.apache.commons.text.translate.{AggregateTranslator, JavaUnicodeEscaper, LookupTranslator}
 
@@ -227,6 +227,13 @@ abstract class Expression extends FirrtlNode {
   */
 sealed trait RefLikeExpression extends Expression { def flow: Flow }
 
+/** Represents a statement that can be referenced in a firrtl expression.
+  * This explicitly excludes named side-effecting statements like Print, Stop and Verification.
+  * Note: This trait cannot be sealed since the memory ports are declared in WIR.scala.
+  *       Once we fully remove all WIR, this trait could be sealed.
+  */
+trait CanBeReferenced
+
 object Reference {
 
   /** Creates a Reference from a Wire */
@@ -387,7 +394,11 @@ abstract class Statement extends FirrtlNode {
   def foreachString(f: String => Unit):           Unit
   def foreachInfo(f:   Info => Unit):             Unit
 }
-case class DefWire(info: Info, name: String, tpe: Type) extends Statement with IsDeclaration with UseSerializer {
+case class DefWire(info: Info, name: String, tpe: Type)
+    extends Statement
+    with IsDeclaration
+    with CanBeReferenced
+    with UseSerializer {
   def mapStmt(f:       Statement => Statement):   Statement = this
   def mapExpr(f:       Expression => Expression): Statement = this
   def mapType(f:       Type => Type):             Statement = DefWire(info, name, f(tpe))
@@ -408,6 +419,7 @@ case class DefRegister(
   init:  Expression)
     extends Statement
     with IsDeclaration
+    with CanBeReferenced
     with UseSerializer {
   def mapStmt(f: Statement => Statement): Statement = this
   def mapExpr(f: Expression => Expression): Statement =
@@ -429,6 +441,7 @@ object DefInstance {
 case class DefInstance(info: Info, name: String, module: String, tpe: Type = UnknownType)
     extends Statement
     with IsDeclaration
+    with CanBeReferenced
     with UseSerializer {
   def mapExpr(f:       Expression => Expression): Statement = this
   def mapStmt(f:       Statement => Statement):   Statement = this
@@ -462,6 +475,7 @@ case class DefMemory(
   readUnderWrite: ReadUnderWrite.Value = ReadUnderWrite.Undefined)
     extends Statement
     with IsDeclaration
+    with CanBeReferenced
     with UseSerializer {
   def mapStmt(f:       Statement => Statement):   Statement = this
   def mapExpr(f:       Expression => Expression): Statement = this
@@ -477,6 +491,7 @@ case class DefMemory(
 case class DefNode(info: Info, name: String, value: Expression)
     extends Statement
     with IsDeclaration
+    with CanBeReferenced
     with UseSerializer {
   def mapStmt(f:       Statement => Statement):   Statement = this
   def mapExpr(f:       Expression => Expression): Statement = DefNode(info, name, f(value))
@@ -594,22 +609,24 @@ case class Attach(info: Info, exprs: Seq[Expression]) extends Statement with Has
   def foreachString(f: String => Unit):           Unit = ()
   def foreachInfo(f:   Info => Unit):             Unit = f(info)
 }
-@data class Stop(info: Info, ret: Int, clk: Expression, en: Expression)
+
+@data class Stop(info: Info, ret: Int, clk: Expression, en: Expression, @since("FIRRTL 1.5") name: String = "")
     extends Statement
     with HasInfo
+    with IsDeclaration
     with UseSerializer {
   def mapStmt(f:     Statement => Statement):   Statement = this
-  def mapExpr(f:     Expression => Expression): Statement = Stop(info, ret, f(clk), f(en))
+  def mapExpr(f:     Expression => Expression): Statement = Stop(info, ret, f(clk), f(en), name)
   def mapType(f:     Type => Type):             Statement = this
-  def mapString(f:   String => String):         Statement = this
+  def mapString(f:   String => String):         Statement = withName(f(name))
   def mapInfo(f:     Info => Info):             Statement = this.copy(info = f(info))
   def foreachStmt(f: Statement => Unit):        Unit = ()
   def foreachExpr(f: Expression => Unit): Unit = { f(clk); f(en) }
   def foreachType(f:   Type => Unit):   Unit = ()
-  def foreachString(f: String => Unit): Unit = ()
+  def foreachString(f: String => Unit): Unit = f(name)
   def foreachInfo(f:   Info => Unit):   Unit = f(info)
   def copy(info: Info = info, ret: Int = ret, clk: Expression = clk, en: Expression = en): Stop = {
-    Stop(info, ret, clk, en)
+    Stop(info, ret, clk, en, name)
   }
 }
 object Stop {
@@ -622,19 +639,22 @@ object Stop {
   string: StringLit,
   args:   Seq[Expression],
   clk:    Expression,
-  en:     Expression)
+  en:     Expression,
+  @since("FIRRTL 1.5")
+  name: String = "")
     extends Statement
     with HasInfo
+    with IsDeclaration
     with UseSerializer {
   def mapStmt(f:     Statement => Statement):   Statement = this
-  def mapExpr(f:     Expression => Expression): Statement = Print(info, string, args.map(f), f(clk), f(en))
+  def mapExpr(f:     Expression => Expression): Statement = Print(info, string, args.map(f), f(clk), f(en), name)
   def mapType(f:     Type => Type):             Statement = this
-  def mapString(f:   String => String):         Statement = this
+  def mapString(f:   String => String):         Statement = withName(f(name))
   def mapInfo(f:     Info => Info):             Statement = this.copy(info = f(info))
   def foreachStmt(f: Statement => Unit):        Unit = ()
   def foreachExpr(f: Expression => Unit): Unit = { args.foreach(f); f(clk); f(en) }
   def foreachType(f:   Type => Unit):   Unit = ()
-  def foreachString(f: String => Unit): Unit = ()
+  def foreachString(f: String => Unit): Unit = f(name)
   def foreachInfo(f:   Info => Unit):   Unit = f(info)
   def copy(
     info:   Info = info,
@@ -643,7 +663,7 @@ object Stop {
     clk:    Expression = clk,
     en:     Expression = en
   ): Print = {
-    Print(info, string, args, clk, en)
+    Print(info, string, args, clk, en, name)
   }
 }
 object Print {
@@ -665,20 +685,23 @@ object Formal extends Enumeration {
   clk:  Expression,
   pred: Expression,
   en:   Expression,
-  msg:  StringLit)
+  msg:  StringLit,
+  @since("FIRRTL 1.5")
+  name: String = "")
     extends Statement
     with HasInfo
+    with IsDeclaration
     with UseSerializer {
   def mapStmt(f: Statement => Statement): Statement = this
   def mapExpr(f: Expression => Expression): Statement =
     copy(clk = f(clk), pred = f(pred), en = f(en))
   def mapType(f:     Type => Type):      Statement = this
-  def mapString(f:   String => String):  Statement = this
+  def mapString(f:   String => String):  Statement = withName(f(name))
   def mapInfo(f:     Info => Info):      Statement = copy(info = f(info))
   def foreachStmt(f: Statement => Unit): Unit = ()
   def foreachExpr(f: Expression => Unit): Unit = { f(clk); f(pred); f(en); }
   def foreachType(f:   Type => Unit):   Unit = ()
-  def foreachString(f: String => Unit): Unit = ()
+  def foreachString(f: String => Unit): Unit = f(name)
   def foreachInfo(f:   Info => Unit):   Unit = f(info)
   def copy(
     op:   Formal.Value = op,
@@ -688,7 +711,7 @@ object Formal extends Enumeration {
     en:   Expression = en,
     msg:  StringLit = msg
   ): Verification = {
-    Verification(op, info, clk, pred, en, msg)
+    Verification(op, info, clk, pred, en, msg, name)
   }
 }
 object Verification {
@@ -1016,6 +1039,7 @@ case class Port(
   tpe:       Type)
     extends FirrtlNode
     with IsDeclaration
+    with CanBeReferenced
     with UseSerializer {
   def mapType(f:   Type => Type):     Port = Port(info, name, direction, f(tpe))
   def mapString(f: String => String): Port = Port(info, f(name), direction, tpe)
diff --git a/src/main/scala/firrtl/ir/Serializer.scala b/src/main/scala/firrtl/ir/Serializer.scala
index 983a7866..caea0a9c 100644
--- a/src/main/scala/firrtl/ir/Serializer.scala
+++ b/src/main/scala/firrtl/ir/Serializer.scala
@@ -102,11 +102,13 @@ object Serializer {
         s(it.next())
         if (it.hasNext) newLineAndIndent()
       }
-    case Stop(info, ret, clk, en) =>
-      b ++= "stop("; s(clk); b ++= ", "; s(en); b ++= ", "; b ++= ret.toString; b += ')'; s(info)
-    case Print(info, string, args, clk, en) =>
+    case stop @ Stop(info, ret, clk, en) =>
+      b ++= "stop("; s(clk); b ++= ", "; s(en); b ++= ", "; b ++= ret.toString; b += ')'
+      sStmtName(stop.name); s(info)
+    case print @ Print(info, string, args, clk, en) =>
       b ++= "printf("; s(clk); b ++= ", "; s(en); b ++= ", "; b ++= string.escape
-      if (args.nonEmpty) b ++= ", "; s(args, ", "); b += ')'; s(info)
+      if (args.nonEmpty) b ++= ", "; s(args, ", "); b += ')'
+      sStmtName(print.name); s(info)
     case IsInvalid(info, expr)    => s(expr); b ++= " is invalid"; s(info)
     case DefWire(info, name, tpe) => b ++= "wire "; b ++= name; b ++= " : "; s(tpe); s(info)
     case DefRegister(info, name, tpe, clock, reset, init) =>
@@ -138,9 +140,9 @@ object Serializer {
     case Attach(info, exprs)             =>
       // exprs should never be empty since the attach statement takes *at least* two signals according to the spec
       b ++= "attach ("; s(exprs, ", "); b += ')'; s(info)
-    case Verification(op, info, clk, pred, en, msg) =>
+    case veri @ Verification(op, info, clk, pred, en, msg) =>
       b ++= op.toString; b += '('; s(List(clk, pred, en), ", ", false); b ++= msg.escape
-      b += ')'; s(info)
+      b += ')'; sStmtName(veri.name); s(info)
 
     // WIR
     case firrtl.CDefMemory(info, name, tpe, size, seq, readUnderWrite) =>
@@ -155,6 +157,10 @@ object Serializer {
     case other => b ++= other.serialize // Handle user-defined nodes
   }
 
+  private def sStmtName(lbl: String)(implicit b: StringBuilder): Unit = {
+    if (lbl.nonEmpty) { b ++= s" : $lbl" }
+  }
+
   private def s(node: Width)(implicit b: StringBuilder, indent: Int): Unit = node match {
     case IntWidth(width) => b += '<'; b ++= width.toString(); b += '>'
     case UnknownWidth    => // empty string
diff --git a/src/main/scala/firrtl/passes/CheckHighForm.scala b/src/main/scala/firrtl/passes/CheckHighForm.scala
index e3468c4e..05635d00 100644
--- a/src/main/scala/firrtl/passes/CheckHighForm.scala
+++ b/src/main/scala/firrtl/passes/CheckHighForm.scala
@@ -22,6 +22,10 @@ trait CheckHighFormLike { this: Pass =>
       moduleNS += name
       scopes.head += name
     }
+    // ensures that the name cannot be used again, but prevent references to this name
+    def addToNamespace(name: String): Unit = {
+      moduleNS += name
+    }
     def expandMPortVisibility(port: CDefMPort): Unit = {
       // Legacy CHIRRTL ports are visible in any scope where their parent memory is visible
       scopes.find(_.contains(port.mem)).getOrElse(scopes.head) += port.name
@@ -250,10 +254,19 @@ trait CheckHighFormLike { this: Pass =>
       e.foreach(checkHighFormE(info, mname, names))
     }
 
-    def checkName(info: Info, mname: String, names: ScopeView)(name: String): Unit = {
-      if (!names.legalDecl(name))
-        errors.append(new NotUniqueException(info, mname, name))
-      names.declare(name)
+    def checkName(info: Info, mname: String, names: ScopeView, canBeReference: Boolean)(name: String): Unit = {
+      // Empty names are allowed for backwards compatibility reasons and
+      // indicate that the entity has essentially no name.
+      if (name.isEmpty) { assert(!canBeReference, "A statement with an empty name cannot be used as a reference!") }
+      else {
+        if (!names.legalDecl(name))
+          errors.append(new NotUniqueException(info, mname, name))
+        if (canBeReference) {
+          names.declare(name)
+        } else {
+          names.addToNamespace(name)
+        }
+      }
     }
 
     def checkInstance(info: Info, child: String, parent: String): Unit = {
@@ -270,7 +283,11 @@ trait CheckHighFormLike { this: Pass =>
         case NoInfo => minfo
         case x      => x
       }
-      s.foreach(checkName(info, mname, names))
+      val canBeReference = s match {
+        case _: CanBeReferenced => true
+        case _ => false
+      }
+      s.foreach(checkName(info, mname, names, canBeReference))
       s match {
         case DefRegister(info, name, tpe, _, reset, init) =>
           if (hasFlip(tpe))
diff --git a/src/main/scala/firrtl/passes/Inline.scala b/src/main/scala/firrtl/passes/Inline.scala
index 4eba5d59..912acf8e 100644
--- a/src/main/scala/firrtl/passes/Inline.scala
+++ b/src/main/scala/firrtl/passes/Inline.scala
@@ -187,18 +187,23 @@ class InlineInstances extends Transform with DependencyAPIMigration with Registe
       renameMap:     RenameMap
     )(s:             Statement
     ): Statement = {
-      def onName(ofModuleOpt: Option[String])(name: String) = {
-        if (prefix.nonEmpty && !ns.tryName(prefix + name)) {
-          throw new Exception(s"Inlining failed. Inlined name '${prefix + name}' already exists")
-        }
-        ofModuleOpt match {
-          case None =>
-            renameMap.record(currentModule.ref(name), nextModule.ref(prefix + name))
-          case Some(ofModule) =>
-            renameMap.record(currentModule.instOf(name, ofModule), nextModule.instOf(prefix + name, ofModule))
+      def onName(ofModuleOpt: Option[String])(name: String): String = {
+        // Empty names are allowed for backwards compatibility reasons and
+        // indicate that the entity has essentially no name and thus cannot be prefixed.
+        if (name.isEmpty) { name }
+        else {
+          if (prefix.nonEmpty && !ns.tryName(prefix + name)) {
+            throw new Exception(s"Inlining failed. Inlined name '${prefix + name}' already exists")
+          }
+          ofModuleOpt match {
+            case None =>
+              renameMap.record(currentModule.ref(name), nextModule.ref(prefix + name))
+            case Some(ofModule) =>
+              renameMap.record(currentModule.instOf(name, ofModule), nextModule.instOf(prefix + name, ofModule))
+          }
+          renames(name) = prefix + name
+          prefix + name
         }
-        renames(name) = prefix + name
-        prefix + name
       }
 
       s match {
diff --git a/src/main/scala/firrtl/transforms/DeadCodeElimination.scala b/src/main/scala/firrtl/transforms/DeadCodeElimination.scala
index 13173fdd..1d9bfd0e 100644
--- a/src/main/scala/firrtl/transforms/DeadCodeElimination.scala
+++ b/src/main/scala/firrtl/transforms/DeadCodeElimination.scala
@@ -258,6 +258,11 @@ class DeadCodeElimination extends Transform with RegisteredTransform with Depend
               renames.delete(inst.name)
               EmptyStmt
           }
+        case print:  Print        => deleteIfNotEnabled(print, print.en)
+        case stop:   Stop         => deleteIfNotEnabled(stop, stop.en)
+        case formal: Verification => deleteIfNotEnabled(formal, formal.en)
+        // Statements are also declarations and thus this case needs to come *after* checking the
+        // print, stop and verification statements.
         case decl: IsDeclaration =>
           val node = LogicNode(mod.name, decl.name)
           if (deadNodes.contains(node)) {
@@ -265,10 +270,7 @@ class DeadCodeElimination extends Transform with RegisteredTransform with Depend
             renames.delete(decl.name)
             EmptyStmt
           } else decl
-        case print:  Print => deleteIfNotEnabled(print, print.en)
-        case stop:   Stop  => deleteIfNotEnabled(stop, stop.en)
-        case formal: Verification => deleteIfNotEnabled(formal, formal.en)
-        case con:    Connect =>
+        case con: Connect =>
           val node = getDeps(con.loc) match { case Seq(elt) => elt }
           if (deadNodes.contains(node)) EmptyStmt else con
         case Attach(info, exprs) => // If any exprs are dead then all are
diff --git a/src/main/scala/firrtl/transforms/EnsureNamedStatements.scala b/src/main/scala/firrtl/transforms/EnsureNamedStatements.scala
new file mode 100644
index 00000000..a40409f9
--- /dev/null
+++ b/src/main/scala/firrtl/transforms/EnsureNamedStatements.scala
@@ -0,0 +1,39 @@
+// SPDX-License-Identifier: Apache-2.0
+
+package firrtl.transforms
+
+import firrtl._
+import firrtl.ir._
+
+/** Adds default names to print, stop and verification statements if their name is empty. */
+object EnsureNamedStatements extends Transform with DependencyAPIMigration {
+  override def invalidates(a: Transform) = false
+
+  override protected def execute(state: CircuitState): CircuitState = {
+    val c = state.circuit.mapModule(onModule)
+    state.copy(circuit = c)
+  }
+
+  private def onModule(m: DefModule): DefModule = m match {
+    case e:   ExtModule => e
+    case mod: Module =>
+      val namespace = Namespace(mod)
+      // Ensure we always start with _0 suffix
+      val prefixes = Seq("cover", "assert", "assume", "print", "stop")
+      prefixes.filterNot(namespace.contains).foreach(namespace.newName)
+      mod.mapStmt(onStmt(namespace))
+  }
+
+  private def onStmt(namespace: Namespace)(stmt: Statement): Statement = stmt match {
+    case s: Print if s.name.isEmpty => s.withName(namespace.newName("print"))
+    case s: Stop if s.name.isEmpty => s.withName(namespace.newName("stop"))
+    case s: Verification if s.name.isEmpty =>
+      val baseName = s.op match {
+        case Formal.Cover  => "cover"
+        case Formal.Assert => "assert"
+        case Formal.Assume => "assume"
+      }
+      s.withName(namespace.newName(baseName))
+    case other => other.mapStmt(onStmt(namespace))
+  }
+}
diff --git a/src/main/scala/firrtl/transforms/RemoveWires.scala b/src/main/scala/firrtl/transforms/RemoveWires.scala
index ee03ad30..f2907db2 100644
--- a/src/main/scala/firrtl/transforms/RemoveWires.scala
+++ b/src/main/scala/firrtl/transforms/RemoveWires.scala
@@ -115,7 +115,10 @@ class RemoveWires extends Transform with DependencyAPIMigration {
           val initDep = Some(reg.init).filter(we(WRef(reg)) != we(_)) // Dependency exists IF reg doesn't init itself
           regInfo(we(WRef(reg))) = reg
           netlist(we(WRef(reg))) = (Seq(reg.clock) ++ resetDep ++ initDep, reg.info)
-        case decl: IsDeclaration => // Keep all declarations except for nodes and non-Analog wires
+        case decl: CanBeReferenced =>
+          // Keep all declarations except for nodes and non-Analog wires and "other" statements.
+          // Thus this is expected to match DefInstance and DefMemory which both do not connect to
+          // any signals directly (instead a separate Connect is used).
           decls += decl
         case con @ Connect(cinfo, lhs, rhs) =>
           kind(lhs) match {
diff --git a/src/test/scala/firrtl/testutils/FirrtlSpec.scala b/src/test/scala/firrtl/testutils/FirrtlSpec.scala
index 6de2af1e..24793437 100644
--- a/src/test/scala/firrtl/testutils/FirrtlSpec.scala
+++ b/src/test/scala/firrtl/testutils/FirrtlSpec.scala
@@ -123,21 +123,21 @@ trait FirrtlRunners extends BackendCompilationUtilities {
   }
 
   /** Check equivalence of Firrtl with reference Verilog
-   *
+    *
     * @note the name of the reference Verilog module is grabbed via regex
     * @param inputFirrtl string containing Firrtl source
     * @param referenceVerilog Verilog that will be used as reference for LEC
     * @param timesteps the maximum number of timesteps to consider
     */
   def firrtlEquivalenceWithVerilog(
-    inputFirrtl:       String,
-    referenceVerilog:  String,
-    timesteps:         Int = 1
+    inputFirrtl:      String,
+    referenceVerilog: String,
+    timesteps:        Int = 1
   ): Unit = {
     val VerilogModule = """(?s).*module\s(\w+).*""".r
     val refName = referenceVerilog match {
       case VerilogModule(name) => name
-      case _ => throw new Exception(s"Reference Verilog must match simple regex! $VerilogModule")
+      case _                   => throw new Exception(s"Reference Verilog must match simple regex! $VerilogModule")
     }
     val circuit = Parser.parse(inputFirrtl.split("\n").toIterator)
     val inputName = circuit.main
@@ -163,7 +163,6 @@ trait FirrtlRunners extends BackendCompilationUtilities {
     assert(BackendCompilationUtilities.yosysExpectSuccess(inputName, refName, testDir, timesteps))
   }
 
-
   /** Compiles input Firrtl to Verilog */
   def compileToVerilog(input: String, annotations: AnnotationSeq = Seq.empty): String = {
     val circuit = Parser.parse(input.split("\n").toIterator)
diff --git a/src/test/scala/firrtl/transforms/EnsureNamedStatementsSpec.scala b/src/test/scala/firrtl/transforms/EnsureNamedStatementsSpec.scala
new file mode 100644
index 00000000..4c993994
--- /dev/null
+++ b/src/test/scala/firrtl/transforms/EnsureNamedStatementsSpec.scala
@@ -0,0 +1,39 @@
+// SPDX-License-Identifier: Apache-2.0
+
+package firrtl.transforms
+
+import firrtl.options.Dependency
+import firrtl.testutils.LeanTransformSpec
+
+class EnsureNamedStatementsSpec extends LeanTransformSpec(Seq(Dependency(EnsureNamedStatements))) {
+  behavior.of("EnsureNamedStatements")
+
+  it should "automatically name statements that do not have a name yet" in {
+    val src = """circuit test :
+                |  module test :
+                |    input clock : Clock
+                |    input stop_ : UInt<1>
+                |    assert(clock, UInt(1), not(UInt(0)), "")
+                |    stop(clock, UInt(1), 1) : stop_123
+                |    stop(clock, UInt(1), 1)
+                |    assert(clock, UInt(0), UInt(0), "")
+                |    assume(clock, UInt(0), UInt(0), "")
+                |    cover(clock, UInt(0), UInt(0), "")
+                |    cover(clock, UInt(0), UInt(0), "")
+                |
+                |""".stripMargin
+
+    val result = compile(src, List()).circuit.serialize.split('\n').map(_.trim)
+
+    val expected = List(
+      """assert(clock, UInt<1>("h1"), not(UInt<1>("h0")), "") : assert_0""",
+      """stop(clock, UInt<1>("h1"), 1) : stop_123""",
+      """stop(clock, UInt<1>("h1"), 1) : stop_0""",
+      """assert(clock, UInt<1>("h0"), UInt<1>("h0"), "") : assert_1""",
+      """assume(clock, UInt<1>("h0"), UInt<1>("h0"), "") : assume_0""",
+      """cover(clock, UInt<1>("h0"), UInt<1>("h0"), "") : cover_0""",
+      """cover(clock, UInt<1>("h0"), UInt<1>("h0"), "") : cover_1"""
+    )
+    expected.foreach(e => assert(result.contains(e)))
+  }
+}
diff --git a/src/test/scala/firrtlTests/CheckSpec.scala b/src/test/scala/firrtlTests/CheckSpec.scala
index 1137f8cd..a3efc784 100644
--- a/src/test/scala/firrtlTests/CheckSpec.scala
+++ b/src/test/scala/firrtlTests/CheckSpec.scala
@@ -384,6 +384,36 @@ class CheckSpec extends AnyFlatSpec with Matchers {
     }
   }
 
+  "Attempting to shadow a statement name" should "throw an error" in {
+    val input =
+      s"""|circuit scopes:
+          |  module scopes:
+          |    input c: Clock
+          |    input i: UInt<1>
+          |    output o: UInt<1>
+          |    wire x: UInt<1>
+          |    when i:
+          |      stop(c, UInt(1), 1) : x
+          |    o <= and(x, i)
+          |""".stripMargin
+    assertThrows[CheckHighForm.NotUniqueException] {
+      checkHighInput(input)
+    }
+  }
+
+  "Colliding statement names" should "throw an error" in {
+    val input =
+      s"""|circuit test:
+          |  module test:
+          |    input c: Clock
+          |    stop(c, UInt(1), 1) : x
+          |    stop(c, UInt(1), 1) : x
+          |""".stripMargin
+    assertThrows[CheckHighForm.NotUniqueException] {
+      checkHighInput(input)
+    }
+  }
+
   "Conditionally statements" should "create separate consequent and alternate scopes" in {
     val input =
       s"""|circuit scopes:
@@ -536,6 +566,20 @@ class CheckSpec extends AnyFlatSpec with Matchers {
     }
   }
 
+  it should "throw an exception if a statement name is used as a reference" in {
+    val src = """
+                |circuit test:
+                |  module test:
+                |    input clock: Clock
+                |    output a: UInt<2>
+                |    stop(clock, UInt(1), 1) : hello
+                |    a <= hello
+                |""".stripMargin
+    assertThrows[CheckHighForm.UndeclaredReferenceException] {
+      checkHighInput(src)
+    }
+  }
+
 }
 
 object CheckSpec {
diff --git a/src/test/scala/firrtlTests/InlineInstancesTests.scala b/src/test/scala/firrtlTests/InlineInstancesTests.scala
index 6bee2b77..cc7257d2 100644
--- a/src/test/scala/firrtlTests/InlineInstancesTests.scala
+++ b/src/test/scala/firrtlTests/InlineInstancesTests.scala
@@ -460,6 +460,60 @@ class InlineInstancesTests extends LowTransformSpec {
     )
   }
 
+  "inlining named statements" should "work" in {
+    val input =
+      """circuit Top :
+        |  module Top :
+        |    input clock : Clock
+        |    input a : UInt<32>
+        |    output b : UInt<32>
+        |    inst i of Inline
+        |    i.clock <= clock
+        |    i.a <= a
+        |    b <= i.b
+        |  module Inline :
+        |    input clock : Clock
+        |    input a : UInt<32>
+        |    output b : UInt<32>
+        |    b <= a
+        |    assert(clock, UInt(1), eq(a,b), "a == b") : assert1
+        |    assert(clock, UInt(1), not(eq(a,b)), "a != b")
+        |    stop(clock, UInt(0), 0)
+        |""".stripMargin
+    val check =
+      """circuit Top :
+        |  module Top :
+        |    input clock : Clock
+        |    input a : UInt<32>
+        |    output b : UInt<32>
+        |    wire i_clock : Clock
+        |    wire i_a : UInt<32>
+        |    wire i_b : UInt<32>
+        |    i_b <= i_a
+        |    assert(i_clock, UInt(1), eq(i_a, i_b), "a == b") : i_assert1
+        |    assert(i_clock, UInt(1), not(eq(i_a, i_b)), "a != b")
+        |    stop(i_clock, UInt(0), 0)
+        |    b <= i_b
+        |    i_clock <= clock
+        |    i_a <= a
+        |""".stripMargin
+    val top = CircuitTarget("Top").module("Top")
+    val inlined = top.instOf("i", "Inline")
+
+    executeWithAnnos(
+      input,
+      check,
+      Seq(
+        inline("Inline"),
+        NoCircuitDedupAnnotation,
+        DummyAnno(inlined.ref("assert1"))
+      ),
+      Seq(
+        DummyAnno(top.ref("i_assert1"))
+      )
+    )
+  }
+
   "inlining both grandparent and grandchild" should "should work" in {
     val input =
       """circuit Top :
diff --git a/src/test/scala/firrtlTests/LowerTypesSpec.scala b/src/test/scala/firrtlTests/LowerTypesSpec.scala
index da84b362..78d03e68 100644
--- a/src/test/scala/firrtlTests/LowerTypesSpec.scala
+++ b/src/test/scala/firrtlTests/LowerTypesSpec.scala
@@ -321,6 +321,25 @@ class LowerTypesUniquifySpec extends FirrtlFlatSpec {
     executeTest(input, expected)
   }
 
+  it should "rename nodes colliding with labled statements" in {
+    val input =
+      """circuit Test :
+        |  module Test :
+        |    input clock : Clock
+        |    reg x : { b : UInt<1>, c : { d : UInt<2>, e : UInt<3>}[2], c_1_e : UInt<4>}[2], clock
+        |    node a = x
+        |    printf(clock, UInt(1), "") : a_0_c_
+        |    assert(clock, UInt(1), UInt(1), "") : a__0
+      """.stripMargin
+    val expected = Seq(
+      "node a___0_b = x_0_b",
+      "node a___1_c__1_e = x_1_c__1_e",
+      "node a___1_c_1_e = x_1_c_1_e"
+    )
+
+    executeTest(input, expected)
+  }
+
   it should "rename DefRegister expressions: clock, reset, and init" in {
     val input =
       """circuit Test :
diff --git a/src/test/scala/firrtlTests/ParserSpec.scala b/src/test/scala/firrtlTests/ParserSpec.scala
index 373b960c..ba61b134 100644
--- a/src/test/scala/firrtlTests/ParserSpec.scala
+++ b/src/test/scala/firrtlTests/ParserSpec.scala
@@ -147,6 +147,27 @@ class ParserSpec extends FirrtlFlatSpec {
     }
   }
 
+  // ********** Statement labels **********
+  it should "allow certain statement to have a label" in {
+    val prelude = Seq("circuit top :", "  module top :", "    input c : Clock")
+    val statements = Seq("stop(c, UInt(1), 0)", "printf(c, UInt(1), \"\")") ++
+      Seq("assert", "assume", "cover").map(_ + "(c, UInt(1), UInt(1), \"\")")
+    val validLabels = Seq(":test" -> "test", " :test" -> "test", " : test" -> "test", " : test01" -> "test01")
+    statements.foreach { stmt =>
+      validLabels.foreach {
+        case (lbl, expected) =>
+          val line = "    " + stmt + lbl
+          val src = (prelude :+ line).mkString("\n") + "\n"
+          val res = firrtl.Parser.parse(src)
+          CircuitState(res, Nil) should containTree {
+            case s: Stop         => s.name == expected
+            case s: Print        => s.name == expected
+            case s: Verification => s.name == expected
+          }
+      }
+    }
+  }
+
   // ********** Keywords **********
   "Keywords" should "be allowed as Ids" in {
     import KeywordTests._
diff --git a/src/test/scala/firrtlTests/VerilogEquivalenceSpec.scala b/src/test/scala/firrtlTests/VerilogEquivalenceSpec.scala
index d88309ce..747f6689 100644
--- a/src/test/scala/firrtlTests/VerilogEquivalenceSpec.scala
+++ b/src/test/scala/firrtlTests/VerilogEquivalenceSpec.scala
@@ -7,116 +7,116 @@ import firrtl.testutils._
 class VerilogEquivalenceSpec extends FirrtlFlatSpec {
   "mul followed by cat" should "be correct" in {
     val header = s"""
-      |circuit Multiply :
-      |  module Multiply :
-      |    input x : UInt<4>
-      |    input y : UInt<2>
-      |    input z : UInt<2>
-      |    output out : UInt<8>
-      |""".stripMargin
+                    |circuit Multiply :
+                    |  module Multiply :
+                    |    input x : UInt<4>
+                    |    input y : UInt<2>
+                    |    input z : UInt<2>
+                    |    output out : UInt<8>
+                    |""".stripMargin
     val input1 = header + """
-      |    out <= cat(z, mul(x, y))""".stripMargin
+                            |    out <= cat(z, mul(x, y))""".stripMargin
     val input2 = header + """
-      |    node n = mul(x, y)
-      |    node m = cat(z, n)
-      |    out <= m""".stripMargin
+                            |    node n = mul(x, y)
+                            |    node m = cat(z, n)
+                            |    out <= m""".stripMargin
     val expected = s"""
-      |module MultiplyRef(
-      |  input [3:0] x,
-      |  input [1:0] y,
-      |  input [1:0] z,
-      |  output [7:0] out
-      |);
-      |  wire [5:0] w = x * y;
-      |  assign out = {z, w};
-      |endmodule""".stripMargin
+                      |module MultiplyRef(
+                      |  input [3:0] x,
+                      |  input [1:0] y,
+                      |  input [1:0] z,
+                      |  output [7:0] out
+                      |);
+                      |  wire [5:0] w = x * y;
+                      |  assign out = {z, w};
+                      |endmodule""".stripMargin
     firrtlEquivalenceWithVerilog(input1, expected)
     firrtlEquivalenceWithVerilog(input2, expected)
   }
 
   "div followed by cat" should "be correct" in {
     val header = s"""
-      |circuit Divide :
-      |  module Divide :
-      |    input x : UInt<4>
-      |    input y : UInt<2>
-      |    input z : UInt<2>
-      |    output out : UInt<6>
-      |""".stripMargin
+                    |circuit Divide :
+                    |  module Divide :
+                    |    input x : UInt<4>
+                    |    input y : UInt<2>
+                    |    input z : UInt<2>
+                    |    output out : UInt<6>
+                    |""".stripMargin
     val input1 = header + """
-      |    out <= cat(z, div(x, y))""".stripMargin
+                            |    out <= cat(z, div(x, y))""".stripMargin
     val input2 = header + """
-      |    node n = div(x, y)
-      |    node m = cat(z, n)
-      |    out <= m""".stripMargin
+                            |    node n = div(x, y)
+                            |    node m = cat(z, n)
+                            |    out <= m""".stripMargin
     val expected = s"""
-      |module DivideRef(
-      |  input [3:0] x,
-      |  input [1:0] y,
-      |  input [1:0] z,
-      |  output [5:0] out
-      |);
-      |  wire [3:0] w = x / y;
-      |  assign out = {z, w};
-      |endmodule""".stripMargin
+                      |module DivideRef(
+                      |  input [3:0] x,
+                      |  input [1:0] y,
+                      |  input [1:0] z,
+                      |  output [5:0] out
+                      |);
+                      |  wire [3:0] w = x / y;
+                      |  assign out = {z, w};
+                      |endmodule""".stripMargin
     firrtlEquivalenceWithVerilog(input1, expected)
     firrtlEquivalenceWithVerilog(input2, expected)
   }
 
   "signed mul followed by cat" should "be correct" in {
     val header = s"""
-      |circuit SignedMultiply :
-      |  module SignedMultiply :
-      |    input x : SInt<4>
-      |    input y : SInt<2>
-      |    input z : SInt<2>
-      |    output out : UInt<8>
-      |""".stripMargin
+                    |circuit SignedMultiply :
+                    |  module SignedMultiply :
+                    |    input x : SInt<4>
+                    |    input y : SInt<2>
+                    |    input z : SInt<2>
+                    |    output out : UInt<8>
+                    |""".stripMargin
     val input1 = header + """
-      |    out <= cat(z, mul(x, y))""".stripMargin
+                            |    out <= cat(z, mul(x, y))""".stripMargin
     val input2 = header + """
-      |    node n = mul(x, y)
-      |    node m = cat(z, n)
-      |    out <= m""".stripMargin
+                            |    node n = mul(x, y)
+                            |    node m = cat(z, n)
+                            |    out <= m""".stripMargin
     val expected = s"""
-      |module SignedMultiplyRef(
-      |  input signed [3:0] x,
-      |  input signed [1:0] y,
-      |  input signed [1:0] z,
-      |  output [7:0] out
-      |);
-      |  wire [5:0] w = x * y;
-      |  assign out = {z, w};
-      |endmodule""".stripMargin
+                      |module SignedMultiplyRef(
+                      |  input signed [3:0] x,
+                      |  input signed [1:0] y,
+                      |  input signed [1:0] z,
+                      |  output [7:0] out
+                      |);
+                      |  wire [5:0] w = x * y;
+                      |  assign out = {z, w};
+                      |endmodule""".stripMargin
     firrtlEquivalenceWithVerilog(input1, expected)
     firrtlEquivalenceWithVerilog(input2, expected)
   }
 
   "signed div followed by cat" should "be correct" in {
     val header = s"""
-      |circuit SignedDivide :
-      |  module SignedDivide :
-      |    input x : SInt<4>
-      |    input y : SInt<2>
-      |    input z : SInt<2>
-      |    output out : UInt<7>
-      |""".stripMargin
+                    |circuit SignedDivide :
+                    |  module SignedDivide :
+                    |    input x : SInt<4>
+                    |    input y : SInt<2>
+                    |    input z : SInt<2>
+                    |    output out : UInt<7>
+                    |""".stripMargin
     val input1 = header + """
-      |    out <= cat(z, div(x, y))""".stripMargin
+                            |    out <= cat(z, div(x, y))""".stripMargin
     val input2 = header + """
-      |    node n = div(x, y)
-      |    node m = cat(z, n)
-      |    out <= m""".stripMargin
+                            |    node n = div(x, y)
+                            |    node m = cat(z, n)
+                            |    out <= m""".stripMargin
     val expected = s"""
-      |module SignedDivideRef(
-      |  input signed [3:0] x,
-      |  input signed [1:0] y,
-      |  input signed [1:0] z,
-      |  output [6:0] out
-      |);
-      |  wire [4:0] w = x / y;
-      |  assign out = {z, w};
-      |endmodule""".stripMargin
+                      |module SignedDivideRef(
+                      |  input signed [3:0] x,
+                      |  input signed [1:0] y,
+                      |  input signed [1:0] z,
+                      |  output [6:0] out
+                      |);
+                      |  wire [4:0] w = x / y;
+                      |  assign out = {z, w};
+                      |endmodule""".stripMargin
     firrtlEquivalenceWithVerilog(input1, expected)
     firrtlEquivalenceWithVerilog(input2, expected)
   }