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