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
|
// SPDX-License-Identifier: Apache-2.0
package firrtl.transforms.formal
import firrtl._
import firrtl.ir._
import firrtl.options.Dependency
/** Convert Asserts
*
* Replaces all Assert nodes with a gated print-and-stop. This effectively
* emulates the assert for IEEE 1364 Verilog.
*/
object ConvertAsserts extends Transform with DependencyAPIMigration {
override def prerequisites = Nil
override def optionalPrerequisites = Nil
override def optionalPrerequisiteOf =
Seq(Dependency[VerilogEmitter], Dependency[MinimumVerilogEmitter], Dependency[RemoveVerificationStatements])
override def invalidates(a: Transform): Boolean = false
def convertAsserts(namespace: Namespace, stmt: Statement): Statement = stmt match {
case v: Verification if v.op == Formal.Assert =>
val nPred = DoPrim(PrimOps.Not, Seq(v.pred), Nil, v.pred.tpe)
val gatedNPred = DoPrim(PrimOps.And, Seq(nPred, v.en), Nil, v.pred.tpe)
val name = if (v.name.nonEmpty) { v.name }
else { namespace.newName("assert") }
val stop = Stop(v.info, 1, v.clk, gatedNPred, name)
v.msg match {
case StringLit("") => stop
case msg =>
val printName = namespace.newName(name + "_print")
Block(Print(v.info, msg, Nil, v.clk, gatedNPred, printName), stop)
}
case s => s.mapStmt(convertAsserts(namespace, _))
}
def execute(state: CircuitState): CircuitState = {
state.copy(circuit = state.circuit.mapModule { m =>
val namespace = Namespace(m)
// make sure the name assert is reserved
if (!namespace.contains("assert")) { namespace.newName("assert") }
m.mapStmt(convertAsserts(namespace, _))
})
}
}
|
