8x8 matrix constraint

I am trying to write a constraint on a 8x8 matrix, such that all 3x3 matrix with the 8x8 matrix will not have all “FALSE”.

Example:
The following should not be present in the 8x8 matrix,(F-False)
FFF-----
FFF-----
FFF-----





or
-FFF----
-FFF----
-FFF----





Good:
-FF-----
-FFF----
-FFF----






class mat;

typedef enum{YES,NO,TRUE,FALSE} mat_t;

rand mat_t matrix[8][8];

// I need to find all the 36 3x3 matrices inside the 8x8 matrix and constraint them to be not all FALSE
rand mat_t matrix3x3[6][6][3][3];

// How do you guys approach such problem?
// I am finding hard to get the indices to get the small 3x3 matrices from the 8x8 matrix, any document/link/boo which explains this might help!



In reply to n347:

See Constraint in a 2d pixel matrix | Verification Academy

In reply to dave_59:

Thanks Dave! that looks similar but this is slightly different.

I need to be sure that atleast one neighboring pixel of FALSE has to be different than FALSE.


class mat;
 
typedef enum{YES,NO,TRUE,FALSE} mat_t;
 
rand mat_t matrix[8][8];
 
// I need to find all the 36 3x3 matrices inside the 8x8 matrix and constraint them to be not all FALSE
rand mat_t matrix3x3[6][6][3][3];
 
// BAsically i want to ensure atleast one neighboring pixel is not FALSE, i didnt have the boundary conditions taken care of .... 
// Its getting very complicated, I there any better solution? 
constraint mat_c{
 foreach(matrix[i,j]){
        if(matrix[i][j] == FALSE) -> !((matrix[i-1][j-1] == FALSE) && (matrix[i-1][j] == FALSE) && (matrix[i-1][j+1] == FALSE) && (matrix[i][j-1] == FALSE) && (matrix[i][j+1] == FALSE) &&(matrix[i+1][j-1] == FALSE) && (matrix[i+1][j] == FALSE) &&(matrix[i+1][j+1] == FALSE))
}
}

In reply to n347:

I don’t think there is any better way of doing this. You cannot use procedural for loops to do more complex iterations. The boundary conditions are easy.

constraint mat_c{
 foreach(matrix[i,j])
        i inside {[1:6}} && j inside {[1:6]} -> 
     matrix[i-1][j-1] != FALSE || matrix[i-1][j] != FALSE || matrix[i-1][j+1] != FALSE || 
     matrix[i]  [j-1] != FALSE || matrix[i]  [j] != FALSE || matrix[i]  [j+1] != FALSE ||
     matrix[i+1][j-1] != FALSE || matrix[i+1][j] != FALSE || matrix[i+1][j+1] != FALSE ;
}

In reply to dave_59:

Dave, Thank you.

You cannot use procedural for loops to do more complex iterations. → what does this mean?

Any ideas from others if i can somehow get the individual 3x3 matices, how do i constraint the 3x3 matrices to not have all FALSE and also affect the bigger 8x8 matrix?

// I need to find all the 36 3x3 matrices inside the 8x8 matrix and constraint them to be not all FALSE
rand mat_t matrix3x3[6][6][3][3];

In reply to n347:

I meant I had to write out the 9 terms in one single equation, I couldn’t use a for loop to gather the terms. That would be more useful if the matrix sizes were parametrizable. Probably could get the array op() reduction operator to do this, but I don’t have the time or energy to do that.
The 36 3X3 matrixes would be easier to write the constraints

constraint mat_c{
 foreach(matrix3x3[g,h])
      maxtrix3x3[g][h].or(iD) with (iD.or(jD) with (jD != FALSE));
}

But tying that to the 8x8 would be more difficult and too many constraints.

In reply to n347:

I meant I had to write out the 9 terms in one single equation, I couldn’t use a for loop to gather the terms. That would be more useful if the matrix sizes were parametrizable. Probably could get the array op() reduction operator to do this, but I don’t have the time or energy to do that.
The 36 3X3 matrixes would be easier to write the constraints

constraint mat_c{
 foreach(matrix3x3[g,h])
      maxtrix3x3[g][h].or(iD) with (iD.or(jD) with (jD != FALSE));
}

But tying that to the 8x8 would be more difficult and too many constraints.

In reply to dave_59:

Thanks Dave!