Foreach loop in aux code for FPV

SystemVerilog
1

Hi!

I am learning how to do formal verification with SVA and I wanted to have a foreach loop to search through a multidimensional array, I cannot figure out if this is possible to do. Can anyone point out to examples of this? Or if it’s not possible, how could I do it?

Thank you in advance!

2

However, inside an assertion, a foreach loop is not directly supported. Instead, you can create a property that checks a condition over multiple indices.

Here’s a complete SystemVerilog testbench with an assertion that iterates over a multidimensional array using a external function. It will check if any value in the array is 8'hFF and trigger an assertion if found.

module tb;
    logic clk;
    bit [7:0] my_array [4][4]; // 4x4 array of 8-bit values

    // Clock generation
    always #5 clk = ~clk;

    // Function to check if any value in the array is 8'hFF
    function automatic bit check_array();
        foreach (my_array[i, j]) begin
            if (my_array[i][j] == 8'hFF)
                return 1; // Found a match
        end
        return 0; // No match found
    endfunction

    // Signal to hold function result
    logic found_ff;

    // Evaluate function on clock edge
    always @(posedge clk) found_ff <= check_array();

    // Assertion to check for 8'hFF in the array
    property check_array_property;
        @(posedge clk) found_ff |-> ##1 1'b1;
    endproperty

    // Assertion instance
    assert property (check_array_property)
        $display("ASSERTION PASSED: Found 0xFF in the array!");
    else
        $display("ASSERTION FAILED: No 0xFF found!");

    initial begin
        clk = 0;
        
        // Initialize array with random values
        foreach (my_array[i, j]) begin
            my_array[i][j] = $random;
        end

        // Introduce 8'hFF at a random location
        my_array[2][3] = 8'hFF; 

        #50;
        $finish;
    end
endmodule
1 Like