Hi Tom, I think that you should use $sampled on a and b in the assignmens of your example to avoid discrepancy between what the assertion and the asssignments observe. Best.. ed > -----Original Message----- > From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On > Behalf Of Thomas Thatcher > Sent: Tuesday, July 24, 2007 5:22 PM > To: Seligman, Erik > Cc: sv-ac@eda-stds.org > Subject: Re: [sv-ac] Feedback on 1900 (new 'checker' construct) > > Hi Erik, > > Just putting in writing what I said in the committee meeting today. > > We are in favor of the checker construct, and are very > interested in seeing it > implemented. > > We have the following suggestion: Allow the inclusion of > reg, wire, logic > variables, as well as always block constructs. However, any > construct within > a checker should be defined as non-synthesizable, and won't > result in extra > hardware in the design. > > My reasoning is that people writing checker code may be more > comfortable with > that syntax than with the new free variable syntax. (I will > check around Sun > to see if others agree with me on this). > > For example, we might write a checker like this: > > checker follows (clk = $inferred_clk, a, b); > > reg a_active = 1'b0; > always @(posedge clk) { > if (a) a_active <= 1'b1; > else if (b) a_active <= 1'b0; > else a_active <= a_active; > > a1 : assert property (!a_active |-> !b); > endchecker > > > > This would be pretty much equivalent to this > > checker follows (clk = $inferred_clk, a, b); > > bit a_active = 1'b0; > > function bit next_a_active; > if (a) return 1'b1; > else if (b) return 1'b0; > else return a_active > endfunction > > a_active <= @(clk) next_a_active; > a1 : assert property (!a_active |-> !b); > endchecker > > with the exceptions of sampling regions, etc. Either syntax > should work, > either in simulation or in the formal tools. In fact, in > this case, with the > if-then-else, the first syntax may be slightly more > convenient. A function > wasn't needed to contain the if-then-else construct. > > Free variables would have advantages, and advanced people > would probably use > them exclusively, but average designers would have a choice > to use familiar > syntax. > > Tom > > Seligman, Erik wrote On 07/23/07 11:53 AM,: > > > > Hi guys-- > > I'm going to start working on the 'real' proposal (manual > format) for > > item 1900. Please try to send any feedback you have at this point. > > Thanks! > > > > -- > ------------------ > Thomas J. Thatcher > Sun Microsystems > 408-616-5589 > ------------------ > > -- > This message has been scanned for viruses and > dangerous content by MailScanner, 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 Tue Jul 24 18:43:14 2007
This archive was generated by hypermail 2.1.8 : Tue Jul 24 2007 - 18:43:28 PDT