SoC Test and Verification -> Assertions speed processor core verification

If the processor vendor provides assertions for these three areas, the SoC team will have an easier time integrating the processor into the chip and ensuring that it is working correctly. This is most obvious for the assertions that capture the interface rules. If the SoC designer connects the processor incorrectly or the verification team writes tests that stimulate the processor incorrectly, this will be detected as a protocol violation during simulation.

Processors are usually designed to handle only legal input sequences on the interface, so misuse of the interface can often put the processor into an illegal or inconsistent state. Without a robust set of protocol rule checks, the SoC designer will most likely suspect that an illegal state is the result of a bug in the processor. Experienced providers of virtual components have learned that a high-quality interface protocol monitor saves the support costs of solving problems when customers don't follow the rules.

Some of the most complicated operational rules for a processor involve its instruction set sequences and the interactions between different instructions in the execution pipeline. Not only can these rules be captured by assertions, but in fact the assertions often look much like protocol rules.

An embedded processor contains a number of common design structures whose operation can also be checked by assertions. Rules to be checked might include:

• A state machine never makes any illegal transitions.

• A controller never gets into a trap state.

• An arbiter follows the intended arbitration scheme.

• No memory location is ever read before it has been written.

All those rules can be easily checked with an assertion library that provides "reference models" for common design structures. A violation of such rules in simulation might indicate misuse of the processor, or possibly an inter nal design flaw in the embedded processor itself. In either case, it is far better for the SoC team to find out about the problem during verification than when debugging an actual chip in the bring-up lab.

With proper specification, assertions are useful with formal verification tools as well as in simulation. This approach allows an embedded processor provider to target the internal assertions and the output protocol rules using formal techniques while respecting the input protocol rules as constraints. The goal is to see if any possible legal input sequence on the processor interface could ever violate the rules for proper processor operation.

If the assertions for the protocol rules are specified properly, it is possible for the SoC verification team to use formal verification methods as well. The constraints are simply reversed, so that the formal analysis checks to see whether any legal output sequences from the processor could cause problems for the SoC interface logic.

Tensilica, Inc. is a vendor of embedded processors using an assertion-based methodology successfully. Tensilica uses 0-In Design Automation's CheckerWare library of assertion checkers to capture the rules for proper operation of both the processor interface and the internal structures for its Xtensa IV configurable processor. Many of the checkers in the library map directly to such common design structures as memories, FIFOs, pipelines and state machines. Other checkers allow easy specification of temporal rules for complex protocols.

Designers specify the 0-In checkers with inline, in-context directives that adapt to the surrounding RTL. This is especially important for a configurable design, since it is not necessary to write a new set of assertions for each variation of the embedded processor. For example, identical directives can be used to specify a bus assertion in different processor configurations with different bus widths.