Oski Formal Verification IP Library for ARM© AMBA© Standard Protocols

Oski’s library of verification IP components enable formal sign-off of compliance to ARM protocols in SoC designs. Oski VIPs are carefully designed to have minimal state space in order to maximize the efficiency of formal tools. They are compatible with a variety of formal, simulation and emulation tools. This makes the library components usable throughout the design cycle and portable across tool vendor flows.

VIP Diagram

Key Benefits

  • Protocol Compliance Testing
    • Enables exhaustive formal analysis
  • Silicon Proven
    • Used by Oski for formal verification sign-off
  • Formal Friendly
    • Minimal state space overhead
  • Portable
    • Tool vendor independent
    • Usable throughout the design flow
  • Comprehensive Checking
    • Interface protocol checks
    • System level checks
    • Configuration checks

Library Components

  • ARM AMBA 5
    • CHI
      • Interface VIP
      • Coherence VIP
    • AHB
  • ARM AMBA 4
    • ACE
      • Interface VIP
      • Coherence VIP
    • AXI
  • ARM AMBA 3
    • AHB-Lite
  • ARM AMBA 2
    • AHB


  • RTL Formal Sign-off of Protocol Compliance
    • Master and slave interface controllers
    • Bridges
    • Interconnect fabrics
  • Architectural Formal Verification
    • Verify system cache coherence
  • Assertion Monitor
    • Simulation
    • Emulation

Contact Oski to obtain more information or to request a datasheet.