FishTail’s timing-exception verification solution establishes if false and multi-cycle specifications are correct, i.e. supported by the logic, architecture and use model for a design. We strongly recommend verifying timing exceptions with RTL input but support netlist input as well. Our timing-exception verification solution, in particular multi-cycle path verification, is used as plan-of-record by leading semiconductor firms around the world, because it is complete, scales to handle large, complex designs and minimizes designer review effort, while eliminating a risk of silicon failure and the need for gate-level simulation.
Timing-Exception Verification Features
Verification of
False Paths
Verification of
Multi-Cycle Paths
What Makes us Different
Our exception verification solution scales to handle the largest designs, verifies all constrained paths, but the most significant value proposition of our solution is our unmatched signal to noise ratio. Unlike our competition, we do not synthesize RTL to gates and formally verify exceptions at the gate-level. Instead, we perform our analysis at the RTL level using a proprietary formal engine that has an excellent understanding of the state machines and control flow on a design. This allows us to formally prove as correct more exceptions than competing tools. For anything that fails formal proof we generate System Verilog Assertions (SVA) that is imported by designers into their existing RTL regressions. Since we have the same RTL view of a design as a simulator our SVA is compact and our assertions integrate seamlessly into all the major simulation tools. Designers review assertions that fail using the same debug techniques that they are already familiar with and typically have to review less than 1% of their timing exceptions using our formal + ABV flow.