diff options
Diffstat (limited to 'src/test/scala/firrtlTests/formal')
3 files changed, 233 insertions, 0 deletions
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) + } +} |