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
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
|
// SPDX-License-Identifier: Apache-2.0
package chiselTests
import chisel3._
import chisel3.experimental.{ChiselAnnotation, verification => formal}
import chisel3.stage.ChiselStage
import firrtl.annotations.{ReferenceTarget, SingleTargetAnnotation}
import org.scalatest.matchers.should.Matchers
import java.io.File
class SimpleTest extends Module {
val io = IO(new Bundle {
val in = Input(UInt(8.W))
val out = Output(UInt(8.W))
})
io.out := io.in
cover(io.in === 3.U)
when(io.in === 3.U) {
assume(io.in =/= 2.U)
assert(io.out === io.in)
}
}
/** Dummy verification annotation.
* @param target target of component to be annotated
*/
case class VerifAnnotation(target: ReferenceTarget) extends SingleTargetAnnotation[ReferenceTarget] {
def duplicate(n: ReferenceTarget): VerifAnnotation = this.copy(target = n)
}
object VerifAnnotation {
/** Create annotation for a given verification component.
* @param c component to be annotated
*/
def annotate(c: VerificationStatement): Unit = {
chisel3.experimental.annotate(new ChiselAnnotation {
def toFirrtl: VerifAnnotation = VerifAnnotation(c.toTarget)
})
}
}
class VerificationSpec extends ChiselPropSpec with Matchers {
def assertContains(s: Seq[String], x: String): Unit = {
val containsLine = s.map(_.contains(x)).reduce(_ || _)
assert(containsLine, s"\n $x\nwas not found in`\n ${s.mkString("\n ")}``")
}
property("basic equality check should work") {
val fir = ChiselStage.emitChirrtl(new SimpleTest)
val lines = fir.split("\n").map(_.trim)
// reset guard around the verification statement
assertContains(lines, "when _T_2 : @[VerificationSpec.scala")
assertContains(lines, "cover(clock, _T, UInt<1>(\"h1\"), \"\")")
assertContains(lines, "when _T_6 : @[VerificationSpec.scala")
assertContains(lines, "assume(clock, _T_4, UInt<1>(\"h1\"), \"\")")
assertContains(lines, "when _T_10 : @[VerificationSpec.scala")
assertContains(lines, "assert(clock, _T_8, UInt<1>(\"h1\"), \"\")")
}
property("annotation of verification constructs should work") {
/** Circuit that contains and annotates verification nodes. */
class AnnotationTest extends Module {
val io = IO(new Bundle {
val in = Input(UInt(8.W))
val out = Output(UInt(8.W))
})
io.out := io.in
val cov = cover(io.in === 3.U)
val assm = chisel3.assume(io.in =/= 2.U)
val asst = chisel3.assert(io.out === io.in)
VerifAnnotation.annotate(cov)
VerifAnnotation.annotate(assm)
VerifAnnotation.annotate(asst)
}
// compile circuit
val testDir = new File("test_run_dir", "VerificationAnnotationTests")
(new ChiselStage).emitSystemVerilog(
gen = new AnnotationTest,
args = Array("-td", testDir.getPath)
)
// read in annotation file
val annoFile = new File(testDir, "AnnotationTest.anno.json")
annoFile should exist
val annoLines = scala.io.Source.fromFile(annoFile).getLines.toList
// check for expected verification annotations
exactly(3, annoLines) should include("chiselTests.VerifAnnotation")
exactly(1, annoLines) should include("~AnnotationTest|AnnotationTest>asst")
exactly(1, annoLines) should include("~AnnotationTest|AnnotationTest>assm")
exactly(1, annoLines) should include("~AnnotationTest|AnnotationTest>cov")
// read in FIRRTL file
val firFile = new File(testDir, "AnnotationTest.fir")
firFile should exist
val firLines = scala.io.Source.fromFile(firFile).getLines.toList
// check that verification components have expected names
exactly(1, firLines) should include("cover(clock, _T, UInt<1>(\"h1\"), \"\") : cov")
exactly(1, firLines) should include("assume(clock, _T_3, UInt<1>(\"h1\"), \"\") : assm")
exactly(1, firLines) should include("assert(clock, _T_7, UInt<1>(\"h1\"), \"\") : asst")
}
property("annotation of verification constructs with suggested name should work") {
/** Circuit that annotates a renamed verification nodes. */
class AnnotationRenameTest extends Module {
val io = IO(new Bundle {
val in = Input(UInt(8.W))
val out = Output(UInt(8.W))
})
io.out := io.in
val goodbye = chisel3.assert(io.in === 1.U)
goodbye.suggestName("hello")
VerifAnnotation.annotate(goodbye)
VerifAnnotation.annotate(chisel3.assume(io.in =/= 2.U).suggestName("howdy"))
}
// compile circuit
val testDir = new File("test_run_dir", "VerificationAnnotationRenameTests")
(new ChiselStage).emitSystemVerilog(
gen = new AnnotationRenameTest,
args = Array("-td", testDir.getPath)
)
// read in annotation file
val annoFile = new File(testDir, "AnnotationRenameTest.anno.json")
annoFile should exist
val annoLines = scala.io.Source.fromFile(annoFile).getLines.toList
// check for expected verification annotations
exactly(2, annoLines) should include("chiselTests.VerifAnnotation")
exactly(1, annoLines) should include("~AnnotationRenameTest|AnnotationRenameTest>hello")
exactly(1, annoLines) should include("~AnnotationRenameTest|AnnotationRenameTest>howdy")
// read in FIRRTL file
val firFile = new File(testDir, "AnnotationRenameTest.fir")
firFile should exist
val firLines = scala.io.Source.fromFile(firFile).getLines.toList
// check that verification components have expected names
exactly(1, firLines) should include("assert(clock, _T, UInt<1>(\"h1\"), \"\") : hello")
exactly(1, firLines) should include("assume(clock, _T_4, UInt<1>(\"h1\"), \"\") : howdy")
}
}
|
