[sv-ac] [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)

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