[sv-ac] RE: [sv-bc] New Proposal uploaded for Mantis 2005

OK, that's a good suggestion.

Here is what I changed the example to.

 

Note: I changed the blocking assignments in the always_ff

to be NBA's.  Is that still considered "good RTL coding style"

for clocked processes, Cliff?

 

module fsm(input clk, rst, a, b);

...

always_comb begin : b1

    a42: assert @(posedge clk) (a == b);

    ...

end

 

always_ff (@posedge clk) begin : b2

    state <= nextstate;

    if (somecond) begin

        b <= !b;

        ...

    end

    ...

end

endmodule

 

In this case, deferred assertion a42 is associated with the design's
clock as its event control.  This construct will never result in any
deferred assertion reports. The current clock cycle's deferred assertion
will mature in the Observed region of the time step corresponding to the
start of the next clock cycle. But by that time, the Active region of
the next clock cycle will already have executed (since b changed and
triggered the always_comb), which will result in a flush point for a42.
Thus by the time the Observed region occurs, the original pending
assertion report will no longer be scheduled on the deferred assertion
report queue, and no report will be issued.

 

Thanks and regards,

Doug

 

From: Adam Krolnik [mailto:adam.krolnik@verisilicon.com] 
Sent: Wednesday, October 31, 2007 12:23 PM
To: Warmke, Doug
Cc: sv-ac@server.eda.org; sv-bc@server.eda.org
Subject: Re: [sv-bc] New Proposal uploaded for Mantis 2005

 


Hi Doug;

Don't you want to explain how 'a' or 'b' being changed at the positive
edge of the clock will flush
an deferring assertion reporting ? Having the b2 block seems to do this.

Lint tools will do well to check for deferred assertions operating on
registers that are affected by
the same event as the deferred assertion - as discussed below.

    Thanks.


Warmke, Doug wrote: 

Hi Adam,

 

A couple responses embedded...

 

From: Adam Krolnik [mailto:adam.krolnik@verisilicon.com] 
Sent: Wednesday, October 31, 2007 8:52 AM
To: Warmke, Doug
Cc: sv-ac@server.eda.org; sv-bc@server.eda.org
Subject: Re: [sv-bc] New Proposal uploaded for Mantis 2005

 


Hello all;

Section 16.4.4, the last example could be enhanced to show the
connection between the signals
used in the assertion and the signal being registered. Presumably the
connection is to show
that 'a' or 'b' is influenced (changed) by state being changed.

 

The b2 block is irrelevant to the issue at hand.

I was just trying to create a more 'realistic-looking' RTL module.

I have removed b2 from rev 2 of the proposal.



module fsm(input clk, rst, a, b);
...
always_comb begin : b1
    a42: assert @(posedge clk) (a == b);
    ...
end
always_ff (@posedge clk) begin : b2
    state = nextstate; // change to a or b ?
    ...
end
endmodule

I have a concern with this close syntax and quite different operation.

good:   assert property ( @(posedge clk) a == b);
almost: assert @(posedge clk) (a == b);

The assertion labeled 'good' is a concurrent assertion that will verify
'a' versus 'b'.
The assertion labeled 'almost' is a deferred assertion that will NOT
result in any assertion report
if 'a' or 'b' are registers based on 'clk'.  And yet it almost looks
correct - even to the trained eye.

 

I see your point. I think that with training and experience

it will be OK for people to train themselves to look for 'property'.

 

Think about immediate assertions, too. See "kinda" below.

 

        good:   assert property ( @(posedge clk) a == b);
        almost: assert @(posedge clk) (a == b);

        kinda:  assert (clk == 1'b1 && a == b);

 

The main point is the existence of the assert keyword to

start everything off.  After that, one has to parse through

the rest of the syntax to figure out what's going on.

 

The problem with what you have below is that it breaks symmetry.

The original idea (and possibly a future idea if the problems can be
worked out)

is to have the syntax be

 

             assert [ delay_control | event_control ] (expression) ...

 

For now, the only kind of delay_control allowed is #0.

We wanted to have arbitrary time delays, but as Steven Sharp pointed
out,

there are some serious problems with that approach.  With time and
effort,

maybe those can be overcome, but not for this rev of the LRM.

 

I think adding a new keyword, like 'deferred', could help alleviate

the 'closeness' in the syntax.  But keyword inflation is a bad thing.

And if we went that way, why not add 'immediate' as well,

to really clarify the differences?

 

In summary, I'm OK with the syntactic differences, but I think

it would be good if someone hits a breakthrough idea that

makes sense and helps make the syntax even clearer.

 

Regards,

Doug



Could it be one of these syntaxes to more correctly distinguish between
the two ? The #0
better distinguishes concurrent assertions from deferred assertions.

better1: assert #0 @(posedge clk) (a == b);
better2: assert @(posedge clk) #0 (a == b);



Warmke, Doug wrote: 

Hi SV-AC,
 
I finally got our ideas incorporated into Erik's proposal,
and I uploaded it to Mantis.  The "Motivation" section
includes discussion of various changes (features and
non-features) that were made.  Hopefully that will
forestall later attempts to re-introduce them.
(I did forget to add an explanation of why non-zero
delay_control values would be a bad idea, but that
can be added later).
 
See http://www.eda-stds.org/svdb/view.php?id=2005
and look at the attached file SV-2005_D4-1.pdf.
 
Tej will be available to explain the proposal and answer
questions during the regular SV-AC meeting.
 
By the way, I created a similar proposal for unique/priority
if/case (Mantis 2008).  Pending review of 2005, I can modify
the proposal for 2008 and then upload it to Mantis as well.
 
Regards,
Doug
 
  






-- 
    Soli Deo Gloria
    Adam Krolnik
    Director of Design Verification
    VeriSilicon Inc.
    Plano TX. 75074
    Co-author "Assertion-Based Design", "Creating Assertion-Based IP"





-- 
    Soli Deo Gloria
    Adam Krolnik
    Director of Design Verification
    VeriSilicon Inc.
    Plano TX. 75074
    Co-author "Assertion-Based Design", "Creating Assertion-Based IP"

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.