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, and is believed to be clean.Received on Wed Jun 4 08:25:11 2008
This archive was generated by hypermail 2.1.8 : Wed Jun 04 2008 - 08:28:01 PDT