AXI VALID signals deasserted during reset

The first assertion checks that AXI ARVALID signal is not asserted during reset. This can be coded either as a combinational property or as an implication. There are two ways to paraphrase this rule:

• Combinational: never allow ARVALID==1 & ARESETn==0
• Implication: ARESETn==0 implies ARVALID==0

The assertion is coded using the implication method since the cause and effect are more clearly identified. The example below shows how to use Zazz to create the assertion to check all five valid signals:

ARESETn ==0 implies (ARVALID==0 && AWVALID==0 && WVALID==0 && RVALID==0 && BVALID==0)