How Are Assertions Used?

There are two commonly accepted approaches to verification: black box testing and white box testing. Black box testing generates stimulus without any knowledge of the implementation and relies purely on external interfaces. White box testing generates stimulus based on knowledge of the

implementation. In practice, both black box and white box approaches are needed to verify a given design. This hybrid approach is usually referred to as “gray box” testing.

An extension of the white box approach is to write checks within the design, in addition to, or instead of, checking the response at the output. The checks are written at the point of implementation, using knowledge of the design’s internals, to verify certain characteristics—for example, simple checks

throughout the RTL for such things as state machines, FIFOs, or queues. Assertions can be used with both simulators and model checkers to verify a given design. Simulation environments are usually event-driven and rely on stimulus generation to drive the test. Model checkers are usually cycle-driven and apply mathematical algorithms to verify a design. Assertions can be utilized in both environments to verify a design.

Assertions in Simulation

In simulation, assertions can be used as functional checkers and/or coverage monitors. As checkers they can check invariants, protocols, and state machines in internal nodes, external interfaces, or any control logic. Assertion may also be used for data path applications, but in most cases procedural languages are better suited for data path designs, since these generally tend to deal with

movement of blocks of data rather than cycle-to-cycle interaction of signals. Assertions can also be used to track coverage. They act as indicators that specific sequences, series of events, have occurred in the stimulus or within the design. Each coverage assertion monitors a particular portion of the design and therefore provides an indication of the activity of that portion. This indication is different from traditional code coverage in the sense that assertions don’t just map statically to the RTL (for example, did this state transition happen?), but they also imply specific sequences of events within

Chapter One: The Art of Verification with SystemVerilog Assertions

© 2006 by Verification Central. All Rights Reserved. No part of this publication may be reproduced, stored in a retrieval system, or transmitted in any form or by any means, mechanical, photocopying, recording, or otherwise without the prior written permission of the publisher, Verification Central, Fremont, California.