Synopsys adds formal, CDC, low-power checks to Verification Compiler
Synopsys has added formal, clock-domain crossing, and low-power checking tools to its verification offering. They’ll be available as part of Verification Compiler or standalone.
Linting tools are expected to follow by the end of the year.
“On static and formal we have had five years of not having competitive products,” said David Hsu, “so why would customers trust us on our return to the market?”
Hsu said there were two reasons: the capability of the individual tools, and their integration within Verification Compiler.
The tools are built on a new generation of data models, databases and analysis engines which the company says gives them greater capacity and capability, and reduces violation “noise”.
Low-power checking
VC LP supports the verification of deigns whose power management architecture has been defined using the Unified Power Format (UPF). The user specifies how a design should be powered and how that power should by managed in UPF, and then VC LP checks the UPF definition before the synthesis step. Once Design Compiler and IC Compiler have implemented the necessary power and ground network, VC LP can then be used to check the implementation against the intent.
“Low power checking was the first consumer of all the underlying infrastructure,” said Hsu. “To get the capacity and performance necessary we had to rebuild that infrastructure,”
Formal
Hsu characterised formal verification as “a very large and interesting challenge.”
VC Formal offers property checking, sequential equivalence checking, connectivity checking and formal coverage analysis.
Hsu said that using formal checks was always a trade-off between the size of the target design, the complexity of the check you want to make, and how long you’ve got. He characterised VC Formal as a block-level solution, capable of handling designs of “millions of gates”, but also able to read in entire SoCs and subject them to simpler checks.
“We think connectivity checking, for example, is an ideal application of formal techniques,” he added. He said the approach would also work well for checking a design against a asset of communications protocols, for example.
Formal techniques rely on engineers who can specify the properties of their designs and write assertions about them. With VC Formal, Synoosts is trying to make this process more accessible
Hsu added that Synopsys wanted to make formal checking more accessible to engineers, and so enable them to check their designs more thoroughly.
“Because we have put his formal layer in [to Verification Compiler], customers will implement checks that no-one thought relevant until now.” This could eventually lead to the exchange of, or even a market in, assertion IP that represents complex checks for common issues.
Clock domain crossing
Synopsys says that VC CDC can check the way that clock signals cross power domains on entire SoCs at RTL.
Hsu argued that clock-domain crossing checks may be easier to handle that other classes of problem because it is well defined, but that tools have to have the capacity to handle large designs.
“For CDC, if you don’t load the whole design and check the whole chip, you’re going to miss things.”
Users can specify any type of CDC synchronizer structure and the tool will automatically recognise them in the netlist and cheek that they have been properly implemented.
