Veritable Inc. is announcing version 1.0 of its innovative Design Verity-Validation formal test bench generator. 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.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 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.
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. 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.
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.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.
About Veritable
Veritable Inc. is a privately held Electronic Design Automation company that provides innovative formal validation solutions and services. Veritable has headquarters in Mountain View, California. For
further information, visit the Veritable web-site at
