Randomization result with and without (solve x before y)

SystemVerilog
,
1

Hi Experts,

The below constraint in a packet determines the data length of the packet based on packet kind.
eg: If packet kind is LONG then data length is greater that 10 bytes.

typedef enum int {SHORT, MED, LONG} kind_e;
rand kind_e kind;
rand int unsigned len;
rand bit [3:0] data[];
 
constraint pkt_constraint1 {
    (kind==SHORT)-> (len <5);
    (kind==MED)  -> (len inside {[5:9]});
    (kind==LONG) -> (len >= 10);   
}

LRM says that the constraints are resolved parallel and (solve x before y) does not change the solution set.
Then what will be the impact of (solve kind before len) in the constraint block “pkt_constraint2” ?
Will pkt_constraint1 and pkt_constraint2 create the same set of values on randomization ?

constraint pkt_constraint2 {
    (kind==SHORT)-> (len <5);
    (kind==MED)  -> (len inside {[5:9]});
    (kind==LONG) -> (len >= 10);
    solve kind before len;       
}

Thanks in advance

2

The way it should work is as follows:


constraint pkt_constraint1 {
    (kind==SHORT)-> (len <5);
    (kind==MED)  -> (len inside {[5:9]});
    (kind==LONG) -> (len >= 10);

The solution space is then // let S==SHORT, M == MED, L==LONG
{S,0}, {S, 1}, … {S,4} // 5 elements
{M,5}, {M, 6}, … {M, 9} // 5 elements
{L, 10}, {L, 11}, … {L, 2^31-1} // LOTS AND LOTS of elements
The solver will then randomly pick one of the sets from this set. In other words,
the probability of getting the LONG is very very high, compared to the SHORT or MED.
However, with


constraint pkt_constraint2 {
    (kind==SHORT)-> (len <5);
    (kind==MED)  -> (len inside {[5:9]});
    (kind==LONG) -> (len >= 10);
    solve kind before len;       
}

The probability of SHORT is 1/3, MED is 1/3, and LONG is 1/3.
Thus, you DO need the solve kind before len.

HOWEVER, and this is where it can get tricky, due to performance considerations, many solvers are not strictly LRM-compliant with regard to the distribution of results. The effect is that the solver will “approximate” the probability of the solution distribution for unordered variables (i.e. variables that do not participate in an explicit solve/before). That is why without the solve/before constraint it would work sort of like the solve before. You’ll need to experiment as to the statistics you would get.
However, solvers will provide LRM-compliant distribution for variables that are explicitly ordered (via solve/before constraints). Tools do provide strict LRM-compliance for the solver, even for unordered variables, by adding an option to the simulation command line (although this may reduce the performance/capacity of the solver for complex testcases).

SystemVerilog is indeed interesting! My advice for this problem, add the solve before.

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us

  • SystemVerilog Assertions Handbook 3rd Edition, 2013 ISBN 878-0-9705394-3-6
  • A Pragmatic Approach to VMM Adoption 2006 ISBN 0-9705394-9-5
  • Using PSL/SUGAR for Formal and Dynamic Verification 2nd Edition, 2004, ISBN 0-9705394-6-0
  • Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn 0-9705394-2-8
  • Component Design by Example ", 2001 ISBN 0-9705394-0-1
  • VHDL Coding Styles and Methodologies, 2nd Edition, 1999 ISBN 0-7923-8474-1
  • VHDL Answers to Frequently Asked Questions, 2nd Edition ISBN 0-7923-8115
2 Likes
3

In reply to ben@SystemVerilog.us:

Thanks Ben.

4

You are correct in quoting the fact that the solve x before y constraint has no effect on the set of available solutions, it only affects the distribution of values chosen. The way the constraint solver effectively works is that is constructs the entire set of solutions involving all variables first, then randomly picks one of those solutions, with each solution having uniform probability of being picked.

Using pkt_constraint1 as an example, there are the following solution sets

SHORT, 0
SHORT, 1
SHORT, 2
SHORT, 3
SHORT, 4
MED, 5
MED, 6
MED, 7
MED, 8
MED, 9
LONG,10
LONG,11
…
LONG,4294967294
LONG,4294967295

So there are 4294967295 possible solutions, but only 5 of them have kind==SHORT and 5 have lind=MED. So the probability of picking a value for kind other than LONG is 10/4294967295 , a very slim chance.

What solve kind before len pkt_constraint2 does do is instead of picking one of the 4294967295 solutions randomly, it will pick a value for kind uniformly out of the 3 possible values from the solution set, and then pick a value for len uniformly from the remaining valid values. So the probability of picking (SHORT, 0) is now 1/(3*5) = 1/15.
This constraint should really be thought of as a “choose x before y” directive rather than a constraint.

3 Likes
5

In reply to dave_59:

Thanks Dave.

6

In reply to dave_59:

Hello Dave ,

For the following Snippet :



rand bit x;
rand bit [1:0] y;

constraint CONS { ( x == 0 ) -> ( y == 0 ) ; }

I have the following Solution Space


 x    y     Probability

  0   0      1/5
  0   1      0 
  0   2      0
  0   3      0
  1   0      1/5
  1   1      1/5 
  1   2      1/5
  1   3      1/5

What would be the solution space if :

( A ) I have solve x before y ;
( B ) I have solve y before x ;

Having both would be an error

Thanks ,
Himanshu Valecha

7

In reply to himanshu valecha:

As I stated above, and more detailed here, the solve before construct does not change the solution space. Solve x before y changes the distribution of values chosen for x from 0: 20%, 1: 80%, to 0: 50%, 1: 50%.

1 Like
8

Revisiting an old thread:
If I rewrite the constraint in the original post and add a distribution on ‘kind’ variable. How would it work with and without ‘solve kind before len’ ? Would there be an implicit ordering enforced in simulator to satisfy distribution on ‘kind’?


constraint pkt_constraint1 {
    kind dist {SHORT:=70, MED:=20, and LONG:=10};
    (kind==SHORT)-> (len <5);
    (kind==MED)  -> (len inside {[5:9]});
    (kind==LONG) -> (len >= 10); 
}
9

In reply to sidda9:
Yes, you could say there is an implicit ordering with a distribution constraint. However the LRM is very lax when it comes to dealing with more than one distribution constraint.

1 Like