anonymous_ifb Imported from Blogger

Very prettily done - thanks.

I’ve used $onehot constraints but I’m not 100% sure that all the main tools support that.

Did you, at any point in your experiments, try using an auxiliary variable (one for each column, and possibly another for each row) that contains the location of the queen? That might make some of the constraints easier to write, but perhaps would give the solver a harder time.

When doing “interesting” things with SV constraints - whether for intellectual pastime like this, or for the day job - I’ve often found myself hitting incomprehensible performance problems, simply because I have no idea how the tools’ solvers are doing their job. Each tool seems to have its own “no go areas”, constraint idioms that cause solver performance to drop horribly - but it’s really hard to get any kind of grip on why that happens, and what you can do to avoid it. That’s a slightly simpler problem for Specman users because they have only one implementation to worry about (two, I suppose, if you count both Intelligen and pgen?) and the Specman documentation says quite a lot about how things work behind the curtain. Constraint solver performance in SV, and how to avoid hobbling it, would be a good topic for a future post or series of posts, if anyone has any expertise in that area.

1 reply

anonymous_ifb Imported from Blogger

That’s a pity. Only 1 of 3 simulators I tried supports $onehot in constraints. Using an auxiliary “which bit should be set” variable works fine, and does not seem to cause any trouble when combined with other constraints on the vector:

rand bit [N-1:0] v;
rand int position;
constraint v_onequeen {
position inside {[0:N-1]};
v == (1 << position);
}

TudorTimi Verification Gentleman

I didn’t want to use the method you describe (with the auxiliary variable per row/column) because that’s how Vitaly did it in his Specman post and I didn’t want my post to just be a simple translation from e to SV. I also wanted to experiment with the array reduction method in constraints (as that’s something new in the 2012 standard).

With respect to solver performance, I’ve tried it out in 2 simulators and I have noticed considerably worse performance on one vs. the other. It’s as you say, pretty much impossible to know why. I usually try to stay away from such topics as simulator performance as I don’t want to get slapped with a lawsuit. Even ignoring that, I would have no idea where to start, since what applies to one simulator won’t apply to another.

unknown_ifb Imported from Blogger

class n_queen_puzzle#(int n=8);
rand bit board[n][n];
rand bit board_tx[n][n];

constraint unique_row_c {
foreach(board[i,])
board[i].sum() with (int’(item)) == 1;
}

constraint board_tx_c {
foreach (board[i,j])
board_tx[j][i] == board[i][j];

solve board before board\_tx;  

}

constraint unique_col_c {
foreach(board_tx[i,])
board_tx[i].sum() with (int’(item)) == 1;

}

constraint board_c2 {
foreach(board[i, j]) {
if(board[i][j]) {
foreach(board[k, l]) {
if(i != k && k+l == i+j) board[k][l] != 1;
if(i != k && l-k == j-i) board[k][l] != 1;
}
}
}
}
endclass

anirban_ifb Imported from Blogger

class array;
rand bit a[8][8];
constraint c_c{
foreach(a[i,])
{
a.sum() with ( item.index(1) == i ? 4’(item) : 0) == 1;
a.sum() with ( item.index(2) == i ? 4’(item) : 0) == 1;
a.sum() with ( item.index(1) - item.index(2) == -i ? int’(item) : 0) <= 1;
a.sum() with ( item.index(1) - item.index(2) == i ? int’(item) : 0) <= 1;
a.sum() with ( item.index(1) + item.index(2) == i ? int’(item) : 0) <= 1;
a.sum() with ( item.index(1) + item.index(2) == i*2 ? int’(item) : 0) <= 1;
}
}

function display();
foreach(a[i]) begin
foreach(a[,j])
$write("%3d",a[i][j]);
$display;
end
endfunction
endclass