3.3. Property type

Table 3.3 lists the available settings for the PropertyType parameter in each OVL instantiation for specific groups of assertions. You can use them to control how these groups of assertions are used during formal verification.

For example, if you are formally verifying compliance of a master interface then you want to prove all of the master rules, ERRM and RECM, but assume that all slave rules, ERRS and RECS, are true. To do this, you leave the master rules set as 0, the default in Table 3.3, but change the slave rules to 1. This means that you test the master in an environment where the slave is compliant. This is only performed as part of formal verification.

Table 3.3. Property type parameters

NameDescriptionDefault
AXI_ERRL_PropertyTypeDevice Under Test (DUT) low-power interface compliance with the rules.0
AXI_ERRM_PropertyTypeDUT master interface compliance with the rules.0
AXI_RECM_PropertyTypeDUT master interface compliance with the recommendations.0
AXI_AUXM_PropertyTypeDUT master interface compliance with the internal auxiliary logic.0
AXI_ERRS_PropertyTypeDUT slave interface compliance with the rules.0
AXI_RECS_PropertyTypeDUT slave interface compliance with the recommendations.0
AXI_AUXS_PropertyTypeDUT slave interface compliance with the internal auxiliary logic.0

You can set the OVL PropertyType parameter to the following values:

0

Assert, this is the default.

1

Assume.

2

Ignore.

3

Assert 2-state.

4

Assume 2-state.

Copyright © 2005, 2006, 2009 ARM. All rights reserved.ARM DUI 0305C
Non-Confidential