[sv-ac] 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> 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] *On Behalf Of *Bresticker,
> Shalom
> *Sent:* Tuesday, May 07, 2013 7:55 AM
> *To:* hdlcohen@gmail.com; sv-ac@eda-stds.org; Korchemny, Dmitry; Eduard
> Cerny; 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]
> *Sent:* Saturday, March 09, 2013 20:34
> *To:* sv-ac@eda-stds.org; Korchemny, Dmitry; Eduard Cerny; Bresticker,
> Shalom; 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* 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.*
>
>
>
> 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.
>

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.