1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
|
// SPDX-License-Identifier: Apache-2.0
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)
}
}
|
