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.