Hi Adam, Active method should be very useful, but it requires a precise definition of an active evaluation attempt. Are you talking about antecedents only, do you recognize them syntactically, what if they are negated or nested, how to define this method for coverage etc.? What its formal semantics should be? I suggest opening a Mantis item to be addressed during the next PAR. Thanks, Dmitry ________________________________ From: Adam Krolnik [mailto:adam.krolnik@verisilicon.com] Sent: Saturday, June 07, 2008 12:24 AM To: Thomas.Thatcher@Sun.COM Cc: Korchemny, Dmitry; sv-ac@eda.org; sv-sc@eda.org Subject: Re: [sv-sc] ended vs. triggered Hello all; As a separate idea on the assert window checker, I once proposed a way to determine if there was a started property/sequence (looking for the consequent.) That way instead of having to write the window function, you could directly check for the property or sequence being active (a certain number of times.) property active_window(start, test, end) (start & active_window.active == 0 |-> test [*0:$] ##0 end) endproperty There are protocols that only allow one active transaction, and there are protocols that allow for more than one (but limited). Having the 'active' method, returning the number of active threads would allow one to easily model the various protocols. Back to the original discussion... Thomas Thatcher wrote: 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(). 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. 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. 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. 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? 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/> <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/> <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. -- Soli Deo Gloria Adam Krolnik Director of Design Verification VeriSilicon Inc. Plano TX. 75074 Co-author "Assertion-Based Design", "Creating Assertion-Based IP" --------------------------------------------------------------------- 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:55:57 2008
This archive was generated by hypermail 2.1.8 : Wed Jun 11 2008 - 01:58:50 PDT