diff options
Diffstat (limited to 'src')
25 files changed, 545 insertions, 24 deletions
diff --git a/src/main/antlr4/FIRRTL.g4 b/src/main/antlr4/FIRRTL.g4 index 39988e18..f0ea5b10 100644 --- a/src/main/antlr4/FIRRTL.g4 +++ b/src/main/antlr4/FIRRTL.g4 @@ -107,6 +107,9 @@ stmt | 'printf(' exp exp StringLit ( exp)* ')' info? | 'skip' info? | 'attach' '(' exp+ ')' info? + | 'assert' '(' exp exp exp StringLit ')' info? + | 'assume' '(' exp exp exp StringLit ')' info? + | 'cover' '(' exp exp exp StringLit ')' info? ; memField diff --git a/src/main/proto/firrtl.proto b/src/main/proto/firrtl.proto index 3d2c89f1..b4c8f36d 100644 --- a/src/main/proto/firrtl.proto +++ b/src/main/proto/firrtl.proto @@ -188,6 +188,25 @@ message Firrtl { Expression en = 4; } + enum Formal { + ASSERT = 0; + ASSUME = 1; + COVER = 2; + } + + message Verification { + // Required. + Formal op = 1; + // Required. + Expression clk = 2; + // Required. + Expression cond = 3; + // Required. + Expression en = 4; + // Required. + string msg = 5; + } + message Skip { // Empty } diff --git a/src/main/resources/META-INF/services/firrtl.options.RegisteredTransform b/src/main/resources/META-INF/services/firrtl.options.RegisteredTransform index 638404be..bb72d45c 100644 --- a/src/main/resources/META-INF/services/firrtl.options.RegisteredTransform +++ b/src/main/resources/META-INF/services/firrtl.options.RegisteredTransform @@ -2,3 +2,4 @@ firrtl.transforms.DeadCodeElimination firrtl.transforms.CheckCombLoops firrtl.passes.InlineInstances firrtl.passes.clocklist.ClockListTransform +firrtl.transforms.formal.AssertSubmoduleAssumptions diff --git a/src/main/scala/firrtl/Emitter.scala b/src/main/scala/firrtl/Emitter.scala index 3b065bf4..268841da 100644 --- a/src/main/scala/firrtl/Emitter.scala +++ b/src/main/scala/firrtl/Emitter.scala @@ -5,7 +5,6 @@ package firrtl import java.io.Writer import scala.collection.mutable - import firrtl.ir._ import firrtl.passes._ import firrtl.transforms.LegalizeAndReductionsTransform @@ -15,8 +14,9 @@ import firrtl.PrimOps._ import firrtl.WrappedExpression._ import Utils._ import MemPortUtils.{memPortField, memType} -import firrtl.options.{Dependency, HasShellOptions, ShellOption, StageUtils, PhaseException, Unserializable} +import firrtl.options.{Dependency, HasShellOptions, PhaseException, ShellOption, Unserializable} import firrtl.stage.{RunFirrtlTransformAnnotation, TransformManager} +import firrtl.transforms.formal.RemoveVerificationStatements // Datastructures import scala.collection.mutable.ArrayBuffer @@ -182,6 +182,7 @@ class VerilogEmitter extends SeqTransform with Emitter { def outputForm = LowForm override def prerequisites = + Dependency[RemoveVerificationStatements] +: Dependency[LegalizeAndReductionsTransform] +: firrtl.stage.Forms.LowFormOptimized @@ -454,6 +455,13 @@ class VerilogEmitter extends SeqTransform with Emitter { case m: Module => new VerilogRender(m, moduleMap)(writer) } } + + def addFormalStatement(formals: mutable.Map[Expression, ArrayBuffer[Seq[Any]]], + clk: Expression, en: Expression, + stmt: Seq[Any], info: Info): Unit = { + throw EmitterException("Cannot emit verification statements in Verilog" + + "(2001). Use the SystemVerilog emitter instead.") + } /** * Store Emission option per Target @@ -594,6 +602,7 @@ class VerilogEmitter extends SeqTransform with Emitter { // memories need to be initialized even when randomization is disabled val memoryInitials = ArrayBuffer[Seq[Any]]() val simulates = ArrayBuffer[Seq[Any]]() + val formals = mutable.LinkedHashMap[Expression, ArrayBuffer[Seq[Any]]]() def bigIntToVLit(bi: BigInt): String = if (bi.isValidInt) bi.toString else s"${bi.bitLength}'d$bi" @@ -818,6 +827,14 @@ class VerilogEmitter extends SeqTransform with Emitter { lines += Seq("`endif // SYNTHESIS") } + def addFormal(clk: Expression, en: Expression, stmt: Seq[Any], info: Info) = { + addFormalStatement(formals, clk, en, stmt, info) + } + + def formalStatement(op: Formal.Value, cond: Expression): Seq[Any] = { + Seq(op.toString, "(", cond, ");") + } + def stop(ret: Int): Seq[Any] = Seq(if (ret == 0) "$finish;" else "$fatal;") def printf(str: StringLit, args: Seq[Expression]): Seq[Any] = { @@ -921,6 +938,8 @@ class VerilogEmitter extends SeqTransform with Emitter { simulate(sx.clk, sx.en, stop(sx.ret), Some("STOP_COND"), sx.info) case sx: Print => simulate(sx.clk, sx.en, printf(sx.string, sx.args), Some("PRINTF_COND"), sx.info) + case sx: Verification => + addFormal(sx.clk, sx.en, formalStatement(sx.op, sx.pred), sx.info) // If we are emitting an Attach, it must not have been removable in VerilogPrep case sx: Attach => // For Synthesis @@ -1120,6 +1139,14 @@ class VerilogEmitter extends SeqTransform with Emitter { emit(Seq("`endif // SYNTHESIS")) } + if (formals.keys.nonEmpty) { + for ((clk, content) <- formals if content.nonEmpty) { + emit(Seq(tab, "always @(posedge ", clk, ") begin")) + for (line <- content) emit(Seq(tab, tab, line)) + emit(Seq(tab, "end")) + } + } + emit(Seq("endmodule")) } @@ -1213,6 +1240,7 @@ class VerilogEmitter extends SeqTransform with Emitter { class MinimumVerilogEmitter extends VerilogEmitter with Emitter { override def prerequisites = + Dependency[RemoveVerificationStatements] +: Dependency[LegalizeAndReductionsTransform] +: firrtl.stage.Forms.LowFormMinimumOptimized @@ -1224,8 +1252,20 @@ class MinimumVerilogEmitter extends VerilogEmitter with Emitter { class SystemVerilogEmitter extends VerilogEmitter { override val outputSuffix: String = ".sv" + override def prerequisites = + Dependency[LegalizeAndReductionsTransform] +: + firrtl.stage.Forms.LowFormOptimized + + override def addFormalStatement(formals: mutable.Map[Expression, ArrayBuffer[Seq[Any]]], + clk: Expression, en: Expression, + stmt: Seq[Any], info: Info): Unit = { + val lines = formals.getOrElseUpdate(clk, ArrayBuffer[Seq[Any]]()) + lines += Seq("if (", en, ") begin") + lines += Seq(tab, stmt, info) + lines += Seq("end") + } + override def execute(state: CircuitState): CircuitState = { - StageUtils.dramaticWarning("SystemVerilog Emitter is the same as the Verilog Emitter!") super.execute(state) } } diff --git a/src/main/scala/firrtl/LoweringCompilers.scala b/src/main/scala/firrtl/LoweringCompilers.scala index 14d222f6..19e7d8c6 100644 --- a/src/main/scala/firrtl/LoweringCompilers.scala +++ b/src/main/scala/firrtl/LoweringCompilers.scala @@ -3,7 +3,6 @@ package firrtl import firrtl.transforms.IdentityTransform -import firrtl.options.StageUtils import firrtl.stage.{Forms, TransformManager} @deprecated("Use a TransformManager or some other Stage/Phase class. Will be removed in 1.4.", "FIRRTL 1.2") @@ -174,5 +173,4 @@ class MinimumVerilogCompiler extends Compiler { ) class SystemVerilogCompiler extends VerilogCompiler { override val emitter = new SystemVerilogEmitter - StageUtils.dramaticWarning("SystemVerilog Compiler behaves the same as the Verilog Compiler!") } diff --git a/src/main/scala/firrtl/Visitor.scala b/src/main/scala/firrtl/Visitor.scala index 4033c0fd..48a887de 100644 --- a/src/main/scala/firrtl/Visitor.scala +++ b/src/main/scala/firrtl/Visitor.scala @@ -328,6 +328,17 @@ class Visitor(infoMode: InfoMode) extends AbstractParseTreeVisitor[FirrtlNode] w case "attach" => Attach(info, ctx_exp map visitExp) case "printf(" => Print(info, visitStringLit(ctx.StringLit), ctx_exp.drop(2).map(visitExp), visitExp(ctx_exp(0)), visitExp(ctx_exp(1))) + // formal + case "assert" => Verification(Formal.Assert, info, visitExp(ctx_exp(0)), + visitExp(ctx_exp(1)), visitExp(ctx_exp(2)), + visitStringLit(ctx.StringLit)) + case "assume" => Verification(Formal.Assume, info, visitExp(ctx_exp(0)), + visitExp(ctx_exp(1)), visitExp(ctx_exp(2)), + visitStringLit(ctx.StringLit)) + case "cover" => Verification(Formal.Cover, info, visitExp(ctx_exp(0)), + visitExp(ctx_exp(1)), visitExp(ctx_exp(2)), + visitStringLit(ctx.StringLit)) + // end formal case "skip" => EmptyStmt } // If we don't match on the first child, try the next one diff --git a/src/main/scala/firrtl/ir/IR.scala b/src/main/scala/firrtl/ir/IR.scala index a47a4cea..9914ad45 100644 --- a/src/main/scala/firrtl/ir/IR.scala +++ b/src/main/scala/firrtl/ir/IR.scala @@ -541,6 +541,38 @@ case class Print( def foreachString(f: String => Unit): Unit = Unit def foreachInfo(f: Info => Unit): Unit = f(info) } + +// formal +object Formal extends Enumeration { + val Assert = Value("assert") + val Assume = Value("assume") + val Cover = Value("cover") +} + +case class Verification( + op: Formal.Value, + info: Info, + clk: Expression, + pred: Expression, + en: Expression, + msg: StringLit +) extends Statement with HasInfo { + def serialize: String = op + "(" + Seq(clk, pred, en).map(_.serialize) + .mkString(", ") + ", \"" + msg.serialize + "\")" + info.serialize + 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 mapInfo(f: Info => Info): Statement = copy(info = f(info)) + def foreachStmt(f: Statement => Unit): Unit = Unit + def foreachExpr(f: Expression => Unit): Unit = { f(clk); f(pred); f(en); } + def foreachType(f: Type => Unit): Unit = Unit + def foreachString(f: String => Unit): Unit = Unit + def foreachInfo(f: Info => Unit): Unit = f(info) +} +// end formal + case object EmptyStmt extends Statement { def serialize: String = "skip" def mapStmt(f: Statement => Statement): Statement = this diff --git a/src/main/scala/firrtl/passes/CheckFlows.scala b/src/main/scala/firrtl/passes/CheckFlows.scala index b4ce4d5f..3a9cc212 100644 --- a/src/main/scala/firrtl/passes/CheckFlows.scala +++ b/src/main/scala/firrtl/passes/CheckFlows.scala @@ -105,6 +105,10 @@ object CheckFlows extends Pass { case (s: Stop) => check_flow(info, mname, flows, SourceFlow)(s.en) check_flow(info, mname, flows, SourceFlow)(s.clk) + case (s: Verification) => + check_flow(info, mname, flows, SourceFlow)(s.clk) + check_flow(info, mname, flows, SourceFlow)(s.pred) + check_flow(info, mname, flows, SourceFlow)(s.en) case _ => } s foreach check_flows_e(info, mname, flows) diff --git a/src/main/scala/firrtl/passes/CheckTypes.scala b/src/main/scala/firrtl/passes/CheckTypes.scala index 5173b8c4..601ee524 100644 --- a/src/main/scala/firrtl/passes/CheckTypes.scala +++ b/src/main/scala/firrtl/passes/CheckTypes.scala @@ -310,6 +310,10 @@ object CheckTypes extends Pass { errors.append(new PrintfArgNotGround(info, mname)) if (wt(sx.clk.tpe) != wt(ClockType)) errors.append(new ReqClk(info, mname)) if (wt(sx.en.tpe) != wt(ut)) errors.append(new EnNotUInt(info, mname)) + case sx: Verification => + if (wt(sx.clk.tpe) != wt(ClockType)) errors.append(new ReqClk(info, mname)) + if (wt(sx.pred.tpe) != wt(ut)) errors.append(new PredNotUInt(info, mname)) + if (wt(sx.en.tpe) != wt(ut)) errors.append(new EnNotUInt(info, mname)) case sx: DefMemory => sx.dataType match { case AnalogType(w) => errors.append(new IllegalAnalogDeclaration(info, mname, sx.name)) case t => diff --git a/src/main/scala/firrtl/passes/ExpandWhens.scala b/src/main/scala/firrtl/passes/ExpandWhens.scala index 32fec4ed..75aad29a 100644 --- a/src/main/scala/firrtl/passes/ExpandWhens.scala +++ b/src/main/scala/firrtl/passes/ExpandWhens.scala @@ -156,6 +156,7 @@ object ExpandWhens extends Pass { case sx: Stop => simlist += (if (weq(p, one)) sx else Stop(sx.info, sx.ret, sx.clk, AND(p, sx.en))) EmptyStmt + case sx: Verification => if (weq(p, one)) sx else sx.copy(en = AND(p, sx.en)) // Expand conditionally, see comments below case sx: Conditionally => /* 1) Recurse into conseq and alt with empty netlist, updated defaults, updated predicate diff --git a/src/main/scala/firrtl/proto/FromProto.scala b/src/main/scala/firrtl/proto/FromProto.scala index ea4cec1f..5de92b57 100644 --- a/src/main/scala/firrtl/proto/FromProto.scala +++ b/src/main/scala/firrtl/proto/FromProto.scala @@ -8,7 +8,7 @@ import java.io.{File, FileInputStream, InputStream} import collection.JavaConverters._ import FirrtlProtos._ import com.google.protobuf.CodedInputStream -import Firrtl.Statement.ReadUnderWrite +import Firrtl.Statement.{ReadUnderWrite, Formal} object FromProto { @@ -181,6 +181,16 @@ object FromProto { def convert(stop: Firrtl.Statement.Stop, info: Firrtl.SourceInfo): ir.Stop = ir.Stop(convert(info), stop.getReturnValue, convert(stop.getClk), convert(stop.getEn)) + def convert(formal: Formal): ir.Formal.Value = formal match { + case Formal.ASSERT => ir.Formal.Assert + case Formal.ASSUME => ir.Formal.Assume + case Formal.COVER => ir.Formal.Cover + } + + def convert(ver: Firrtl.Statement.Verification, info: Firrtl.SourceInfo): ir.Verification = + ir.Verification(convert(ver.getOp), convert(info), convert(ver.getClk), + convert(ver.getCond), convert(ver.getEn), ir.StringLit(ver.getMsg)) + def convert(mem: Firrtl.Statement.Memory, info: Firrtl.SourceInfo): ir.DefMemory = { val dtype = convert(mem.getType) val rs = mem.getReaderIdList.asScala diff --git a/src/main/scala/firrtl/proto/ToProto.scala b/src/main/scala/firrtl/proto/ToProto.scala index e2481d08..6cc6d11f 100644 --- a/src/main/scala/firrtl/proto/ToProto.scala +++ b/src/main/scala/firrtl/proto/ToProto.scala @@ -6,7 +6,7 @@ package proto import java.io.OutputStream import FirrtlProtos._ -import Firrtl.Statement.ReadUnderWrite +import Firrtl.Statement.{ReadUnderWrite, Formal} import Firrtl.Expression.PrimOp.Op import com.google.protobuf.{CodedOutputStream, WireFormat} import firrtl.PrimOps._ @@ -114,6 +114,12 @@ object ToProto { case ir.ReadUnderWrite.New => ReadUnderWrite.NEW } + def convert(formal: ir.Formal.Value): Formal = formal match { + case ir.Formal.Assert => Formal.ASSERT + case ir.Formal.Assume => Formal.ASSUME + case ir.Formal.Cover => Formal.COVER + } + def convertToIntegerLiteral(value: BigInt): Firrtl.Expression.IntegerLiteral.Builder = { Firrtl.Expression.IntegerLiteral.newBuilder() .setValue(value.toString) @@ -272,6 +278,13 @@ object ToProto { .setClk(convert(clk)) .setEn(convert(en)) sb.setStop(stopb) + case ir.Verification(op, _, clk, cond, en, msg) => + val vb = Firrtl.Statement.Verification.newBuilder() + .setOp(convert(op)) + .setClk(convert(clk)) + .setCond(convert(cond)) + .setEn(convert(en)) + .setMsg(msg.string) case ir.IsInvalid(_, expr) => val ib = Firrtl.Statement.IsInvalid.newBuilder() .setExpression(convert(expr)) diff --git a/src/main/scala/firrtl/stage/Forms.scala b/src/main/scala/firrtl/stage/Forms.scala index 9cf711d8..e6ed9603 100644 --- a/src/main/scala/firrtl/stage/Forms.scala +++ b/src/main/scala/firrtl/stage/Forms.scala @@ -57,7 +57,8 @@ object Forms { Dependency[passes.ExpandWhensAndCheck], Dependency[passes.RemoveIntervals], Dependency(passes.ConvertFixedToSInt), - Dependency(passes.ZeroWidth) ) + Dependency(passes.ZeroWidth), + Dependency[firrtl.transforms.formal.AssertSubmoduleAssumptions] ) val LowForm: Seq[TransformDependency] = MidForm ++ Seq( Dependency(passes.LowerTypes), 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 + } +} diff --git a/src/test/scala/firrtlTests/CustomTransformSpec.scala b/src/test/scala/firrtlTests/CustomTransformSpec.scala index d736ec3c..677aa6ff 100644 --- a/src/test/scala/firrtlTests/CustomTransformSpec.scala +++ b/src/test/scala/firrtlTests/CustomTransformSpec.scala @@ -6,12 +6,11 @@ import firrtl.ir.Circuit import firrtl._ import firrtl.passes.Pass import firrtl.ir._ - import firrtl.stage.{FirrtlSourceAnnotation, FirrtlStage, Forms, RunFirrtlTransformAnnotation} import firrtl.options.Dependency import firrtl.transforms.{IdentityTransform, LegalizeAndReductionsTransform} - import firrtl.testutils._ +import firrtl.transforms.formal.RemoveVerificationStatements import scala.reflect.runtime @@ -173,10 +172,15 @@ class CustomTransformSpec extends FirrtlFlatSpec { .map(target => new firrtl.stage.transforms.Compiler(target)) .map(_.flattenedTransformOrder.map(Dependency.fromTransform(_))) - Seq( (Seq(Dependency[LowFirrtlEmitter]), Seq(low.last) ), - (Seq(Dependency[LegalizeAndReductionsTransform], Dependency[MinimumVerilogEmitter]), Seq(lowMinOpt.last)), - (Seq(Dependency[LegalizeAndReductionsTransform], Dependency[VerilogEmitter]), Seq(lowOpt.last) ), - (Seq(Dependency[LegalizeAndReductionsTransform], Dependency[SystemVerilogEmitter]), Seq(lowOpt.last) ) + Seq( (Seq(Dependency[LowFirrtlEmitter]), Seq(low.last) ), + (Seq(Dependency[LegalizeAndReductionsTransform], + Dependency[RemoveVerificationStatements], + Dependency[MinimumVerilogEmitter]), Seq(lowMinOpt.last)), + (Seq(Dependency[LegalizeAndReductionsTransform], + Dependency[RemoveVerificationStatements], + Dependency[VerilogEmitter]), Seq(lowOpt.last) ), + (Seq(Dependency[LegalizeAndReductionsTransform], + Dependency[SystemVerilogEmitter]), Seq(lowOpt.last) ) ).foreach((testOrder _).tupled) } diff --git a/src/test/scala/firrtlTests/ExpandWhensSpec.scala b/src/test/scala/firrtlTests/ExpandWhensSpec.scala index d4b3d0df..250a75d7 100644 --- a/src/test/scala/firrtlTests/ExpandWhensSpec.scala +++ b/src/test/scala/firrtlTests/ExpandWhensSpec.scala @@ -134,6 +134,20 @@ class ExpandWhensSpec extends FirrtlFlatSpec { val check = "mux(p, in[0], in[1])" executeTest(input, check, true) } + it should "handle asserts" in { + val input = + """circuit Test : + | module Test : + | input clock : Clock + | input in : UInt<32> + | input p : UInt<1> + | when p : + | assert(clock, eq(in, UInt<1>("h1")), UInt<1>("h1"), "assert0") + | else : + | skip""".stripMargin + val check = "assert(clock, eq(in, UInt<1>(\"h1\")), and(and(UInt<1>(\"h1\"), p), UInt<1>(\"h1\")), \"assert0\")" + executeTest(input, check, true) + } } class ExpandWhensExecutionTest extends ExecutionTest("ExpandWhens", "/passes/ExpandWhens") diff --git a/src/test/scala/firrtlTests/LoweringCompilersSpec.scala b/src/test/scala/firrtlTests/LoweringCompilersSpec.scala index cc4914f2..75f2ea02 100644 --- a/src/test/scala/firrtlTests/LoweringCompilersSpec.scala +++ b/src/test/scala/firrtlTests/LoweringCompilersSpec.scala @@ -173,7 +173,9 @@ class LoweringCompilersSpec extends FlatSpec with Matchers { Dependency[firrtl.passes.InferWidths])), Del(14), Add(15, Seq(Dependency(firrtl.passes.ResolveKinds), - Dependency(firrtl.passes.InferTypes))) + Dependency(firrtl.passes.InferTypes))), + // TODO + Add(17, Seq(Dependency[firrtl.transforms.formal.AssertSubmoduleAssumptions])) ) compare(legacyTransforms(new HighFirrtlToMiddleFirrtl), tm, patches) } @@ -351,7 +353,9 @@ class LoweringCompilersSpec extends FlatSpec with Matchers { Seq(new Transforms.LowToLow, new firrtl.MinimumVerilogEmitter) val tm = (new TransformManager(Seq(Dependency[firrtl.MinimumVerilogEmitter], Dependency[Transforms.LowToLow]))) val patches = Seq( - Add(62, Seq(Dependency[firrtl.transforms.LegalizeAndReductionsTransform])) + Add(63, Seq( + Dependency[firrtl.transforms.formal.RemoveVerificationStatements], + Dependency[firrtl.transforms.LegalizeAndReductionsTransform])) ) compare(expected, tm, patches) } @@ -362,7 +366,9 @@ class LoweringCompilersSpec extends FlatSpec with Matchers { Seq(new Transforms.LowToLow, new firrtl.VerilogEmitter) val tm = (new TransformManager(Seq(Dependency[firrtl.VerilogEmitter], Dependency[Transforms.LowToLow]))) val patches = Seq( - Add(69, Seq(Dependency[firrtl.transforms.LegalizeAndReductionsTransform])) + Add(70, Seq( + Dependency[firrtl.transforms.formal.RemoveVerificationStatements], + Dependency[firrtl.transforms.LegalizeAndReductionsTransform])) ) compare(expected, tm, patches) } diff --git a/src/test/scala/firrtlTests/formal/AssertSubmoduleAssumptionsSpec.scala b/src/test/scala/firrtlTests/formal/AssertSubmoduleAssumptionsSpec.scala new file mode 100644 index 00000000..edfd31d3 --- /dev/null +++ b/src/test/scala/firrtlTests/formal/AssertSubmoduleAssumptionsSpec.scala @@ -0,0 +1,108 @@ + +package firrtlTests.formal + +import firrtl.{CircuitState, Parser, Transform, UnknownForm} +import firrtl.testutils.FirrtlFlatSpec +import firrtl.transforms.formal.AssertSubmoduleAssumptions +import firrtl.stage.{Forms, TransformManager} + +class AssertSubmoduleAssumptionsSpec extends FirrtlFlatSpec { + behavior of "AssertSubmoduleAssumptions" + + val transforms = new TransformManager(Forms.HighForm, Forms.MinimalHighForm) + .flattenedTransformOrder ++ Seq(new AssertSubmoduleAssumptions) + + def run(input: String, check: Seq[String], debug: Boolean = false): Unit = { + val circuit = Parser.parse(input.split("\n").toIterator) + val result = transforms.foldLeft(CircuitState(circuit, UnknownForm)) { + (c: CircuitState, p: Transform) => p.runTransform(c) + } + val lines = result.circuit.serialize.split("\n") map normalized + + if (debug) { + println(lines.mkString("\n")) + } + + for (ch <- check) { + lines should contain (ch) + } + } + + it should "convert `assume` to `assert` in a submodule" in { + val input = + """circuit Test : + | module Test : + | input clock : Clock + | input reset : UInt<1> + | input in : UInt<8> + | output out : UInt<8> + | inst sub of Sub + | sub.clock <= clock + | sub.reset <= reset + | sub.in <= in + | out <= sub.out + | assume(clock, eq(in, UInt(0)), UInt(1), "assume0") + | assert(clock, eq(out, UInt(0)), UInt(1), "assert0") + | + | module Sub : + | input clock : Clock + | input reset : UInt<1> + | input in : UInt<8> + | output out : UInt<8> + | out <= in + | assume(clock, eq(in, UInt(1)), UInt(1), "assume1") + | assert(clock, eq(out, UInt(1)), UInt(1), "assert1") + |""".stripMargin + + val check = Seq( + "assert(clock, eq(in, UInt<1>(\"h1\")), UInt<1>(\"h1\"), \"assume1\")" + ) + run(input, check) + } + + it should "convert `assume` to `assert` in a nested submodule" in { + val input = + """circuit Test : + | module Test : + | input clock : Clock + | input reset : UInt<1> + | input in : UInt<8> + | output out : UInt<8> + | inst sub of Sub + | sub.clock <= clock + | sub.reset <= reset + | sub.in <= in + | out <= sub.out + | assume(clock, eq(in, UInt(0)), UInt(1), "assume0") + | assert(clock, eq(out, UInt(0)), UInt(1), "assert0") + | + | module Sub : + | input clock : Clock + | input reset : UInt<1> + | input in : UInt<8> + | output out : UInt<8> + | inst nestedSub of NestedSub + | nestedSub.clock <= clock + | nestedSub.reset <= reset + | nestedSub.in <= in + | out <= nestedSub.out + | assume(clock, eq(in, UInt(1)), UInt(1), "assume1") + | assert(clock, eq(out, UInt(1)), UInt(1), "assert1") + | + | module NestedSub : + | input clock : Clock + | input reset : UInt<1> + | input in : UInt<8> + | output out : UInt<8> + | out <= in + | assume(clock, eq(in, UInt(2)), UInt(1), "assume2") + | assert(clock, eq(out, UInt(2)), UInt(1), "assert2") + |""".stripMargin + + val check = Seq( + "assert(clock, eq(in, UInt<1>(\"h1\")), UInt<1>(\"h1\"), \"assume1\")", + "assert(clock, eq(in, UInt<2>(\"h2\")), UInt<1>(\"h1\"), \"assume2\")" + ) + run(input, check) + } +} diff --git a/src/test/scala/firrtlTests/formal/RemoveVerificationStatementsSpec.scala b/src/test/scala/firrtlTests/formal/RemoveVerificationStatementsSpec.scala new file mode 100644 index 00000000..10e63ae4 --- /dev/null +++ b/src/test/scala/firrtlTests/formal/RemoveVerificationStatementsSpec.scala @@ -0,0 +1,70 @@ + +package firrtlTests.formal + +import firrtl.{CircuitState, Parser, Transform, UnknownForm} +import firrtl.stage.{Forms, TransformManager} +import firrtl.testutils.FirrtlFlatSpec +import firrtl.transforms.formal.RemoveVerificationStatements + +class RemoveVerificationStatementsSpec extends FirrtlFlatSpec { + behavior of "RemoveVerificationStatements" + + val transforms = new TransformManager(Forms.HighForm, Forms.MinimalHighForm) + .flattenedTransformOrder ++ Seq(new RemoveVerificationStatements) + + def run(input: String, antiCheck: Seq[String], debug: Boolean = false): Unit = { + val circuit = Parser.parse(input.split("\n").toIterator) + val result = transforms.foldLeft(CircuitState(circuit, UnknownForm)) { + (c: CircuitState, p: Transform) => p.runTransform(c) + } + val lines = result.circuit.serialize.split("\n") map normalized + + if (debug) { + println(lines.mkString("\n")) + } + + for (ch <- antiCheck) { + lines should not contain (ch) + } + } + + it should "remove all verification statements" in { + val input = + """circuit Test : + | module Test : + | input clock : Clock + | input reset : UInt<1> + | input in : UInt<8> + | output out : UInt<8> + | inst sub of Sub + | sub.clock <= clock + | sub.reset <= reset + | sub.in <= in + | out <= sub.out + | assume(clock, eq(in, UInt(0)), UInt(1), "assume0") + | assert(clock, eq(out, UInt(0)), UInt(1), "assert0") + | cover(clock, eq(out, UInt(0)), UInt(1), "cover0") + | + | module Sub : + | input clock : Clock + | input reset : UInt<1> + | input in : UInt<8> + | output out : UInt<8> + | out <= in + | assume(clock, eq(in, UInt(1)), UInt(1), "assume1") + | assert(clock, eq(out, UInt(1)), UInt(1), "assert1") + | cover(clock, eq(out, UInt(1)), UInt(1), "cover1") + |""".stripMargin + + val antiCheck = Seq( + "assume(clock, eq(in, UInt<1>(\"h0\")), UInt<1>(\"h1\"), \"assume0\")", + "assert(clock, eq(out, UInt<1>(\"h0\")), UInt<1>(\"h1\"), \"assert0\")", + "cover(clock, eq(out, UInt<1>(\"h0\")), UInt<1>(\"h1\"), \"cover0\")", + "assume(clock, eq(in, UInt<1>(\"h1\")), UInt<1>(\"h1\"), \"assume1\")", + "assert(clock, eq(out, UInt<1>(\"h1\")), UInt<1>(\"h1\"), \"assert1\")", + "cover(clock, eq(out, UInt<1>(\"h1\")), UInt<1>(\"h1\"), \"cover1\")" + ) + run(input, antiCheck) + } + +} diff --git a/src/test/scala/firrtlTests/formal/VerificationSpec.scala b/src/test/scala/firrtlTests/formal/VerificationSpec.scala new file mode 100644 index 00000000..0b160082 --- /dev/null +++ b/src/test/scala/firrtlTests/formal/VerificationSpec.scala @@ -0,0 +1,55 @@ +package firrtlTests.formal + +import firrtl.{SystemVerilogCompiler} +import firrtl.testutils.FirrtlFlatSpec +import logger.{LogLevel, Logger} + +class VerificationSpec extends FirrtlFlatSpec { + behavior of "Formal" + + it should "generate SystemVerilog verification statements" in { + val compiler = new SystemVerilogCompiler + val input = + """circuit Asserting : + | module Asserting : + | input clock: Clock + | input reset: UInt<1> + | input in: UInt<8> + | output out: UInt<8> + | wire areEqual: UInt<1> + | wire inputEquals0xAA: UInt<1> + | wire outputEquals0xAA: UInt<1> + | out <= in + | areEqual <= eq(out, in) + | inputEquals0xAA <= eq(in, UInt<8>("hAA")) + | outputEquals0xAA <= eq(out, UInt<8>("hAA")) + | node true = UInt("b1") + | assume(clock, inputEquals0xAA, true, "assume input is 0xAA") + | assert(clock, areEqual, true, "assert that output equals input") + | cover(clock, outputEquals0xAA, true, "cover output is 0xAA") + |""".stripMargin + val expected = + """module Asserting( + | input [7:0] in, + | output [7:0] out + |); + | wire areEqual = out == in; + | wire inputEquals0xAA = in == 8'haa; + | wire outputEquals0xAA = out == 8'haa; + | assign out = in; + | always @(posedge clock) begin + | if (1'h1) begin + | assume(inputEquals0xAA); + | end + | if (1'h1) begin + | assert(areEqual); + | end + | if (1'h1) begin + | cover(outputEquals0xAA); + | end + | end + |endmodule + |""".stripMargin.split("\n") map normalized + executeTest(input, expected, compiler) + } +} diff --git a/src/test/scala/firrtlTests/stage/FirrtlMainSpec.scala b/src/test/scala/firrtlTests/stage/FirrtlMainSpec.scala index bd6d3ac7..5c8f1129 100644 --- a/src/test/scala/firrtlTests/stage/FirrtlMainSpec.scala +++ b/src/test/scala/firrtlTests/stage/FirrtlMainSpec.scala @@ -200,8 +200,7 @@ class FirrtlMainSpec extends AnyFeatureSpec with GivenWhenThen with Matchers wit FirrtlMainTest(args = Array("-X", "verilog", "-E", "verilog", "-foaf", "foo.anno"), files = Seq("Top.v", "foo.anno.anno.json")), FirrtlMainTest(args = Array("-X", "sverilog", "-E", "sverilog", "-foaf", "foo.json"), - files = Seq("Top.sv", "foo.json.anno.json"), - stdout = Some("SystemVerilog Compiler behaves the same as the Verilog Compiler!")), + files = Seq("Top.sv", "foo.json.anno.json")), /* Test all one file per module emitters */ FirrtlMainTest(args = Array("-X", "none", "-e", "chirrtl"), @@ -215,8 +214,7 @@ class FirrtlMainSpec extends AnyFeatureSpec with GivenWhenThen with Matchers wit FirrtlMainTest(args = Array("-X", "verilog", "-e", "verilog"), files = Seq("Top.v", "Child.v")), FirrtlMainTest(args = Array("-X", "sverilog", "-e", "sverilog"), - files = Seq("Top.sv", "Child.sv"), - stdout = Some("SystemVerilog Compiler behaves the same as the Verilog Compiler!")), + files = Seq("Top.sv", "Child.sv")), /* Test mixing of -E with -e */ FirrtlMainTest(args = Array("-X", "middle", "-E", "high", "-e", "middle"), @@ -235,8 +233,7 @@ class FirrtlMainSpec extends AnyFeatureSpec with GivenWhenThen with Matchers wit FirrtlMainTest(args = Array("-X", "verilog", "-E", "verilog", "-o", "foo.sv"), files = Seq("foo.sv.v")), FirrtlMainTest(args = Array("-X", "sverilog", "-E", "sverilog", "-o", "Foo"), - files = Seq("Foo.sv"), - stdout = Some("SystemVerilog Compiler behaves the same as the Verilog Compiler!")) + files = Seq("Foo.sv")) ) .foreach(runStageExpectFiles) |