DesignCon 2005 paper on using formal verification to verify the correctness of false-path and multi-cycle path constraints in SDC files.
DesignCon 2005 paper on using formal verification to verify that AMBA-compliant IP strictly adheres to ARM's bus protocol.
Cisco presents experience with Solidify and wins award for Best Design Case paper in System-on-Chip at DesignCon 2000.
The increasing complexity of system-on-a-chip and ASIC designs has caused an ever-widening gap between what can be designed and what can be verified. It is estimated that between 50-70% of the time required to design a complex IC is spent in verifying that the functionality of the system is correct. Bugs in a design are least expensive to fix just after they are created. At this stage the design is still fresh in the designer's mind and other parts of the project or other design team members are unaffected. Bugs are at least an order of magnitude more expensive to fix during system integration. In this phase it takes more time and people to analyze the cause, regression tests must be rerun, and the entire group may be delayed. These challenges are giving rise to some exciting new tools and approaches in Verification techniques.
The growing complexity of ASICs and programmable parts means functional verification is the nightmare that keeps projects managers up at night. Designers are creating ASICs that can't be completely verified in a reasonable time with the talent and computing resources they have available. As a result of the gap between what can be designed and what can be verified, achieving a functionally stable design is difficult and involves many iterations. This paper presents Solidification, a new low-risk methodology for faster debug of ASICs and programmable parts that significantly reduces verification time and effort while increasing quality and robustness of designs.
Paper by Mike Turpin of ARM, Ltd., describing how to use Solidify for Sequential Equivalence check in order to uncover hidden "X" values in a design. This is particularly important for an IP provider where the RTL may be implemented using different synthesis flows. Hidden X's can cause differences between RTL simulation and the actual silicon, which are not caught by design flows that rely on other tools such as Logical Equivalence checking.