unknown_ifb Imported from Blogger

Getting these to work sometimes feels like an exercise in self-torture. The most elegant constraints are rarely supported by either LRM or the tools. Even so, every time you do one of these, I always try to come up with my own solution.

I rarely (never? ) come up with something better, but I think this time I got an elegant one…

• We can represent required edges in a matrix m_edges[v1][v2], where m_edges[v1][v2] == 1 if there’s an edge between v1 and v2.

• We can represent the drawing path using r_vertex[EDGES] array, where pencil starts on r_vertex[0], moves to r_vertex[1], etc.

• Then, the constraint is to say that for each r_vertex[i], r_vertex[i-1] pair, we must have m_edges[r_vertex[i]][r_vertex[i-1]]==1.

• The only thing missing now is the uniqueness. This is where I use a 3-D matrix r_edges[v1][v2][i] to represent whether step ‘i’ has drawn edge v1-v2 or not. With that available, we can then say that for each m_edges[v1][v2] == 1, we must have a one-hot {r_edges[v1][v2], r_edges[v2][v1]} (accounting for either direction).

Code: (it’s hard to read, blogger doesn’t allow code or pre tags in comments)

class drawer#(VERTICES=5,EDGES=8);

bit[VERTICES-1:0][VERTICES-1:0] m_edges;
rand byte unsigned r_vertex[EDGES:0];
rand bit[VERTICES-1:0][VERTICES-1:0][EDGES:0] r_edges;

constraint c_edges {
foreach(r_edges[v1, v2, i]) {
r_vertex[i] < VERTICES;
(i > 0) && (r_vertex[i] == v2) && (r_vertex[i-1] == v1) →
r_edges[v1][v2][i-1] == 1 &&
m_edges[v1][v2] | m_edges[v2][v1] == 1;

m_edges[v1][v2] → $onehot({r_edges[v1][v2], r_edges[v2][v1]});
}
}
endclass

This works with VCS and Questa. VCS is a bit slow at it… It speeds up quite a bit if we explicitly set r_edges to 0 when they are not drawn on, but I was going for the least amount of constraint code :).

I think Incisive still doesn't support $onehot in a constraint, but one could write a function to replace it.

TudorTimi Verification Gentleman

Self-torture is probably a bit strong for it, but patience for sure. I wanted to dabble with using an adjacency matrix too for the solution, but I didn’t want to go too deep into graph theory. Your solution is anyway pretty cool. It’s interesting to see that one little extra constraint can speed up some solvers.

Regarding $onehot, I had the exact same problem for N-Queens. I’d avoid it since as you say it’s not supported by all sims, but a viable replacement is sum(). A handwritten function would create a unidirectional constraint and that would change the solution space. To use sum(), though we need to work with arrays of bits instead of vectors.

1 reply

unknown_ifb Imported from Blogger

I have originally tried to use a 3-D array with .sum(), but managed to crash 2 of 3 simulators, with third complaining that it didn’t support it yet. (That’s probably where my self-torture comment came from ). So, that sent me the way of the 3-D vector instead.

Using a onehot() custom function would indeed change the solve order, but since it’s essentially being used to “check” the answer at the end, it would still produce the correct answer here.