Debugging Assertions and Efficiency Considerations
Properties and sequences allow us to describe complex behaviors in a very compact declarative form. That form is quite different from the procedural style used for writing RTL and other design models as well as test benches. Thus, assertions may also need a different style for debugging them. Issues related to the runtime and memory overheads for complex temporal assertions also need to be addressed. The same behavior may be expressed using different assertions. Each may have different efficiency in formal verification and simulation. We discuss both debugging and efficiency in this chapter.