aboutsummaryrefslogtreecommitdiff
path: root/src/test
diff options
context:
space:
mode:
Diffstat (limited to 'src/test')
-rw-r--r--src/test/scala/firrtlTests/formal/VerificationSpec.scala5
1 files changed, 5 insertions, 0 deletions
diff --git a/src/test/scala/firrtlTests/formal/VerificationSpec.scala b/src/test/scala/firrtlTests/formal/VerificationSpec.scala
index 0b160082..22dbc1f1 100644
--- a/src/test/scala/firrtlTests/formal/VerificationSpec.scala
+++ b/src/test/scala/firrtlTests/formal/VerificationSpec.scala
@@ -1,3 +1,5 @@
+// See LICENSE for license details.
+
package firrtlTests.formal
import firrtl.{SystemVerilogCompiler}
@@ -38,12 +40,15 @@ class VerificationSpec extends FirrtlFlatSpec {
| wire outputEquals0xAA = out == 8'haa;
| assign out = in;
| always @(posedge clock) begin
+ | // assume input is 0xAA
| if (1'h1) begin
| assume(inputEquals0xAA);
| end
+ | // assert that output equals input
| if (1'h1) begin
| assert(areEqual);
| end
+ | // cover output is 0xAA
| if (1'h1) begin
| cover(outputEquals0xAA);
| end