TIC TAC TOE Snapshot generation using SystemVerilog constraints

I think there are more states to consider, and the sum need not be 5. We want to model a tic-tac-toe snapshot… there are many possibilities.
Game stops when a player wins, thus we need to model empty slots as well.

A better way to represent the problem is to consider -1 and 1 to be X and O and 0’s as empty space.
Each player takes a chance, so the number of -1/1 will always be within one difference, and thus for a valid play the sum of the board will always be within -1,0,1;

Below set of constraints are quite comprehensive but I feel it covers the ground, please let me know in case you find a bug…


rand int a[3][3];

//constraint for valid values
constraint c_valid_values { foreach( a[i,j] ) a[i][j] inside {-1,0,1}; }

//constraint for valid game 
// if -1 wins the sum will always be -1 or 0
// if 1 wins the sum will always be   1 or 0;
// draw will have a sum of 1 or -1
constraint c_valid_play { a[0].sum() + a[1].sum() + a[2].sum() >= -1; 
                          a[0].sum() + a[1].sum() + a[2].sum() <=  1; }

//constraints to choose a winner. 
// a wins if a row/column/diagonal has a sum of 3 and b does not have that combination
// b wins if b row/column/diagonal has a sum of 3 and a does not have that combination
// draw is when every chance has been played and there are no 0s on the board ( which will come out of above constraints anyway)

//I wish we had an abs function :)
//we always gurantee fair play for each player, a winner might have one chance more than the loser. i.e. number of -1s and 1s will always be "one" count far from each other.

//any row hit, other rows should not be
constraint c_valid_row {
  foreach ( a[i] ) {
    foreach ( a[j] ) {
      if( i!= j ) ( a[i].sum inside {3,-3} ) -> ( !a[i].sum inside {3,-3} );
    }
  }
}

//any column hit, other columns should not be 
constraint c_valid_column {
  if ( (a[0][0] + a[1][0] + a[2][0]) inside {3,-3} ) {
    !( (a[0][1] + a[1][1] + a[2][1]) inside {3,-3} ); 
    !( (a[0][2] + a[1][2] + a[2][2]) inside {3,-3} );
  }
  //similar for other two columns
  if ( (a[0][1] + a[1][1] + a[2][1]) inside {3,-3} ) {
    !( (a[0][0] + a[1][0] + a[2][0]) inside {3,-3} ); 
    !( (a[0][2] + a[1][2] + a[2][2]) inside {3,-3} );
  }
  if ( (a[0][2] + a[1][2] + a[2][2]) inside {3,-3} ) {
    !( (a[0][0] + a[1][0] + a[2][0]) inside {3,-3} ); 
    !( (a[0][1] + a[1][1] + a[2][1]) inside {3,-3} );
  }
}

//if any cross is hit, then no other combo should be valid.
constraint c_valid_cross {
  if( (a[0][0] + a[1][1] + a[2][2]) inside {3,-3} ) {
    foreach ( a[i] ) !(a[i].sum() inside {3,-3}); 
    !( (a[0][0] + a[1][0] + a[2][0]) inside {3,-3} ); 
    !( (a[0][1] + a[1][1] + a[2][1]) inside {3,-3} ); 
    !( (a[0][2] + a[1][2] + a[2][2]) inside {3,-3} ); 
    !( (a[0][2] + a[1][1] + a[2][0]) inside {3,-3} ); //other cross 
  }
  if( (a[0][2] + a[1][1] + a[2][0]) inside {3,-3} ) {
    foreach ( a[i] ) !(a[i].sum() inside {3,-3}); 
    !( (a[0][0] + a[1][0] + a[2][0]) inside {3,-3} ); 
    !( (a[0][1] + a[1][1] + a[2][1]) inside {3,-3} ); 
    !( (a[0][2] + a[1][2] + a[2][2]) inside {3,-3} ); 
    !( (a[0][0] + a[1][1] + a[2][2]) inside {3,-3} ); //other cross 
  }
}

-Order from chaos!!
ps: please excuse any syntactical errors.