Hi Tom, Please, see my comments below. Thanks, Dmitry -----Original Message----- From: Thomas.Thatcher@Sun.COM [mailto:Thomas.Thatcher@Sun.COM] Sent: Saturday, June 07, 2008 12:06 AM To: Korchemny, Dmitry Cc: Adam Krolnik; sv-ac@eda.org; sv-sc@eda.org Subject: Re: [sv-sc] ended vs. triggered Dmitry, Your example had what was probably a typo: start_event and end_event were defined as "logic". You probably intended to define them as "sequence". Since they were defined as logic, it's doubtful that you could use sequence methods on them. (You could argue that a logic variable is a boolean, which is the simplest type of sequence, but I think this is a stretch). If start_event and and end_event were defined as sequences (which I think is what you intended). Then yes, you can use the sequence methods ended() and triggered(). [Korchemny, Dmitry] Yes, thanks, this is a typo. I've fixed it. Non-blocking statements occur in two steps: 1. The Right-hand side is evaluated (Active Region) 2. The left-has side is updated (NBA (or Re-NBA?) Region) (see draft 5, p 187) So although we delay the update to Re-NBA, does that help with anything? The RHS value is still evaluated in the Active region. We can't move the evaluation to Reactive region, because then we would see shoot-through of values on the inputs of the checker. [Korchemny, Dmitry] Could you elaborate your statement about the Reactive region? The only way to make this work with sequences, I believe is to modify the always block as follows: always @(clock or start_flag or end_flag) window <= next_window(window); Here's how I think it would work: 1. First time through the Active region: clock event processed. New value for window is calculated. The function sees start_event.triggered==0, end_event.triggered==0 2. Observed Region: start_event.ended set to 1 3. Loop back to Active region. start_event.triggered causes always block to execute again. 4. New value for active calculated: It overrides the previous calculated value. 5. Re-NBA region: variable *active* is assigned. [Korchemny, Dmitry] I will make this fix, but I would like to understand why we can't process the clock event in the Reactive region. Note that this ONLY works if the following conditions are satisfied: 1. The assignments don't refer to any inputs to the checker. OR 2. Any references to input variables must use the $sampled() function. [Korchemny, Dmitry] The original proposal contained a statement that the design variables in the right-hand side of a checker variable assignment were sampled. I could not find this statement anymore in the new proposal, so I am putting it back at the top of Page 11 (Checker variable assignments): All variables in the right-hand side of a checker variable assignment are sampled. After looking at this, I believe there is no reason to make a special case for non-blocking assignments in checkers. Having non-blocking assignments update in the NBA region should work fine, even within checkers. The coding guidelines would be as follows: 1. If you are just doing normal assignments, and not calling sequence methods, everything is the same as it is outside of a checker. 2. If a non-blocking assignment contains a call to a sequence method like triggered(), then: a. The sequence method itself must be in the process sensitivity list b. References to all other state variables must explicitly use the $sampled() system function to get the sampled value, if that is what is expected. What do others think? [Korchemny, Dmitry] Calling $sampled method explicitly is problematic since in case of a checker input argument you don't know from where it came: from design or from another checker. This should be done implicitly. Since the checker variables in the blocking assignments are non-sampled, the argument passing from one checker to another one needs to be clarified, it cannot be a substitution anymore. I suggest postponing this discussion until the next PAR. Tom Korchemny, Dmitry wrote: > Hi Tom, > > I don't quite understand your comment. If start_event and end_event are > sequences how the example is supposed to work using > > let start_flag = start_event; > let end_flag = end_event; > > ? > > I don't see a problem with the .triggered method in the always block > since we agreed that the checker variable NBA is executed the in Re-NBA > region. When the assignment is performed, .triggered should have already > been available. > > Thanks, > Dmitry > > -----Original Message----- > From: Thomas.Thatcher@Sun.COM [mailto:Thomas.Thatcher@Sun.COM] > Sent: Friday, June 06, 2008 12:06 AM > To: Adam Krolnik > Cc: Korchemny, Dmitry; sv-ac@eda.org; sv-sc@eda.org > Subject: Re: [sv-sc] ended vs. triggered > > Hi Adam, Dmitry, > > I agree. The example can be fixed by changing the let assignment: > > let start_flag = start_event; > let end_flag = end_event; > > And the checker works as intended. > > > > But suppose start_event and end_event were defined as sequences in the > checker. Using ended or triggered in the procedural code is still > problematic. That is because the always block executes in the active > region when its clock event is processed. At this point, a call to the > triggered() method returns 0. It's not set until the Observed region. > Therefore, the window variable will never be set to one. If the > triggered() status causes the simulator to return to the Active region, > the always procedure will not be re-evaluated. It's event has already > been processed. > > > So for this example, forget about the triggered method. The example > works without it. > > Tom > > Adam Krolnik wrote: >> Hello Mr. Korchemny; >> >> I did not know that you can use the .triggered and .ended methods on a > >> logic typed variable. >> >> *logic* start_event, // Window opens at the completion of the > start_even* >> ** assign* start_flag = start_event.ended; >> >> >> >> Are you supposed to use an expression, or a property/sequence when >> instantiating the checker? >> Or is this supposed to work for both ? >> >> >> >> Korchemny, Dmitry wrote: >>> Hi all, >>> >>> >>> >>> While trying to re-craft the checker proposal, I found a problem >>> regarding .ended and .triggered sequence methods. Here is the > original >>> version of a checker example corresponding to one of the OVL checkers > >>> in the proposal: >>> >>> >>> >>> *typedef enum* { cover_none, cover_all } coverage_level; >>> >>> *checker* assert_window ( >>> >>> *logic* test_expr, // Expression to be true in the window >>> >>> *logic* start_event, // Window opens at the completion of the >>> start_event >>> >>> *logic* end_event, // Window closes at the completion of the > end_event >>> *event* clock = $inferred_clock, >>> >>> *logic* reset = $inferred_disable, >>> >>> *string* error_msg = "violation", >>> >>> coverage_level clevel = cover_all >>> >>> ); >>> >>> *default clocking* @clock; *endclocking* >>> >>> * default disable iff* reset; >>> >>> >>> >>> * free checkvar bit* window = 0; >>> >>> * free checkvar bit* start_flag, end_flag; >>> >>> * assign* start_flag = start_event.ended; >>> >>> * **assign* end_flag = end_event.ended; >>> >>> >>> >>> // Compute next value of window >>> >>> *function bit* next_window (*bit* win); >>> >>> *if *(reset || win && end_flag) >>> >>> * return *1'b0; >>> >>> *if* (!win && start_flag == 1'b1) >>> >>> * return* 1'b1; >>> >>> *return* win; >>> >>> *endfunction* >>> >>> >>> >>> *always_check* @clock >>> >>> window <= next_window(window); >>> >>> >>> >>> *property* p_window; >>> >>> start_flag && !window |=> test_expr[*1:$] ##0 end_flag; >>> >>> *endproperty* >>> >>> >>> >>> a_window: *assert property* (p_window) *else *$error(error_msg); >>> >>> >>> >>> *generate* *if* (coverage_level != ovl_cover_none) *begin* : > cover_b >>> cover_window_open: *cover property* (start_flag && !window) >>> >>> * *$display("win_open_covered"); >>> >>> >>> >>> cover_window: *cover property* ( >>> >>> start_flag && !window >>> >>> ##1 (!end_flag && window) [*0:$] >>> >>> ##1 end_flag && window >>> >>> ) $display("window covered"); >>> >>> *end* : cover_b >>> >>> * endgenerate* >>> >>> *endchecker* : assert_window >>> >>> >>> >>> Note the highlighted part here: .ended method of start_event and >>> end_event is used in continuous assignments of checker variables >>> start_flag and end_flag, and then these checker variables are used in > >>> assignments in functions and in assertions (see highlighted text). >>> This was expected to work. >>> >>> >>> >>> Consider now the new version: >>> >>> >>> >>> *typedef enum* { cover_none, cover_all } coverage_level; >>> >>> *checker* assert_window ( >>> >>> *logic* test_expr, // Expression to be true in the window >>> >>> *logic* start_event, // Window opens at the completion of the >>> start_event >>> >>> *logic* end_event, // Window closes at the completion of the > end_event >>> *event* clock = $inferred_clock, >>> >>> *logic* reset = $inferred_disable, >>> >>> *string* error_msg = "violation", >>> >>> coverage_level clevel = cover_all >>> >>> ); >>> >>> *default clocking* @clock; *endclocking* >>> >>> *default disable iff* reset; >>> >>> >>> >>> *free* *bit* window = 0; >>> >>> * let* start_flag = start_event.triggered; >>> >>> * **let* end_flag = end_event.triggered; >>> >>> >>> >>> // Compute next value of window >>> >>> *function bit* next_window (*bit* win); >>> >>> *if *(reset || win && end_flag == 1'b1) >>> >>> *return* 1'b0; >>> >>> *if* (!win && start_flag == 1'b1) >>> >>> *return* 1'b1; >>> >>> *return* win; >>> >>> *endfunction* >>> >>> >>> >>> *always* @clock >>> >>> window <= next_window(window); >>> >>> >>> >>> *property* p_window; >>> >>> start_flag && !window |=> test_expr[*1:$] ##0 end_flag; >>> >>> *endproperty* >>> >>> >>> >>> a_window: *assert property* (p_window) *else *$error(error_msg); >>> >>> >>> >>> *generate* *if* (coverage_level != ovl_cover_none) *begin* : > cover_b >>> cover_window_open: *cover property* (start_flag && !window) >>> >>> * *$display("win_open_covered"); >>> >>> >>> >>> cover_window: *cover property* ( >>> >>> start_flag && !window >>> >>> ##1 (!end_flag && window) [*0:$] >>> >>> ##1 end_flag && window >>> >>> ) $display("window covered"); >>> >>> *end* : cover_b >>> >>> *endgenerate* >>> >>> *endchecker* : assert_window >>> >>> >>> >>> We don't have continuous assignments in checkers anymore and we need >>> to use let. Now the question is how this let should be defined. In > the >>> code above it has .triggered method, and this will work in the >>> function, but not in the assertions, since it is illegal to use >>> .triggered method there. Had I written .ended instead, it would have >>> worked for assertions but not for assignments, since .ended exists in > >>> the Observed region only. Therefore the only workaround is to have > two >>> let definitions: >>> >>> >>> >>> let start_flag_for_assignments = start_event.triggered; >>> >>> let start_flag_for_assertions = start_event.ended; >>> >>> which IMO is unacceptable. >>> >>> >>> >>> I see two ways to address this problem: >>> >>> 1. To introduce back continuous assignments of checker variables >>> >>> 2. To modify .ended and .triggered definition >>> >>> >>> >>> Since the first possibility was found controversial, and it would be >>> difficult to converge in the remaining timeframe, I suggest >>> investigating the second one. >>> >>> >>> >>> Here are the definitions of .ended and .triggered from 16.13.6: >>> >>> >>> >>> The value of method ended evaluates to true if the given sequence has > >>> reached its end point at that particular >>> >>> point in time and false otherwise. The ended status of the sequence > is >>> set in the Observed region >>> >>> and persists through the Observed region. This method shall only be >>> used to detect the end point of >>> >>> a sequence used in another sequence. It shall be considered an error >>> if this method is used in *disable iff* >>> >>> boolean expression for properties. There shall be no circular >>> dependencies between sequences induced by >>> >>> the use of ended. >>> >>> The value of method triggered evaluates to true if the given sequence > >>> has reached its end point at that particular >>> >>> point in time and false otherwise. The triggered status of the >>> sequence is set in the Observed >>> >>> region and persists through the remainder of the time step. This >>> method shall only be used in *wait *statements >>> >>> (see 9.4.4) or boolean expressions outside sequence context or in the > >>> *disable iff* >>> >>> boolean expression for properties. It shall be considered an error to > >>> invoke this method on sequences that >>> >>> treat their formal arguments as local variables. A sequence treats > its >>> formal argument as a local variable if >>> >>> the formal argument is used as an lvalue in /operator_assignment /or >>> /inc_or_dec_expression /in >>> >>> sequence_match_item. >>> >>> >>> >>> Note that the definitions of .ended and .triggered are mutually >>> exclusive: it is illegal to use .ended where it is legal to use >>> .triggered and vice versa. It means that is enough to have only one >>> construct in the language (and deprecate the other), and to make >>> actual implementation decision based on the context. I have to say >>> that even now it is very confusing for the user to have two different > >>> methods meaning essentially the same thing. >>> >>> >>> >>> What do you think? >>> >>> >>> >>> Dmitry >>> >>> --------------------------------------------------------------------- >>> Intel Israel (74) Limited >>> >>> This e-mail and any attachments may contain confidential material for >>> the sole use of the intended recipient(s). Any review or distribution >>> by others is strictly prohibited. If you are not the intended >>> recipient, please contact the sender and delete all copies. >>> >>> >>> -- >>> This message has been scanned for viruses and >>> dangerous content by *MailScanner* <http://www.mailscanner.info/>, > and is >>> believed to be clean. >> -- >> 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. > --------------------------------------------------------------------- > Intel Israel (74) Limited > > This e-mail and any attachments may contain confidential material for > the sole use of the intended recipient(s). Any review or distribution > by others is strictly prohibited. If you are not the intended > recipient, please contact the sender and delete all copies. > --------------------------------------------------------------------- Intel Israel (74) Limited This e-mail and any attachments may contain confidential material for the sole use of the intended recipient(s). Any review or distribution by others is strictly prohibited. If you are not the intended recipient, please contact the sender and delete all copies. -- This message has been scanned for viruses and dangerous content by MailScanner, and is believed to be clean.Received on Wed Jun 11 01:31:29 2008
This archive was generated by hypermail 2.1.8 : Wed Jun 11 2008 - 01:32:29 PDT