Hardware/software verification enters the atomic age: Part 1

George Harper

March 23, 2008

George Harper

The active rules, where the guards are true, can be applied in parallel, but each rule operates as an atomic transaction--each rule observes and ensures a consistent state relative to all other rules in the system.

This atomicity model is popular because it enables concurrent behavioral descriptions of the highest abstraction and simplifies the reasoning around correctness.

TRS expresses atomicity
One example of a high-level specification language using this computational model is the term rewriting system (TRS). TRSs offer a convenient way to describe parallel and asynchronous systems and prove an implementation's correctness with respect to a specification. TRS descriptions, augmented with proper information about the system building blocks, also hold the promise of high-level synthesis. High-level architectural descriptions that are both automatically synthesizable and verifiable would permit architectural exploration at a fraction of the time and cost required by current commercial tools.

A TRS is defined as a tuple (S, R, S₀), where S is a set of terms, R is a set of rewriting rules, and S₀ is a set of initial terms. The state of a system is represented as a TRS term, while the state transitions are represented as TRS rules. The general structure of rewriting rules is:

where s₁ and s₂ are terms, and p is a predicate. We can use a rule to rewrite a term if the rule's left-hand-side pattern matches the term or one of its subterms, and the corresponding predicate is true. The new term is generated in accordance with the rule's right-hand side.

If several rules apply, then any one of them can be applied. If no rule applies, the term cannot be rewritten any further. In practice, we often use abstract data types such as arrays and FIFO queues to make the descriptions more readable.

With proper abstractions, we can create TRS descriptions in a highly modular fashion. And using a compiler for hardware synthesis from TSRs, such descriptions can be translated into a standard hardware description language like Verilog. By restricting the generated Verilog to be structural, commercial tools can be used to go all the way down to gates and layout.

The terms' grammar, when augmented with details such as instruction formats and sizes of various register files, buffers, memories, and so on, precisely specifies the state elements.