Yes, using non-blocking assignments for clocked processes is considered good style. -- Matt Maidment mmaidmen@ichips.intel.com ________________________________ From: owner-sv-ac@server.eda.org [mailto:owner-sv-ac@server.eda.org] On Behalf Of Warmke, Doug Sent: Wednesday, October 31, 2007 6:27 PM To: Adam Krolnik Cc: sv-ac@server.eda.org Subject: [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 <http://www.mailscanner.info/> , and is believed to be clean. -- This message has been scanned for viruses and dangerous content by MailScanner, and is believed to be clean.Received on Thu Nov 1 00:53:01 2007
This archive was generated by hypermail 2.1.8 : Thu Nov 01 2007 - 00:53:38 PDT