SMT Backend: move undefined memory behavior modelling to firrtl IR level (#2095)

With this PR the smt backend now supports memories
with more than two write ports and the conservative
memory modelling can be selectively turned off with
a new annotation.

2 files changed, 11 insertions, 0 deletions

diff --git a/src/main/scala/firrtl/ir/IR.scala b/src/main/scala/firrtl/ir/IR.scala
index 9c3d6186..13ba3d46 100644
--- a/src/main/scala/firrtl/ir/IR.scala
+++ b/src/main/scala/firrtl/ir/IR.scala
@@ -4,6 +4,7 @@ package firrtl
 package ir
 
 import Utils.{dec2string, trim}
+import firrtl.backends.experimental.smt.random.DefRandom
 import dataclass.{data, since}
 import firrtl.constraint.{Constraint, IsKnown, IsVar}
 import org.apache.commons.text.translate.{AggregateTranslator, JavaUnicodeEscaper, LookupTranslator}
@@ -242,6 +243,9 @@ object Reference {
   /** Creates a Reference from a Register */
   def apply(reg: DefRegister): Reference = Reference(reg.name, reg.tpe, RegKind, UnknownFlow)
 
+  /** Creates a Reference from a Random Source */
+  def apply(rnd: DefRandom): Reference = Reference(rnd.name, rnd.tpe, RandomKind, UnknownFlow)
+
   /** Creates a Reference from a Node */
   def apply(node: DefNode): Reference = Reference(node.name, node.value.tpe, NodeKind, SourceFlow)
 
diff --git a/src/main/scala/firrtl/ir/Serializer.scala b/src/main/scala/firrtl/ir/Serializer.scala
index caea0a9c..dca902fe 100644
--- a/src/main/scala/firrtl/ir/Serializer.scala
+++ b/src/main/scala/firrtl/ir/Serializer.scala
@@ -2,6 +2,8 @@
 
 package firrtl.ir
 
+import firrtl.Utils
+import firrtl.backends.experimental.smt.random.DefRandom
 import firrtl.constraint.Constraint
 
 object Serializer {
@@ -114,6 +116,11 @@ object Serializer {
     case DefRegister(info, name, tpe, clock, reset, init) =>
       b ++= "reg "; b ++= name; b ++= " : "; s(tpe); b ++= ", "; s(clock); b ++= " with :"; newLineAndIndent(1)
       b ++= "reset => ("; s(reset); b ++= ", "; s(init); b += ')'; s(info)
+    case DefRandom(info, name, tpe, clock, en) =>
+      b ++= "rand "; b ++= name; b ++= " : "; s(tpe);
+      if (clock.isDefined) { b ++= ", "; s(clock.get); }
+      en match { case Utils.True() => case _ => b ++= " when "; s(en) }
+      s(info)
     case DefInstance(info, name, module, _) => b ++= "inst "; b ++= name; b ++= " of "; b ++= module; s(info)
     case DefMemory(
           info,