N unique stable data vectors

Hi Ross,

I don't have an answer to the question of repeating N-Times the unique constraint, but other remarks:

1) stable(stable_data))@(posedge clk) is only guaranteeing stability if the design is purely synchronous to the posedge, otherwise there may be arbitrary values at the clock high phase.

2) The unique vector set is a subset of the generic vector set. IFV will apply any vector set to FAIL an assertion, including the one with unique vectors, I don't really see a need to restrict it to the unique set. Potential reason might be

a) you don't like this CEX
b) you need it for a coverage trace
c) this is really a conatraint of the system and causes a false failure in an assertion

Can you elaborat eon your motivation for this conatraints?

Thanks,
Joerg.

Hi Joerg,

A couple uses may be as follows:

There are N requestors to a design and each requestor needs to be restricted such that none of the requestors make requests to the same address.  With a solution to this question I could set up address range limitations for each requestor.

A design needs N requestors to have unique requestor IDs.


Below is something I've come up with (I haven't tried it):

...
localparam W=4,N=8;
wire [W-1:0] stable_data [N-1:0]
genvar gi;
generate for (gi=0;gi
  if(gi==0) begin
    gt_last #(.W(W)) data(
      .clk(clk),
      .min({W{1'b0}}),
      .stable_data(stable_data[gi])
    );
  end else begin
    gt_last #(.W(W)) data(
      .clk(clk),
      .min(stable_data[gi-1]+{{W-1{1'b0}},1'b1}), // Next min 1 greater than last
      .stable_data(stable_data[gi])
    );
  end
end endgenerate
...

module gt_last
#(W=3)
(
input clk,
input [W-1:0] min,
output [W-1:0] stable_data
);

//psl assume_stable_data_ge_min: assume always(
//  stable_data>=min & stable(stable_data)
//)@(posedge clk);

endmodule

Thanks,

Ross

Below is a more elegant (and better) solution than what I posted above.

I just used some verilog to determine when the data slices were equal and wrote an assumption to prevent the signal from ever becoming true.  I also added a stable assumption that is only needed if you want the data to be stable throughout a sequence.

module unique_stable_data
#(
parameter
N=4,
DATA_W=5
)
(
input clk,
input [(N*DATA_W)-1:0] data
);

reg data_eq;
integer i,j;
always @* begin
  data_eq=1'b0;
  for(i=0;i < N-1;i=i+1) begin
    for(j=i+1;j < N;j=j+1) begin
      data_eq = data_eq | (data[i*DATA_W+:DATA_W]==data[j*DATA_W+:DATA_W]);
    end
  end
end

//psl assume_data_ne: assume never(data_eq)@(posedge clk);


// If the data needs to be stable
//psl assume_stable_data: assume always(
//  stable(data)
//)@(posedge clk);

endmodule