Beware: This repository is still in beta version
- Example 01: Source to sink (self check)
- Example 02: Verify another VIP (faxis_slave)
- Example 03: AXI4-Stream FIFO from Alex Forencich's
- Example 04: AXI4-Stream Mat - mul from rahulsridhar5/PLCgroup10
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.
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_handshakeThis increases readability and encapsulates common behaviors easily, so debugging can be less difficult.
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).");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.
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.
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.