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

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"

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