[sv-ac] RE: [SV-AC] Should a[*1:0] be interpreted as a[*0]? // 16.7 Sequences

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<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.

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