User experience with PSL-Sugar

Newsletter · Original Contribution Joined: Dec 08, 2003 Posts: 1107

(Originally from Issue 4.13, Item 7.0)

From: Anonymous

I am interested to know how useful people have found this language -
in a dynamic simulation context?

I recently spent a short time evaluating it on some relatively small
VHDL blocks (~1000 lines). My approach was to attempt to create a
'black-box' description from the (comprehensive) specification.
Although of course not an expert user of the language my feeling, was
that one hits a brick-wall quite quickly in trying to create a full
design description.

For example one of the blocks had a bus-bridge function. It was quite
easy to individually describe correct transactions on each side of the
bridge but creating the logical connection between the two
transactions is not so easy. Contrast this with for example 'e' which
has a scoreboard construct exactly for this purpose.

Maybe my approach is wrong - perhaps PSL was never intended for the
black-box description of complex blocks? Rather instead I should have
perhaps used the designs internal registers, etc to specify the more
complex aspects of the behaviour?

Newsletter · Original Contribution Joined: Dec 08, 2003 Posts: 1107

(Originally from Issue 4.14, Item 7.0)

From: Gadiel Auerbach

I intensively used PSL/Sugar in few verification projects in the last
months. I found the language useful as it addressed my needs as a
verification engineer. My primary use of the language has been for
static formal-verification purposes rather than for dynamic
simulations. PSL/Sugar has dual nature as it's both an assertion
language and a modeling language. However, the language is mainly an
assertion language which formulates declarative statements about the
design. For example, the formula

assert always !(RDY & ERR)

declares that RDY and ERR are mutual exclusive. The modeling part of
the language describes hardware similar to Verilog and VHDL. During a
verification task, most of my time and effort are dedicated to
formulation and checking of assertions.

Although assertions consume most of my time, I usually begin a
verification task using the modeling part. PSL/Sugar modeling
statements are used to drive the input signals of the design under
test. I'm often using mode settings to impose constraints on the
inputs. For example,

vmode read_only {
assume always WRT = 0;
}

defines an artificial limitation on the input signal WRT, which
partitions the verification task. Once the inputs are defined, I write
assertions about every output signal. The assertions verify that each
signal exactly complies with the behavior defined in the specification
document. For example,

vunit RDY {
assert always {RDY; true}(RDY until !REQ};
assert always (fell(RDY) -> fell(REQ));
}

contains a set of assertions about RDY. The first statement declares
that if RDY is asserted than it will remain asserted forever or until
REQ is deasserted. The second statements declares that if the value of
RDY changed from 1 to 0 than the value of REQ changed as well.

I hope this helps. In particular, this should exemplify the nature of
PSL/Sugar as an assertion language, as opposed to a verification
language (which PSL/Sugar is not). This also goes to explain why
PSL/Sugar does not include facilities for scoreboarding, variables
etc.

- Gadiel Auerbach, IBM Israel

Newsletter · Original Contribution Joined: Dec 08, 2003 Posts: 1107

(Originally from Issue 4.14, Item 7.1)

From: Harry Foster

Your conclusion is more or less correct - PSL was not specifically
intended for black-box description of complex blocks. It was designed
to support white-box description of the details of those complex
blocks and associated interfaces.

To elaborate somewhat:

Testbenches typically take a "black-box" view of the design.
Testbench driven verification involves three major elements:

1. vector generation: stimulating the design

2. correctness checking: verifying that the design behaves correctly
when stimulated. This includes scoreboarding techniques for
checking expected results.

3. coverage analysis: verifying that all the relevant functionality
of the design has been tested

PSL was not designed to replace testbench languages. So it does not
include features such as scoreboarding. However, PSL is a very
powerful tool for checking for correct behavior within the design, as
well as for verifying coverage of internal operations. In effect, PSL
enables a "white-box" view of the internal operation of the design.

Complete verification involves a collection of tools and
techniques. Testbenches uses a black-box view to check the
input/output behavior of the design, whereas PSL provides a white-box
view to check the internal operation of the design. As a result, PSL
provides powerful and complementary capabilities when used in
conjunction with traditional simulation testbench approaches.

- Harry Foster, Chair, Accellera FVTC
- Erich Marschner, Co-Chair, Accellera FVTC

Newsletter · Original Contribution Joined: Dec 08, 2003 Posts: 1107

(Originally from Issue 4.15, Item 6.0)

From: Ben Cohen

Even tough testbenchess use black-box views, PSL is also useful at
that black-box level where the interface protocols and restrictions
can be specified in the requirement document, and can be verified
during dynamic or formal verification. For example:

/*
* Behavior: if the transfer type is BUSY then on the corresponding
* data transfer, the slave must provide a zero wait state OKAY response
* (default clock)
*/

// psl property ResponseToBusyMustBeZeroWaitOKAY =
// always (((htrans == BUSY) && (hready == 1)) ->
// next ((hresp == OKAY) && (hready == 1)) );
// psl assert ResponseToBusyMustBeZeroWaitOKAY;

I also believe that PSL can be used with traditional simulation
testbench approaches. For example, a scoreboard can be modeled in HDL
where transaction information and expected results can be written into
the scoreboard. Then a PSL statement can be written to determine if
the DUT is matching the expected results. For example:

// psl property CheckCounterData =
// always ({rose(top.scoreboard.count_load)} |=>
// {[*0:3];top.dut.counter==top.scoreboard.count_value});
// psl assert CheckCounterData;

Above states that if there is a new load transaction, then within 3
cycles the DUT counter must have the count_value that we expect to
have. Note that the 3 cycles is arbitrary, and can be tuned to as
many cycles as expected. The range allows for a variation in cycle
timing in the DUT design. One restriction: The new loaded value must
be different that the previous value. To overcome that restriction, a
new condition or timing needs to be defined. For example, if we know
that it takes exactly 3 cycles after the count_load transaction, then
the following can be described:

// always ({rose(top.scoreboard.count_load)} |=>
// {[*3];top.dut.counter==top.scoreboard.count_value});

Another alternative making use of the DUT FSM:

// always ({rose(top.scoreboard.count_load)} |=>
// {[*0:3];(top.dut.counter==top.scoreboard.count_value) &&
// (top.dut.fsm==LOAD)});

Bottom line: PSL was not designed to replace testbench languages, but
it is great for requirement documentation, and can greatly simplifies
the verification process thru static and dynamic white-box, black-box
(i.e., interfaces) verification. In addition, it simplifies the
verification logic of a TB design.

- Ben Cohen

Newsletter · Original Contribution Joined: Dec 08, 2003 Posts: 1107

(Originally from Issue 4.16, Item 10.0)

From: Robert Ruiz

I wanted to let you know that it's good to see a recent increase in
discussions around assertions. There is much to be said about the
technologies, methodologies, and languages to improve verification
efficiency.

In regard to languages, your readers would benefit if posts such as
the one from IBM's Gadiel Auerbach, made clear which language is being
referenced, PSL or Sugar, rather than referring to a "/" language.
Since there are different proprietors and versions of each language
(Accellera's language is referred to only as PSL), this would help in
the overall understanding of each language and specific tool
capabilities.

- Robert Ruiz, Synopsys