A Formal Tale, Chapter I: AMBA

Beware: This repository is still in beta version

A Formal Tale, Chapter I: AMBA

AMBA Formal Properties Repository

AXI4-Stream

AXI4 Stream

AXI4-Stream Examples

Motivation

The goal of this repository of AMBA properties for Formal Verification is to showcase how to get the most of both AMBA and Model Checking in design and verification of AMBA AXI IP in conjunction with these pillars:

Good organisation of the code.
Debuggability.
Documentation.
Optimised properties for model checking.
Be a reference for others to see the power of SVA, and that strong properties are not necessarily complex.

The following sections briefly describe these points.

Good organisation of the code

This implementation uses the SVA property ... endproperty constructs to define the rules that are to be proven, and a link to the specification where said behavior is mentioned, as shown in the excerpt below:

   /*            ><><><><><><><><><><><><><><><><><><><><             *
    *            Section III: Handshake Rules.                        *
    *            ><><><><><><><><><><><><><><><><><><><><             */
   /* ,         ,                                                     * 
    * |\\\\ ////| "Once TVALID is asserted it must remain asserted    * 
    * | \\\V/// |  until the handshake (TVALID) occurs".              * 
    * |  |~~~|  | Ref: 2.2.1. Handshake Protocol, p2-3.               * 
    * |  |===|  |                                                     * 
    * |  |A  |  |                                                     * 
    * |  | X |  |                                                     * 
    *  \ |  I| /                                                      * 
    *   \|===|/                                                       * 
    *    '---'                                                        */
   property tvalid_tready_handshake;
      @(posedge ACLK) disable iff (!ARESETn)
        TVALID && !TREADY |-> ##1 TVALID;
   endproperty // tvalid_tready_handshake

This increases readability and encapsulates common behaviors easily, so debugging can be less difficult.

Debuggability

A message accompanies the assertion in the action block, so when a failure is found by the new VIP, the user can quickly understand the root cause and fix the problem faster.

assert_SRC_TVALID_until_TREADY: assert property (tvalid_tready_handshake)
           else $error ("Protocol Violation: Once TVALID is asserted \ 
           it must remain asserted until the handshake occurs (2.2.1, p2-3).");

Documentation

There will be an user guide and a set of examples so the user can start real quick to get RoI of using formal for both RTL design bring-up and verification tasks. See, for example, this demonstration using the new VIP.

Optimised properties for model checking.

The aim is to reduce the size of the new verification IP in terms of variables, so it can be used in large designs. To achieve this, the properties should have only the required variables in the antecedent, and complex behaviors will use auxiliary logic instead of, for example, sequences or any other SVA structure that is not formal friendly.

Be used as reference for others to see the power of SVA

By correlating the specification with the property block, users can understand why the property was encoded in that way.

Upon failures, the user would be able to quickly understand the issues, since this repository is open source and does not follow the industrial solution where the IP uses antecedent and consequent of the propositions encrypted, adding unnecessary complexity to the debug.

GuillemCabo/A_Formal_Tale_Chapter_I_AMBA