Formal verification using ARV-FORMAL
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
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 .
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.
So for formally verifying an IP we need to know two things
Example showing Negative testing of register using Assertion Property
Assertion Property generated by IDesignSpec
Types of Assertions Properties Supported
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.
a. Whether field is getting value form HW Interface.
a. Whether HW interface read the correct field value.
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.
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
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