diff options
5 files changed, 96 insertions, 0 deletions
diff --git a/core/src/main/scala/chisel3/experimental/verification/package.scala b/core/src/main/scala/chisel3/experimental/verification/package.scala new file mode 100644 index 00000000..a983a6fd --- /dev/null +++ b/core/src/main/scala/chisel3/experimental/verification/package.scala @@ -0,0 +1,41 @@ +// See LICENSE for license details. + +package chisel3.experimental + +import chisel3.{Bool, CompileOptions} +import chisel3.internal.Builder +import chisel3.internal.Builder.pushCommand +import chisel3.internal.firrtl.{Formal, Verification} +import chisel3.internal.sourceinfo.SourceInfo + +package object verification { + object assert { + def apply(predicate: Bool, msg: String = "")( + implicit sourceInfo: SourceInfo, + compileOptions: CompileOptions): Unit = { + val clock = Builder.forcedClock + pushCommand(Verification(Formal.Assert, sourceInfo, clock.ref, + predicate.ref, msg)) + } + } + + object assume { + def apply(predicate: Bool, msg: String = "")( + implicit sourceInfo: SourceInfo, + compileOptions: CompileOptions): Unit = { + val clock = Builder.forcedClock + pushCommand(Verification(Formal.Assume, sourceInfo, clock.ref, + predicate.ref, msg)) + } + } + + object cover { + def apply(predicate: Bool, msg: String = "")( + implicit sourceInfo: SourceInfo, + compileOptions: CompileOptions): Unit = { + val clock = Builder.forcedClock + pushCommand(Verification(Formal.Cover, sourceInfo, clock.ref, + predicate.ref, msg)) + } + } +} diff --git a/core/src/main/scala/chisel3/internal/firrtl/Converter.scala b/core/src/main/scala/chisel3/internal/firrtl/Converter.scala index 67d87a68..304ddec6 100644 --- a/core/src/main/scala/chisel3/internal/firrtl/Converter.scala +++ b/core/src/main/scala/chisel3/internal/firrtl/Converter.scala @@ -125,6 +125,14 @@ private[chisel3] object Converter { val (fmt, args) = unpack(pable, ctx) Some(fir.Print(convert(info), fir.StringLit(fmt), args.map(a => convert(a, ctx)), convert(clock, ctx), firrtl.Utils.one)) + case Verification(op, info, clk, pred, msg) => + val firOp = op match { + case Formal.Assert => fir.Formal.Assert + case Formal.Assume => fir.Formal.Assume + case Formal.Cover => fir.Formal.Cover + } + Some(fir.Verification(firOp, convert(info), convert(clk, ctx), + convert(pred, ctx), firrtl.Utils.one, fir.StringLit(msg))) case _ => None } diff --git a/core/src/main/scala/chisel3/internal/firrtl/IR.scala b/core/src/main/scala/chisel3/internal/firrtl/IR.scala index 89bc4a63..44fdb833 100644 --- a/core/src/main/scala/chisel3/internal/firrtl/IR.scala +++ b/core/src/main/scala/chisel3/internal/firrtl/IR.scala @@ -735,6 +735,13 @@ case class ConnectInit(sourceInfo: SourceInfo, loc: Node, exp: Arg) extends Comm case class Stop(sourceInfo: SourceInfo, clock: Arg, ret: Int) extends Command case class Port(id: Data, dir: SpecifiedDirection) case class Printf(sourceInfo: SourceInfo, clock: Arg, pable: Printable) extends Command +object Formal extends Enumeration { + val Assert = Value("assert") + val Assume = Value("assume") + val Cover = Value("cover") +} +case class Verification(op: Formal.Value, sourceInfo: SourceInfo, clock: Arg, + predicate: Arg, message: String) extends Command abstract class Component extends Arg { def id: BaseModule def name: String diff --git a/src/main/scala/chisel3/internal/firrtl/Emitter.scala b/src/main/scala/chisel3/internal/firrtl/Emitter.scala index be8d8f2f..36ac8710 100644 --- a/src/main/scala/chisel3/internal/firrtl/Emitter.scala +++ b/src/main/scala/chisel3/internal/firrtl/Emitter.scala @@ -80,6 +80,8 @@ private class Emitter(circuit: Circuit) { val printfArgs = Seq(e.clock.fullName(ctx), "UInt<1>(1)", "\"" + printf.format(fmt) + "\"") ++ args printfArgs mkString ("printf(", ", ", ")") + case e: Verification => s"${e.op}(${e.clock.fullName(ctx)}, ${e.predicate.fullName(ctx)}, " + + s"UInt<1>(1), " + "\"" + s"${printf.format(e.message)}" + "\")" case e: DefInvalid => s"${e.arg.fullName(ctx)} is invalid" case e: DefInstance => s"inst ${e.name} of ${e.id.name}" case w: WhenBegin => diff --git a/src/test/scala/chiselTests/experimental/verification/VerificationSpec.scala b/src/test/scala/chiselTests/experimental/verification/VerificationSpec.scala new file mode 100644 index 00000000..521c16a3 --- /dev/null +++ b/src/test/scala/chiselTests/experimental/verification/VerificationSpec.scala @@ -0,0 +1,38 @@ +// See LICENSE for license details. + +package chiselTests.experimental.verification + +import chisel3._ +import chisel3.experimental.{verification => formal} +import chisel3.stage.ChiselStage +import chiselTests.ChiselPropSpec + +class VerificationModule extends Module { + val io = IO(new Bundle{ + val in = Input(UInt(8.W)) + val out = Output(UInt(8.W)) + }) + io.out := io.in + formal.cover(io.in === 3.U) + when (io.in === 3.U) { + formal.assume(io.in =/= 2.U) + formal.assert(io.out === io.in) + } +} + +class VerificationSpec extends ChiselPropSpec { + + def assertContains[T](s: Seq[T], x: T): Unit = { + val containsLine = s.map(_ == x).reduce(_ || _) + assert(containsLine, s"\n $x\nwas not found in`\n ${s.mkString("\n ")}``") + } + + property("basic equality check should work") { + val stage = new ChiselStage + val fir = stage.emitFirrtl(new VerificationModule) + val lines = fir.split("\n").map(_.trim) + assertContains(lines, "cover(clock, _T, UInt<1>(\"h1\"), \"\") @[VerificationSpec.scala 16:15]") + assertContains(lines, "assume(clock, _T_2, UInt<1>(\"h1\"), \"\") @[VerificationSpec.scala 18:18]") + assertContains(lines, "assert(clock, _T_3, UInt<1>(\"h1\"), \"\") @[VerificationSpec.scala 19:18]") + } +} |