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/passes | |
| 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/passes')
| -rw-r--r-- | src/main/scala/firrtl/passes/ResolveKinds.scala | 2 | ||||
| -rw-r--r-- | src/main/scala/firrtl/passes/memlib/VerilogMemDelays.scala | 3 |
2 files changed, 4 insertions, 1 deletions
diff --git a/src/main/scala/firrtl/passes/ResolveKinds.scala b/src/main/scala/firrtl/passes/ResolveKinds.scala index e3218467..745be1e2 100644 --- a/src/main/scala/firrtl/passes/ResolveKinds.scala +++ b/src/main/scala/firrtl/passes/ResolveKinds.scala @@ -5,6 +5,7 @@ package firrtl.passes import firrtl._ import firrtl.ir._ import firrtl.Mappers._ +import firrtl.backends.experimental.smt.random.DefRandom import firrtl.traversals.Foreachers._ object ResolveKinds extends Pass { @@ -31,6 +32,7 @@ object ResolveKinds extends Pass { case sx: DefRegister => kinds(sx.name) = RegKind case sx: WDefInstance => kinds(sx.name) = InstanceKind case sx: DefMemory => kinds(sx.name) = MemKind + case sx: DefRandom => kinds(sx.name) = RandomKind case _ => } s.map(resolve_stmt(kinds)) diff --git a/src/main/scala/firrtl/passes/memlib/VerilogMemDelays.scala b/src/main/scala/firrtl/passes/memlib/VerilogMemDelays.scala index 8fb2dc88..143b925a 100644 --- a/src/main/scala/firrtl/passes/memlib/VerilogMemDelays.scala +++ b/src/main/scala/firrtl/passes/memlib/VerilogMemDelays.scala @@ -177,7 +177,8 @@ class MemDelayAndReadwriteTransformer(m: DefModule) { object VerilogMemDelays extends Pass { - override def prerequisites = firrtl.stage.Forms.LowForm :+ Dependency(firrtl.passes.RemoveValidIf) + override def prerequisites = firrtl.stage.Forms.LowForm + override val optionalPrerequisites = Seq(Dependency(firrtl.passes.RemoveValidIf)) override val optionalPrerequisiteOf = Seq(Dependency[VerilogEmitter], Dependency[SystemVerilogEmitter]) |