[sv-ac] Re: [sv-sc] ended vs. triggered

From: Thomas Thatcher <Thomas.Thatcher_at_.....>
Date: Fri Jun 06 2008 - 14:27:38 PDT
Hello Everyone,

Does anyone have any example code showing how they use the sequence 
triggered() method?  After all this discussion, I have the impression 
that triggered() may be of limited value.  Or at least, the LRM gives 
the impression that it is more easy-to-use than it really is.

Thanks,

Tom

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/>,
>> 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.
>>
> 

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.
Received on Fri Jun 6 14:28:59 2008

This archive was generated by hypermail 2.1.8 : Fri Jun 06 2008 - 14:29:09 PDT