Constraint to make sure a matrix inverse exists

SystemVerilog
, ,
1

Hi,

I was wondering if there is a easier way to randomize a 2-D array (matrix) so that the inverse exists?
For a matrix to have a valid inverse:

  1. It should be a square matrix.
  2. A x A^-1 = I where A is our matrix, I is a identity matrix (1 along the diagonal, every other element is 0).

Any help is appreciated!

1 Like
2

In reply to DK87:

You can try this (and please check my dot-product math)

module top;
  class matrix;
    rand bit signed [3:0]  A[][], AI[][];
    
    constraint c_size { A.size inside {[2:4]}; A.size == AI.size; }
    constraint c_square { foreach (A[D1]) {A.size == A[D1].size;
                                           A.size == AI[D1].size; } 
                        }
    constraint c_inverse { foreach ( A[D1,D2] )
      A[D1].sum() with (int'(A[item.index][D1] * AI[D2][item.index])) == (D1 == D2); }
  endclass
      
  matrix m = new;
  initial begin
    assert(m.randomize());
    foreach (m.A[i,j]) begin
      if (j==0) $display;
      $write(m.A[i][j],,);
    end
    $write("\n-------");
    foreach (m.AI[i,j]) begin
      if (j==0) $display;
       $write(m.AI[i][j],,);
    end
    $display;
  end
      
endmodule : top

Do realize these constraints explode as you increase the number of bits and the size of the array. A 4X4X4 array is randomizing a 128 bit variable with constraints between every combination of bits.

1 Like
3

In reply to dave_59:

Thank you Dave. I might have to end up doing matrices upto 12x12 which can cause quite a overhead. I’m thinking of just randomizing it (without a constraint) and doing a check in post randomize to make sure if it’s inverse exists (redo it in case inverse doesn’t exist) in case the constraint solver takes too long.

If you have any suggestions on a implementation, what would be great!

Thanks again!

4

In reply to dave_59:
can you please explain c_square and c_inverse constraints?

5

In reply to DK87:

The approach of trying completely random values and then seeing if they match the constraints might take just as long or longer. You may want to try looking for a program designed specifically for creating inverse matrices and import the results.

In reply to juhi_p:

SystemVerilog has arrays of arrays, not really 2-dimensional arrays. The means that each element of the first dimension could have a different second dimension size. The C_square constraint makes sure that each element of the first dimension has an array whose dimension is the same size as the first dimension (i.e number of rows and columns are equal) to make it a square array

The C_inverse constraint is computing the dot product for each row(i)/column(j) and comparing to 0 or 1. The identity matrix is where the only row/column combination elements are true is when row(i) == column(j).

6

In reply to dave_59:

Hi Dave,



lets say for the following 2 matrices shown below:

A = |1  2|   AI = |5 6|
    |3  4|        |7 8|

Now the resultant dot product matrix would be:
Result = |(1*5+2*7)  (1*6+2*8)|
         |(3*5+4*7)  (3*6+4*8)|

You've shown in your code the following constraint: 
constraint c_inverse { foreach ( A[D1,D2] )
      A[D1].sum() with (int'(A[item.index][D1] * AI[D2][item.index])) == (D1 == D2); }

Can you explain how is this [item.index][D1]*[D2][item.index] mapping to the above product dot sum?

Thanks

7

In reply to nnd:
First unroll the foreach

A[0].sum() with (int'(A[item.index][0] * AI[0][item.index])) == (0 == 0)
A[0].sum() with (int'(A[item.index][0] * AI[1][item.index])) == (0 == 1)
A[1].sum() with (int'(A[item.index][1] * AI[0][item.index])) == (1 == 0)
A[1].sum() with (int'(A[item.index][1] * AI[1][item.index])) == (1 == 1)

Then expand the sum

( A[0][0] * AI[0][0] + A[1][0] * AI[0][1] ) == 1 // 1 * 5 + 2 * 7
( A[0][0] * AI[1][0] + A[1][0] * AI[1][1] ) == 0 // 1 * 6 + 2 * 8
( A[0][1] * AI[0][0] + A[1][1] * AI[0][1] ) == 0 // 3 * 5 + 4 * 7
( A[0][1] * AI[1][0] + A[1][1] * AI[1][1] ) == 1 // 3 * 6 + 4 * 8

This assumes D1 is the column and D2 is the row of your matrices.

8

In reply to dave_59:

Thanks!!