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. -- This message has been scanned for viruses and dangerous content by MailScanner, and is believed to be clean.Received on Thu Jun 5 14:06:57 2008
This archive was generated by hypermail 2.1.8 : Thu Jun 05 2008 - 14:07:42 PDT