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.Received on Tue Jul 24 14:22:21 2007
This archive was generated by hypermail 2.1.8 : Tue Jul 24 2007 - 14:22:30 PDT