Design Verity-Check was announced at DAC today and is available now, Design Verity-Validation will be formally introduced in 2002, and Design Verity-CPU, which was also announced today, is available now as a services plus solutions package.

Design Verity-Check

Verity-Check automatically extracts and checks numerous design properties. It offers four levels of checks:

• · Traditional rule based "look ahead" checks such as synthesis, testability and re-use methodology checks, where designers don't have to specify anything except the RTL design to check.
• · Automatic checks of pre-defined properties, where designers only need to specify the design, and optionally design clocks and reset ports
• · Automatic checks of predefined properties where designers also specify the signals to check, and
• · User specified, cycle-bound, temporal property checks where users additionally specify temporal value constraints

The ease of use methodology of Verity-Check allows designers to graduate to more and more powerful checks as their design cycle progresses by providing more information in the form of signal constraints and assertions.

Unlike traditional model checking which requires the designer to specify properties to be checked using a complex temporal logic based language, Verity-Check offers highly specific pre-defined checks that are fully automated. There's no new language to learn, and no configuration or set-up is required. These automatic search-based checks include branch possible, initialization, set-reset conflicts, bus-conflict and floating bus checks in which the tool automatically extracts properties from the design HDL In addition to automatic property extraction and checking, Verity-Check includes powerful checks such as one-hot checks that exhaustively verify, without simulation, that user specified nets are uniquely decoded or one-hot. Verity-Check's constraint capability allows the user to constrain the search, if desired, by specifying temporal conditions that must hold during the check. If a property violation is found then Verity-check generates a counter-example consisting of the test sequence that results in the violation. An example of a bug found in a real customer design using Verity-Check's one hot checking capability was a pipeline control module in which bypass select signals were supposed to be uniquely decoded but under certain conditions two bits of the control signals became active at the same time. This bug escaped detection despite months of random and directed simulation but Verity-Check was able to detect the bug in under a minute.

Verity-check is a high capacity, high performance tool that has been run on customer designs as large as 4M gates. Run times depend on the properties being checked but examples of run times achieved by customers were 2 hours for a four million equivalent gate ASIC and 8 hours for a 500K equivalent gate CPU.

Design Verity-Validation

Verity-Validation is a breakthrough dynamic property checker that performs a formal RTL analysis, automatically extracts design properties and generates a formal test bench. Unlike random, biased pseudo-random or so-called "intelligent" random approaches the test bench is formally proven to uncover discrepancies in design behavior between the RTL and the behavioral model of the design for the extracted properties.

Design Verity-CPU

Verity-CPU consists of three major software modules:

• · An innovative targeted instruction stream generator that performs formal analysis of the RTL and generates assembly code instruction streams targeted at particular areas of the RTL design,
• · A traditional biased random instruction stream generator that utilizes user templates and weights to create instruction streams, and
• · A coverage directed random instruction stream generator that increases instruction permutation and instruction sequence coverage.

Verity-CPU has been used in production on several CPUs and has detected dozens of bugs in production use - including several bugs in a CPU that had already taped out and a late stage micro-architectural bug in a seven stage pipelined processor.

Design Verity Tool Suite has Detected Dozens of Bugs in Production Use

The Design Verity products have been used in production and have detected dozens of hard-to-detect bugs in complex designs. Veritable's customers have taped-out three designs using the tools.