Constraint to make sure a matrix inverse exists

SystemVerilog
, ,
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