diff options
| author | Kevin Laeufer | 2021-03-04 11:23:51 -0800 |
|---|---|---|
| committer | GitHub | 2021-03-04 19:23:51 +0000 |
| commit | c93d6f5319efd7ba42147180c6e2b6f3796ef943 (patch) | |
| tree | cea5c960c6fd15c1680f43d78fa06a69dda7dc6e /src/main/scala/firrtl/ir/Serializer.scala | |
| parent | e58ba0c12e5d650983c70a61a45542f0cd43fb88 (diff) | |
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.
Diffstat (limited to 'src/main/scala/firrtl/ir/Serializer.scala')
| -rw-r--r-- | src/main/scala/firrtl/ir/Serializer.scala | 7 |
1 files changed, 7 insertions, 0 deletions
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, |