diff options
Diffstat (limited to 'src/main/scala/firrtl/transforms')
5 files changed, 131 insertions, 1 deletions
diff --git a/src/main/scala/firrtl/transforms/DeadCodeElimination.scala b/src/main/scala/firrtl/transforms/DeadCodeElimination.scala index b8cfa54e..4182e496 100644 --- a/src/main/scala/firrtl/transforms/DeadCodeElimination.scala +++ b/src/main/scala/firrtl/transforms/DeadCodeElimination.scala @@ -154,6 +154,10 @@ class DeadCodeElimination extends Transform Seq(clk, en).flatMap(getDeps(_)).foreach(ref => depGraph.addPairWithEdge(circuitSink, ref)) case Print(_, _, args, clk, en) => (args :+ clk :+ en).flatMap(getDeps(_)).foreach(ref => depGraph.addPairWithEdge(circuitSink, ref)) + case s: Verification => + for (expr <- Seq(s.clk, s.pred, s.en)) { + getDeps(expr).foreach(ref => depGraph.addPairWithEdge(circuitSink, ref)) + } case Block(stmts) => stmts.foreach(onStmt(_)) case ignore @ (_: IsInvalid | _: WDefInstance | EmptyStmt) => // do nothing case other => throw new Exception(s"Unexpected Statement $other") @@ -256,6 +260,7 @@ class DeadCodeElimination extends Transform 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 => val node = getDeps(con.loc) match { case Seq(elt) => elt } if (deadNodes.contains(node)) EmptyStmt else con diff --git a/src/main/scala/firrtl/transforms/LegalizeClocks.scala b/src/main/scala/firrtl/transforms/LegalizeClocks.scala index 333eb096..f439fdc9 100644 --- a/src/main/scala/firrtl/transforms/LegalizeClocks.scala +++ b/src/main/scala/firrtl/transforms/LegalizeClocks.scala @@ -45,6 +45,10 @@ object LegalizeClocksTransform { val node = DefNode(s.info, namespace.newTemp, s.clk) val sx = s.copy(clk = WRef(node)) Block(Seq(node, sx)) + case s: Verification if illegalClockExpr(s.clk) => + val node = DefNode(s.info, namespace.newTemp, s.clk) + val sx = s.copy(clk = WRef(node)) + Block(Seq(node, sx)) case other => other } diff --git a/src/main/scala/firrtl/transforms/RemoveWires.scala b/src/main/scala/firrtl/transforms/RemoveWires.scala index 0504c19d..33daa8ce 100644 --- a/src/main/scala/firrtl/transforms/RemoveWires.scala +++ b/src/main/scala/firrtl/transforms/RemoveWires.scala @@ -124,7 +124,7 @@ class RemoveWires extends Transform with DependencyAPIMigration { netlist(we(expr)) = (Seq(ValidIf(Utils.zero, UIntLiteral(BigInt(0), width), expr.tpe)), info) case _ => otherStmts += invalid } - case other @ (_: Print | _: Stop | _: Attach) => + case other @ (_: Print | _: Stop | _: Attach | _: Verification) => otherStmts += other case EmptyStmt => // Dont bother keeping EmptyStmts around case block: Block => block.foreach(onStmt) diff --git a/src/main/scala/firrtl/transforms/formal/AssertSubmoduleAssumptions.scala b/src/main/scala/firrtl/transforms/formal/AssertSubmoduleAssumptions.scala new file mode 100644 index 00000000..7370fcfb --- /dev/null +++ b/src/main/scala/firrtl/transforms/formal/AssertSubmoduleAssumptions.scala @@ -0,0 +1,68 @@ + +package firrtl.transforms.formal + +import firrtl.ir.{Circuit, Formal, Statement, Verification} +import firrtl.stage.TransformManager.TransformDependency +import firrtl.{CircuitState, DependencyAPIMigration, Transform} +import firrtl.annotations.NoTargetAnnotation +import firrtl.options.{PreservesAll, RegisteredTransform, ShellOption} + + +/** + * Assert Submodule Assumptions + * + * Converts `assume` statements to `assert` statements in all modules except + * the top module being compiled. This avoids a class of bugs in which an + * overly restrictive assume in a child module can prevent the model checker + * from searching valid inputs and states in the parent module. + */ +class AssertSubmoduleAssumptions extends Transform + with RegisteredTransform + with DependencyAPIMigration + with PreservesAll[Transform] { + + override def prerequisites: Seq[TransformDependency] = Seq.empty + override def optionalPrerequisites: Seq[TransformDependency] = Seq.empty + override def optionalPrerequisiteOf: Seq[TransformDependency] = + firrtl.stage.Forms.MidEmitters + + val options = Seq( + new ShellOption[Unit]( + longOption = "no-asa", + toAnnotationSeq = (_: Unit) => Seq( + DontAssertSubmoduleAssumptionsAnnotation), + helpText = "Disable assert submodule assumptions" ) ) + + def assertAssumption(s: Statement): Statement = s match { + case Verification(Formal.Assume, info, clk, cond, en, msg) => + Verification(Formal.Assert, info, clk, cond, en, msg) + case t => t.mapStmt(assertAssumption) + } + + def run(c: Circuit): Circuit = { + c.mapModule(mod => { + if (mod.name != c.main) { + mod.mapStmt(assertAssumption) + } else { + mod + } + }) + } + + def execute(state: CircuitState): CircuitState = { + val noASA = state.annotations.contains( + DontAssertSubmoduleAssumptionsAnnotation) + if (noASA) { + logger.info("Skipping assert submodule assumptions") + state + } else { + state.copy(circuit = run(state.circuit)) + } + } +} + +case object AssertSubmoduleAssumptionsAnnotation extends NoTargetAnnotation { + val transform = new AssertSubmoduleAssumptions +} + +case object DontAssertSubmoduleAssumptionsAnnotation extends NoTargetAnnotation diff --git a/src/main/scala/firrtl/transforms/formal/RemoveVerificationStatements.scala b/src/main/scala/firrtl/transforms/formal/RemoveVerificationStatements.scala new file mode 100644 index 00000000..9bf4f779 --- /dev/null +++ b/src/main/scala/firrtl/transforms/formal/RemoveVerificationStatements.scala @@ -0,0 +1,53 @@ + +package firrtl.transforms.formal + +import firrtl.ir.{Circuit, EmptyStmt, Statement, Verification} +import firrtl.{CircuitState, DependencyAPIMigration, MinimumVerilogEmitter, Transform, VerilogEmitter} +import firrtl.options.{Dependency, PreservesAll, StageUtils} +import firrtl.stage.TransformManager.TransformDependency + + +/** + * Remove Verification Statements + * + * Replaces all verification statements in all modules with the empty statement. + * This is intended to be required by the Verilog emitter to ensure compatibility + * with the Verilog 2001 standard. + */ +class RemoveVerificationStatements extends Transform + with DependencyAPIMigration + with PreservesAll[Transform] { + + override def prerequisites: Seq[TransformDependency] = Seq.empty + override def optionalPrerequisites: Seq[TransformDependency] = Seq.empty + override def optionalPrerequisiteOf: Seq[TransformDependency] = + Seq( Dependency[VerilogEmitter], + Dependency[MinimumVerilogEmitter]) + + private var removedCounter = 0 + + def removeVerification(s: Statement): Statement = s match { + case _: Verification => { + removedCounter += 1 + EmptyStmt + } + case t => t.mapStmt(removeVerification) + } + + def run(c: Circuit): Circuit = { + c.mapModule(mod => { + mod.mapStmt(removeVerification) + }) + } + + def execute(state: CircuitState): CircuitState = { + val newState = state.copy(circuit = run(state.circuit)) + if (removedCounter > 0) { + StageUtils.dramaticWarning(s"$removedCounter verification statements " + + "were removed when compiling to Verilog because the basic Verilog " + + "standard does not support them. If this was not intended, compile " + + "to System Verilog instead using the `-X sverilog` compiler flag.") + } + newState + } +} |