Dynamic Assertions Using TXP

In this paper, we present a new temporal property specification language TXP. The language is designed to support dynamic monitoring of temporal properties at simulation runtime, as well as to provide the input specification for formal property checking. For design verification of hardware systems, hardware description languages (HDL) provide modeling capabilities, but they are inadequate for concise specification of complex assertions where logic relationships involve multi cycle behavior. TXP is a declarative language that provides a rich set of operators based on regular expressions over sequences of values and events. Its key features are to allow multi-cycle behavior, time shift operations in the past or future, conditional matching, repetition of sequences, and restrictions over sequences. The sequences can be constructed with logical connectives such as “and” and “or” to compose more complex assertions. A TXP engine has been developed to monitor the properties at runtime.