Yes, this is the same type of solution that we often use in other places where the same type of problem arises. It works, but I personally find it awkward and error-prone. However, as I wrote before, there is a cost/benefit tradeoff. Otherwise, functional errors may slip through. Shalom From: Ben Cohen [mailto:hdlcohen@gmail.com] Sent: Tuesday, May 07, 2013 17:57 To: John Havlicek Cc: Bresticker, Shalom; sv-ac@eda-stds.org; Korchemny, Dmitry; Eduard Cerny; stuart@sutherland-hdl.com Subject: Re: [SV-AC] Should a[*1:0] be interpreted as a[*0]? // 16.7 Sequences John, I love your solution! That was very clever! I really like it. Also, thanks about your observation about the sensitivity error in the generate statement. Thus, the answer to "Should a[*1:0] be interpreted as a[*0]? // 16.7 Sequences" is NO; leave the LRM as is in the next go around. Thanks again, Ben On Tue, May 7, 2013 at 7:08 AM, John Havlicek <johnh@cadence.com<mailto:johnh@cadence.com>> wrote: I think that the generate solution is bad because of all the copying - maintenance is a problem. [BTW, I don't think the generate solution shown actually agrees with the English description at the bottom - the generate condition is only sensitive to RD_PARAM. Also, the original and the generate don't have the same sensitivity to "RD_PARAM > 0" and "WR_PARAM > 0" in the assertion antecedents. But I'm going to ignore those differences to make my point.] I don't think that this example is compelling for the language change suggested. One can put a constant expression in the repetition range to switch the lower bounds: ap_readhold: assert property(@ (negedge clk) rd && rd_ct==0 |-> @ (posedge clk) hold[*(RD_PARAM > 0 ? 1 : 0):RD_PARAM] ##1 data==mem[address]); property p_write; logic[31:0] v_data, v_address; @ (negedge clk) (wr && wr_ct==0, v_data=data, v_address=address) |-> @ (posedge clk) hold[*(WR_PARAM > 0 ? 1 : 0):WR_PARAM] ##1 (1, v_data =data, v_address=address) ##1 mem[v_address]==v_data; endproperty : p_write ap_write: assert property(p_write); Or, if that seems too untidy, one can use localparams to compute the repetition bounds and put the case analysis there. E.g. localparam RD_LB = RD_PARAM > 0 ? 1 : 0; localparam WR_LB = WR_PARAM > 0 ? 1 : 0; ... hold[*RD_LB:RD_PARAM] J.H. From: owner-sv-ac@eda.org<mailto:owner-sv-ac@eda.org> [mailto:owner-sv-ac@eda.org<mailto:owner-sv-ac@eda.org>] On Behalf Of Bresticker, Shalom Sent: Tuesday, May 07, 2013 7:55 AM To: hdlcohen@gmail.com<mailto:hdlcohen@gmail.com>; sv-ac@eda-stds.org<mailto:sv-ac@eda-stds.org>; Korchemny, Dmitry; Eduard Cerny; stuart@sutherland-hdl.com<mailto:stuart@sutherland-hdl.com> Subject: [sv-ac] RE: [SV-AC] Should a[*1:0] be interpreted as a[*0]? // 16.7 Sequences This type of thing occurs in other situations as well. There is a tradeoff between flagging errors and reinterpreting as a corner case. Shalom From: Ben Cohen [mailto:hdlcohen@gmail.com<mailto:hdlcohen@gmail.com>] Sent: Saturday, March 09, 2013 20:34 To: sv-ac@eda-stds.org<mailto:sv-ac@eda-stds.org>; Korchemny, Dmitry; Eduard Cerny; Bresticker, Shalom; stuart@sutherland-hdl.com<mailto:stuart@sutherland-hdl.com> Subject: [SV-AC] Should a[*1:0] be interpreted as a[*0]? // 16.7 Sequences 1800'2012::16.7 Sequences (LRM page 346) states "When a range is specified with two expressions, the second expression shall be greater than or equal to the first expression." I had a case where this caused the need to use the "generate .. endgenerate" and write two almost identical assertions to avoid this requirement. What I wanted was for a[*1:0] be interpreted as a[*0]. This occurred because I used parameters for the ranges. QUESTION: Do you feel that this is a worthy upgrade, and if so, should I write a mantis? Here is a piece of the example. Attached is dut_mem_err.sv<http://dut_mem_err.sv> where I am using a parameter initialized to 0, and that causes the second expression of the range to be less than the first. I really wanted a[*1:0] to be the same as a[*0]. The fix with the generate is in dut_mem.sv<http://dut_mem.sv>. module dut_mem #(WR_PARAM =1, RD_PARAM=1, MEM_DEPTH_PARAM=1024) ( input logic clk, rd, wr, rst_n, input logic[31:0] address, output logic hold, inout logic[31:0] data); ap_readhold: assert property(@ (negedge clk) rd && RD_PARAM > 0 && rd_ct==0 |-> @ (posedge clk) hold[*1:RD_PARAM] ##1 data==mem[address]); property p_write; logic[31:0] v_data, v_address; @ (negedge clk) (wr && WR_PARAM > 0 && wr_ct==0, v_data=data, v_address=address) |-> @ (posedge clk) hold[*1:WR_PARAM] ##1 (1, v_data =data, v_address=address) ##1 mem[v_address]==v_data; endproperty : p_write ap_write: assert property(p_write); //.. endmodule : dut_mem module top_tb; logic clk =1'b0, rd, wr, rst_n; logic [31:0] address, data1; logic hold; bit go; wire [31:0] data; dut_mem #(.RD_PARAM (0), .WR_PARAM(0), .MEM_DEPTH_PARAM(16)) dut_mem0 (.*); //.. endmodule The fix to conform to 201 because a[*1:0] is illegal: generate if(RD_PARAM > 0) begin ap_readhold: assert property(@ (negedge clk) rd && hold==1'b0 |-> @ (posedge clk) hold[*1:RD_PARAM] ##1 data==mem[address]); property p_write; logic[31:0] v_data, v_address; @ (negedge clk) (wr && hold==1'b0, v_data=data, v_address=address) |-> @ (posedge clk) hold[*1:WR_PARAM] ##1 (1, v_data =data, v_address=address) ##1 mem[v_address]==v_data; endproperty : p_write ap_write: assert property(p_write); end else begin ap_readhold: assert property(@ (negedge clk) rd && hold==1'b0 |-> @ (posedge clk) data==mem[address]); property p_write; logic[31:0] v_data, v_address; @ (negedge clk) (wr && hold==1'b0, v_data=data, v_address=address) |-> @ (posedge clk) (1, v_data =data, v_address=address) ##1 mem[v_address]==v_data; endproperty : p_write ap_write: assert property(p_write); end endgenerate Ben Cohen when the RD_PARAM== 0, or the WR_PARAM== 0 then the hold[*1:RD_PARAM] or the hold[*1:WR_PARAM] would obviously not compile. The fix: Use of the generate with the if(RD_PARAM > 0) --------------------------------------------------------------------- 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. --------------------------------------------------------------------- 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 Tue May 7 22:27:13 2013
This archive was generated by hypermail 2.1.8 : Tue May 07 2013 - 22:27:24 PDT