+1 855-VERIFYY
+

Newsletter:Formal verification using ARV-FORMAL

Formal verification using ARV-FORMAL

INTRODUCTION

Formal verification avoids the slowness of event-simulation by using mathematical algorithms and heuristics to prove the functional correctness of a design. Popular specification standards such as IP-XACT , SystemRDL, CSV’s have been used as a starting point for automatically generating any Register Models, RTL, Firmware , and Verification Code . The whole verification process can be further upgraded by automating code for formally verifying IP’s with slave interface , since it helps in reducing simulation efforts and the overhead involved in creating and maintaining block/chip level test-benches. By using directed and constrained random test-cases we may miss out corner cases, which can only be verified formally.

Difference between Simulations based verification and Formal Verification

  • Simulation looks at individual points in the space of possible tests, while Formal verification covers that whole space at once.
  • The simulation-based methodology is input driven while the formal methodology is output driven.

 

Formal Verification in IDesignSpec

In IDesignSpec formal verification can be done by extracting a list of properties from specification, each property describes a feature or a property. These properties are further used in formal tools to verify whether they are compliant with the RTL or not.
From the specification point of view we have an address space having registers at known addresses and bus interface used in communicating with those registers .

11

 

These registers can be formally verified with the bus interface only if the register where the response to bus transaction is taking place at valid address. Assertions properties are also written, for empty address spaces and invalid addresses checking through ARV-Formal.

12

So for formally verifying an IP we need to know two things

  1. Bus (Protocol)
  2. Register /Field ( where there is response to the bus transaction)
  • hdl_path is used to specify the name of register or field where there is response to the bus transaction.
  • while the bus information is specified in the settings of the Configure Window.

 

Supported Buses:-

  1. AMBA-AHB
  2. AMBA AHB3 LITE
  3. AMBA-APB
  4. AMBA-AXI

 

Example showing Negative testing of register using Assertion Property

13

 

Assertion Property generated by IDesignSpec

14

 

Types of Assertions Properties Supported

  1. For a field which is SW readable

a. Whether the data read from the bus is actually being read from the selected field.
b. If the field is readable only, whether writing to it yields an error response.

  1. For a field which is HW Writable

a. Whether field is getting value form HW Interface.

  1. For a field which is HW Readable

a. Whether HW interface read the correct field value.

  1. For a field which is SW writable

a. Whether the data written from bus is actually being written to selected field.
b. If the field is writable only, whether reading from it yields an error response.

  1. For a block

a. Assertions are written, for empty address spaces and invalid addresses.
b. During reset, if reset value matches the value specified in specification.
c. Assertions for special register/ fields like lock, alias, shadow

 

Supported Formal Tool

  1. OneSpin360
  2. Mentor’s Questa Formal

Summary

Formal verification avoids the slowness of event-simulation by using mathematical algorithms and heuristics to prove the functional correctness of a design. Formal verification systems can also trace back a cone of influence from a safety critical signal or expression in order to prune the code of logic and reduce analysis time. IDesignSpec provides the better solution to it by automatically generating the Assertion checking Properties to reduce the time to market.

By: Rohit & Mahima