Intelligent Proof Kits and VIPs

Faster, Accurate Verification of SoC Interface Protocols

FEATURES AND BENEFITS
  • Quickly and exhaustively certify standard protocols, including AMBA, AXI, memory controllers
  • Enable automated, encapsulated, plug-and-play capabilities for fast adoption
  • Provide quality support for spec-compliant designs
  • Allow user configurability for variants on standard protocols
  • Visualize properties and analyze timing diagrams to understand property behavior with the JasperGold RTL Development App and JasperGold Formal Property Verification App
  • Prove selected protocol properties with JasperGold Formal Property Verification App

Verification of standard protocols such as AMBA, AXI, PCI-Express, etc. and memory controllers in today’s complex SoC designs is challenging and time-consuming, for compliance with the protocol specifications. This in turn increases dependency of verification engineers on the design team.

SoC teams spend weeks, if not months, to verify standard interface protocols such as AMBA, PCI-Express. Bugs still surface due to either ambiguity in the protocol specification document or inability to exhaustively simulate all possible scenarios. In addition, expertise or understanding of protocols maybe required. It is also difficult to model protocol behavior early in the design cycle, and there is no way to create and manipulate waveforms directly from the spec.

The Jasper Intelligent Proof Kits and Verification IP solutions enable SoC design teams to accelerate verification by quickly and exhaustively certifying standard protocols such as the latest AMBA 4 (AXI 4, ACE, API, APB) PCIe, DDR, LPDDR, OCP, etc.  The Jasper generated protocol related properties allow early exploration and verification of protocol specification and are optimized for formal.  They also plug seamlessly into the simulation environment.

The solutions can be used seamlessly with the JasperGold Formal Property Verification App to formally prove the embedded properties, thereby exhaustively verifying that the design meets the protocol specification. Intelligent Proof Kits eliminate the need to manually write properties, which require in-depth understanding of the protocol specification.

 

IPK screenshot

Jasper's IPKs can be seamlessly used with the JasperGold Formal Property Verification App.

 

Available IPKS
  • AMBA AHB
  • DDR
  • DFI
  • AMBA AHB-Lite
  • DDR2
  • OCP
  • AMBA APB
  • DDR3
  • ETHERNET
  • AMBA AXI3
  • LPDDR
  •  ...
  • AMBA AXI4
  • LPDDR2
 
  • AMBA AXI4-Lite
  • LPDDR3
 
  • AMBA AXI4-Stream
  •  SDRAM
 
  • AMBA AXI ACE
 

Contact Jasper for other

IPKs not listed

info@jasper-da.com

 

 

As shown in the flow, Intelligent Proof Kits are available as part of the JasperGold technology platform. With both the JasperGold RTL Development App and the JasperGold Formal Property Verification App, the user can visualize protocol transactions and timing diagrams to understand behaviors of properties, and design specifications via Jasper’s patented Visualize™ technology. Intelligent Proof Kits automatically generate wrapper and Tcl files, which contain the unencrypted and customizable Proof Kit source code as well as setup commands to prove the properties formally in the JasperGold Formal Property Verification App.Intelligent Proof Kits Flow

Intelligent Proof Kit Flow
Once these selected properties are visualized, they can be imported into JasperGold Apps via the auto-generated wrapper and Tcl files. The JasperGold Formal Property Verification App enables fast and exhaustive certification of standard and memory controller protocols using Jasper’s multiple formal proof engines. These properties are also simulation-friendly and can be leveraged in any simulation environment.

Protocol Certification Made Easy

SoC teams spend weeks, if not months, to verify standard interface protocols. Bugs still surface due to either ambiguity in the protocol specification document or inability to exhaustively simulate all possible scenarios.

Jasper Intelligent Proof Kits ensure verification quality and completeness, and increase confidence that the design is compliant with the protocol specification. They help find critical bugs early on and shorten the overall verification schedule.