SoC Test and Verification -> Assertions speed processor core verification

Assertions speed processor core verification
By Thomas L. Anderson, Vice President, Applications Engineering, 0-In Design Automation Inc., San Jose, Calif. , tla@0-In.com, EE Times
December 13, 2001 (11:08 a.m. EST)
URL: http://www.eetimes.com/story/OEG20011213S0028

Most of today's complex system-on-chip devices contain embedded processors; indeed some analysts insist that a chip must contain a processor even to qualify as an SoC. Quite often, the processor is licensed as a virtual component from a silicon vendor or an intellectual property provider so knowledge of its operation is limited. This is a serious concern for an SoC verification team, which must ensure that the processor is being used properly in the context of the full chip design.

Many embedded processor vendors include a set of "sanity tests" with known fault coverage for a standalone processor. The SoC verification team can use those tests to check the integrity of the delivered processor and may be able to leverage them for SoC manufacturing test. However, the tests are usually of limited value in ensuring that the processor is functioning properly within the SoC device and that rules for processor usage are followed during verification.

Ano ther popular approach is the use of assertions — statements of designer intent — to improve verification for complex SoC devices. Assertion-based methodologies are being adopted widely and are entirely applicable to SoC designs containing embedded processors. If both the processor vendor and the SoC verification team adopt and embrace assertions, the end result is faster, more thorough verification of the SoC.

Assertions can be expressed in a number of different ways, including RTL code, RTL libraries, inline directives, testbench languages and traditional formal verification languages. Whatever the form of expression, there are at least three key areas for assertions associated with an embedded processor:

• Handshaking and protocol rules on the processor interface.

• Operational rules specific to the processor instruction set.

• Checks for proper behavior of internal design structures.

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.

It is in the best interests of both an embedded processor supplier and its SoC customers to ensure successful integration. A customer that has to refabricate an SoC due to a bug in the processor interface logic will blame the vendor for not providing more verification assistance.