Temporal (also known as sequential) logic can now be verified in addition to combinational logic, thanks to Prover Technology's Tempo proof engine. This next-generation product complements Prover 4.0, which only verifies combinational logic.
A proof engine is a software plug-in for verification tools that extend the host tool's native capability to perform automated logical reasoning, or a proof search, to reduce verification time. The engine analyzes logical models of circuit designs or system-control software, finding and identifying any bugs. If there are no bugs, the proof engine establishes this fact and provides proof.
Touted as the industry's first scalable proof engine for sequential system verification, Tempo targets EDA and computer-aided software engineering (CASE) tool developers. It provides automated reasoning for sequential logic to prove, for example, that two sequential systems behave in exactly the same way.
The proof engine searches for bugs while testing every possible contingency a design could en-counter. Bugs are then found and pinpointed. If no bugs are found, designers can be 100% sure that the design functions properly and will meet its specifications.
Tempo serves a variety of applications, including sequential equivalence checking, model checking, property validation, requirements validation, consistency and completeness checking, and test-case validation.
The one-year list price for a node-locked end-user license starts at $30,000, including support.
Prover Technology Inc., 100 S. Ellsworth Ave., 9th floor, San Mateo, CA 94401; Monika Claassen, (650) 696-3350; www.prover.com.
