Camposano started by defending the need for verified designs by citing both the Hubble Telescope and Lockheed Martin Mars Polar Lander as engineering projects launched with insufficient validation. Similarly, he argued that complex, deep-submicron designs must not be launched without verification. Considering the breadth of design expertise in his audience, Camposano was preaching to the choir in lobbying for verification at the conference.

Camposano said the current stable of verification techniques require fractions of seconds for actual system hardware testing, tens of seconds for logic emulation, and up to 1.5 years for gate-level simulation. He said that traditional simulation is here to stay, but must be augmented by the three formal verification techniques now available if there is to be any hope of verifying huge designs. He stressed the proven technical and financial viability of static timing analysis (STA) tools — a $100 million dollar market — and equivalence checking tools — a $50 million market. Alternatively, Camposano said property-checking tools are currently without a market, although that could change in the near future.

In detailing static timing analysis, he said that using STA tools before layout addresses module netlists and constraints, while using the tools after layout facilitates parasitic extraction. The tools determine if a circuit meets its timing constraints by calculating paths and can be 100x faster than dynamic simulation techniques. The technical challenges for STA tools include the inability to analyze asynchronous circuits and analog logic. Additionally, the user must specify timing information for internally derived clocks. Future challenges include analyzing for crosstalk and evaluating signal integrity in the course of design, according to Camposano.

Equivalence checking tools are making their way into mainstream synchronous design by providing comparisons between RTL models and RTL designs, RTL models and gate-level designs, and between gate-level models and gate-level designs, he said. "Equivalence checking is significantly faster verification than gate-level simulation." Not surprisingly, Camposano had data from Synopsys tools to support his claim. Current challenges to the technique, he said, include concerns that the modules are too complex and that timing parameters are too dependent on functionality, while future challenges include developing methodologies for clock-gated designs and asynchronous bypass considerations.

Finally, Camposano turned to descriptions of property checking tools. He said that groups inside of design houses are already pursuing these techniques, although the commercial market has yet to provide adequate data to support third-party development. Property checking verifies that a design does or does not conform to a specified property under all possible sets of legal input conditions. Camposano said that the technique is ideal for verifying a high-level spec with an RTL implementation and can be used to verify that bus access is never guaranteed to two clients at the same time. The exhaustive nature of property checking makes it very attractive for verification, he said, but the excessive cost of symbolic computations and representations of all states that can possibly go bad is prohibitive in the current verification tools market.

In summary, Camposano defended the use of formal verification by arguing that such techniques may eliminate many bugs that traditional simulation techniques cannot find. He said that wide-spread adoption of formal verification is accelerating because "Titanic problems in design will emerge without enhanced verification."