Calling function in consequent of SVA

SystemVerilog
,
1

Hi,

  1. Can we call “get_ AlignMaskR” as shown in below code.
  2. Do the following function will be called on every posedge of clock cycle. even though it is in consequent
function automatic bit [6:0] get_ AlignMaskR()

   case (ARSIZE)
        `AXI4PC_ASIZE_1024:  get_AlignMaskR = 7'b0000000;
        `AXI4PC_ASIZE_512:   get_AlignMaskR = 7'b1000000;
        `AXI4PC_ASIZE_256:   get_AlignMaskR = 7'b1100000;
        `AXI4PC_ASIZE_128:   get_AlignMaskR = 7'b1110000;
        `AXI4PC_ASIZE_64:    get_AlignMaskR = 7'b1111000;
        `AXI4PC_ASIZE_32:    get_AlignMaskR = 7'b1111100;
        `AXI4PC_ASIZE_16:    get_AlignMaskR = 7'b1111110;
        `AXI4PC_ASIZE_8:     get_AlignMaskR = 7'b1111111;
        default:             get_AlignMaskR = 7'b1111111;
      endcase

endfunction 

property AXI_ERRM_ARADDR_WRAP_ALIGN;
    @(posedge ACLK)
            disable iff(assert_en[56] == 0)
         ( !($isunknown({ARVALID,ARBURST,ARADDR})) &
          ARVALID & (ARBURST == `AXI4PC_ABURST_WRAP) ) 
      |-> ((ARADDR[6:0] & get_ AlignMaskR()) == ARADDR[6:0]);
  endproperty
  axi_errm_araddr_wrap_align: assert property (AXI_ERRM_ARADDR_WRAP_ALIGN) else
  `uvm_error("AXI4_assertions", $psprintf("AXI_ERRM_ARADDR_WRAP_ALIGN. A read transaction with burst type WRAP must have an aligned address. Spec: section 4.4.3 on page 4-6."))
2

In reply to uvm_novice:


The property uses the overlapping operator |->.  At every posedge clk , the condition(( !($isunknown({ARVALID,ARBURST,ARADDR})) & ARVALID & (ARBURST == `AXI4PC_ABURST_WRAP) )) is true. the property will evaluate the consequent.
3

If the antecedent fails, Then also function will be called ?

4

In reply to uvm_novice:

antecedent fails means its vacuous pass. In this case consequent will not be executed.
basically, the property will stop at the antecedent only.

5

In reply to uvm_novice:

  1. Yes, you can use function in Assertion and your code should work
  2. this function will only be called when antecedent is TRUE.