Formal Test Bench Generation Reduces Design Verification Effort

Verity-Validation represents a new breed of dynamic property checking tool that uses static formal analysis techniques to generate a test-bench that is simulated dynamically using a traditional logic simulator.

Static Formal Analysis Targets Functional Properties

Verity-Validation statically analyzes RTL design descriptions and automatically extracts properties from classes of pre-defined, time-invariant, functional properties. The extracted properties are formally targeted during test-bench generation resulting in a test-bench that is formally proven to cover targeted properties. Unlike previous "intelligent random" or simulation vector based approaches, formal state-space search, rather than random or semi-formal, techniques are used. The new approach is deterministic and formally proves that extracted properties are covered by the test-bench. Extracted properties include incorrect logic function implementation and incorrect case element activation

Observation based coverage of properties improves effectiveness

Observation based coverage is used to determine whether a property has been covered. In this approach, the effects of property violations must be propagated to points, such as system primary outputs, where they can be observed before they are counted as covered. Observation based coverage techniques are more accurate than traditional code coverage methods that merely check for code activation and do not check that the test-bench results in the effects of incorrect code behavior being observed. Verity-Validation's observation based coverage metrics let you see how well properties have been covered by the generated test-bench.

Automatically perform dynamic checking when static checking fails

Static property checking is a powerful technique that can often identify violations of required design behavior quickly. However, for some properties, static property checking may fail to complete and so is unable to verify that a design property holds. In such cases, the user typically has to fall back on time-consuming manual and constrained random test generation to try to cover the property. Verity-Validation is integrated with Verity-Check in the Design Verity tool suite so allowing users to automatically move to formal test bench generation if static property checking fails to complete. Formal test bench generation involves a static analysis of the state space that targets a new set of design properties and results in a test bench, which is simulated dynamically. This test bench is formally proven to cover targeted properties and Verity-Validation's coverage metrics show you how well the test bench covers your design - so increasing your confidence in the quality of your design.

Simulation seed states increase coverage of interesting state space areas

Verity-Validation works with existing assertion based verification strategies. Design Verity allows you to specify an initial state. Thus, you can run simulation to reach an interesting state and then perform static property checking and formal test bench generation starting from this seed state.During test bench generation, only required inputs are specified formally - the other inputs are left as don't cares, which are filled randomly. As with traditional test bench generation, multiple test cases can be generated starting from different random seeds, so allowing you to combine the benefits of formal and random test bench generation. In addition, you can perform multiple passes that target different paths for property violation detection so that properties can be covered many times under different conditions.

Formal test bench generation reduces manual test generation effort

Verity-Validation's high performance formal test-bench generation capability drastically reduces the amount of manual test-bench creation effort required and significantly increases your confidence that your design functions as expected.

Availability

Release 1.0 of Design Verity-Validation is available now on Solaris, Windows 2000/NT, Linux and HP UX11.  Subscription licenses start from $10,000.

Please contact our Webmaster with questions or comments.
© Copyright 1998-2002 Veritable Inc.  All rights reserved.