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

We formally verify if false paths are supported by the logic on the design. We account for the gating of timing paths in clock and datapath logic, and architectural considerations such as static registers, synchronizer endpoints, etc. We flag issues such as a false-path that applies to paths that it should not, or a false-path that is missing the required gating conditions.

Verification of Multi-Cycle Paths

We formally verify if multi-cycle paths (MCPs) are supported by the logic on the design. We verify MCPs specified between the same clocks, or between synchronous fast-to-slow, slow-to-fast clocks. We verify hold MCPs when required. We account for the sequential behavior of the design, the way counters and state machines assert enable signals in clock and datapaths, static configuration registers, metastable endpoints, etc. We catch bugs such as MCPs that are written too broadly, or where the gating logic is missing, or where an endpoint has a risk of metastability when it should not.

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.

SDC Verification Solutions

Download Documents

Formal Verification of MBIST MCPs

White paper

DOWNLOAD
Delay Safe False Paths

White paper

DOWNLOAD
DAC User Track Presentation

White paper

DOWNLOAD