SV solver puzzle part II – “guidance” vs. “dictation”

 

With one of our recent blog entries on SystemVerilog constraint solver (http://www.cvcblr.com/blog/?p=725) becoming so popular, several readers have contacted us via email to know little more about the puzzle. Specifically they wanted to understand how the solver ordering of variables is determined. Consider the same example as in that previous blog entry:

As noted in the previous blog, this creates an “implicit ordering” of variables – i.e. ‘v1” is solved BEFORE “v2”. A smart engineer (Muthurasu Sivaramakrishnan) asked this:

• Nice one. However, why cant we use Solve.. Before constraint in this scenario?

The answer is a little involved with yet-another subtlety in the language, and hence this new entry:

This reader’s question boils down to whether the above constraint “cst_ordered” is same as the following;

constraint cst_guidance {solve v1 before v2;}

First intuition says YES, but the answer unfortunately is NO. In SV there are 2 kinds of solver ordering - an ordering constraint is more of a "guidance on probability" and does NOT change the solution space. Hence it can't lead to a failure from a success or vice-versa. This is what happens with a solve..before – i.e. it is simply a “guidance” or suggestion to the solver.

However the ordering that gets enforced via function call is more STRICT/DICTATIVE in nature. It enforces the order by further "subdividing" the solution space and in a sense invokes the solver twice. In Questa you can actually see this in action via -solveverbose - you will see 2 "Working Set" prints for function based constraint:

1. First the solver gets “dictated” to solve “v1” INDEPENDENTLY. In a random choice, say it picked a value “1”

2. Now the solver takes up the next variable to be solved in THAT order, i.e. “v2” – you see in Questa the “Working Set’ print with details (note: randomize is called only once per iteration in user code)

 

So this leads to a constraint solver failure. Whereas a mere “guidance” shown by a solve..before would have solved both the variables TOGETHER, leading to a successful solving operation.

Bottomline: The function call “strictly enforces” the solve order, while the “solve..before” is more of a “guidance/suggestion”.

To learn more about this and other advanced SystemVerilog topics, join our training via www.cvcblr.com/trainings

Good Luck

TeamCVC 

Technorati Tags: SystemVerilog,EDA,Constraints,Questa

SVA: default disable – a boon or a bane?

As the SVA usage expands/grows in the industry, so do the language syntax/features. One of the recent (2009) addition to System Verilog language was the ability to code “default disabling condition”.

It is very handy to have an “inferred” disabling condition for all assertions so that one can save on verbosity while typing – every assertion doesn’t have to repeat;

  a_without_default_disable : assert property (disable iff (!rst_n) my_prop);

vs.

a_with_default_disable : assert property (my_prop);

Obviously anything that helps to save some typing is a BOON.

However there are some special category of assertions that may get unintentionally disabled by this. For instance the “reset-checks” – assertions that check the reset value of various DUT outputs. For e.g.

• FIFO empty flag during reset
• serialout signal from a de-serializer design

We recently had a similar DUT being verified with SVA. In the below code, notice the “default disable” and the reset-check

As the callout/marking shows – there is a bug in DUT, the signal “serialout” is indeed HIGH during reset, yet the assertion doesn’t fire (Questa shows it as INACTIVE – meaning it is a vacuous success in this case).

So that begs the question of “is the default disable a boon or a BANE”?       

The answer is – you need a methodology and a plan while doing your assertions – categorize the assertions appropriately. Specifically group them as:

• Reset checks
• Functional checks
• Low Power checks

etc. Here is a nice work-around for this:

• Use an explicit “disable iff (1’b0)” for those special category assertions

 

Now Questa flags it nicely as below:

So do use the new SVA stuff on “default disable” – it is indeed a BOON. Just make sure you “think” before you code those special category of assertions.

This is part of our larger story of ABV methodology being rolled out as next generation verification training sessions at CVC. So do contact us via training@cvcblr.com  for more advanced, practical usage of this wonderful technology.

Good Luck

TeamCVC

Technorati Tags: SystemVerilog,SVA,ABV

SystemVerilog constraint puzzle – treat for CRV lovers

Are you an avid fan of CRV – Constraint Random Verification? Have you played enough with System Verilog constraints? Many of our customers having attended our regular VSV training (http://www.cvcblr.com/trainings) do become so! One of the nice features of SystemVerilog constraint mechanism is its “bi-directionality” – a key feature that makes the distribution fairly wide spread and makes the state space well covered.

The industry has learnt it over the last decade of CRV usage – bidirectional constraints are better than unidirectional ones (that was the default in previous generation solver inside popular tool like Specman – called PGen. Even Specman has moved to a more robust, bi-directional IGEN/Intelligen few years back).

In SV this bi-directionality is subtle. Consider the code below:

To an average SV engineer the above 2 constraints look “same” as the function is trivially doing a return job. However they are different for an avid SV user or a solid SV solver such as Questa from Mentor. As per LRM:

Random variables used as function arguments shall establish an implicit variable ordering.

Hence in case of “cst_ordered”, the variable “v1” is solved FIRST and then the “v2” – i.e. they are solved separately and not together (Which is what happens with ‘cst_bidir”).

So what’s the big deal? Consider “v1” is chosen to be “1” first, then the solver has NO solution for “v2” :-( leading to a constraint failure.

So, next time when you use a function in a constraint, remember/recall/read this blog :-)

Care for a proof? See what Questa’s solveverbose prints:

qverilog file.sv –R –solveverbose=2

Enjoy CRV, enjoy SystemVerilog. In case you want to delve deeper into SV, do call us via training@cvcblr.com

TeamCVC

Technorati Tags: SystemVerilog,EDA,Questa