Jasper, Duolog bring formal verification to IP specification and assembly, low-power design
Prompted by ARM, Jasper Design Automation and Duolog Technologies have signed a deal to contribute methodologies and tools to a flow that will help designers deliver qualified, integration-ready IP and SoC assemblies verified using formal methods.
The idea of the formal verification flow is to check the initial specification of a block of IP, or the definition of how several blocks should be assembled, against the implementation. This process should also reveal any gaps in the specification.
Two flows have been defined: one for capturing and verifying register metadata, combining Duolog’s Socrates Bitwise register management tool with the JasperGold Control and Status Register verification tool. The flow will enable IP designers to verify both executable specifications and RTL for consistency and completeness.
The second flow uses Duolog’s Socrates Weaver SoC integration tool and the JasperGold Connectivity verification tool. This flow enables SoC design teams to assemble, construct and verify a complete SoC integration, including temporal and conditional connections, as well as multiplexed I/Os.
The flows use the IEEE1685 IP-XACT standard as their data exchange format. ARM uses this format to package its IP.
Oz Levia, vice president of marketing and business development at Jasper Design Automation, said: “The integrated design flow is very intuitive, from black-box system specifications, through design capture and integration, to verification.”
John Goodenough, vice president of design technology and automation, at ARM, said: “The integrated flows from [Jasper and Duolog] should both increase productivity and quality for us and for our customers.”
Jasper has also added a tool that provides a formal check on the impact of implementing low power strategies, such as the introduction of multiple power domains. This usually involves structural changes, such as the insertion of isolation buffers and retention cells, as well as functional changes, which impact the behaviour of the rest of the chip. The low power verification tool, one of Jasper’s series of formal methods based apps, checks issues such as whether the connectivity of the chip remains valid, and whether the design remains free of deadlocks.
The tool ingests the design RTL and the power intent expressed in a UPF file, and then creates an internal RTL model that includes the power management enhancements. This is then checked for structural integrity, as well as applying automatic functional assertions to check for issue such as whether the power sequencing works.
Although the internal RTL model that the tool develops for itself is not used in the rest of the design flow – other tools will insert the power mangement structures in the actual design RTL – Levias argues that most tools are now inferring power-management structures from the UPF file in much the same way, so the two versions of the power-managed design should be congruent.
