Applications of Specification

Today’s increasing design complexity requires innovative methods for verification
and debug. With verification consuming up to 70% of the design cycle,
assertion-based design (Foster et al., 2003) is viewed as one key method for
improving productivity. An assertion is a design property that is declared to
be true and should be evaluated by one or more techniques among simulation,
emulation, or formal verification. The introduction of new standard languages
such as Property Specification Language (PSL) or SystemVerilog has made assertions
more easy to write and very powerful. An assertion can also be seen
as a high-level functional specification for a circuit intended for monitoring of
events over time.
We developed an original method for generating hardware that monitors signals
whose behavior is specified by logical and temporal properties under the
form of assertions in declarative form. In this chapter, we shall use Accellera’s
PSL standard (Accellera, 2003, 2004) and assume the reader to be familiar
with its basic concepts. The method is founded on a library of primitive digital
components and a technique to interconnect them, resulting in a digital
module that can be properly connected to the signals of interest. Monitoring
can be initialized and started independently from the system under scrutiny;
it runs concurrently with the system under verification and notifies its environment when the property checking is terminated with a true or false value
or whether the property is still being evaluated, possibly with a transient false
value. Properties over finite and infinite state sequences over time are covered
by the method. Monitors under this method may be used for design verification
by simulation. But their primary use is online checking during either hardware
emulation for debug or normal system operation for safety-critical property
checking.