Home > Community > Forums > Functional Verification > N unique stable data vectors

Email

* Required Fields

Recipients email * (separate multiple addresses with commas)

Your name *

Your email *

Message *

Contact Us

* Required Fields
First Name *

Last Name *

Email *

Company / Institution *

Comments: *

 N unique stable data vectors 

Last post Sun, Mar 4 2007 3:34 PM by archive. 3 replies.
Started by archive 04 Mar 2007 03:34 PM. Topic has 3 replies and 1202 views
Page 1 of 1 (4 items)
Sort Posts:
  • Sun, Mar 4 2007 3:34 PM

    • archive
    • Top 75 Contributor
    • Joined on Fri, Jul 4 2008
    • Posts 88
    • Points 4,910
    N unique stable data vectors Reply

    Working off the concept that a property like the following causes a formal tool to try all values of the stable_data wire...

    wire [W-1:0] stable_data;
    //psl assume_stable_data: assume always(stable(stable_data))@(posedge clk);

    Is there a way to generate N stable_data vectors and at the same time guarantee that at any one time the data in them is unique.

    If I just wanted 2 vectors I might do something like the following:

    wire [W-1:0] stable_data0,stable_data1;
    //psl assume_stable_data0: assume always(stable(stable_data0))@(posedge clk);
    //psl assume_stable_data1: assume always(stable(stable_data1))@(posedge clk);

    //psl assume_unique_data: assume always(
    // stable_data0!=stable_data1
    //)@(posedge clk);

    Extending this to N vectors seems troublsome.  Any ideas?

    One might also ask how to fill a NxW array with unique stable data.

    Just for clarification, the fact that the data is stable isn't really a necessary component of this question.  I am mainly just wondering how I could easily generate N unique vectors of data.  It's just that data like this is usually stable in proofs.

    Thanks,

    Ross


    Originally posted in cdnusers.org by weberrm
    • Post Points: 0
  • Mon, Mar 5 2007 12:37 AM

    • archive
    • Top 75 Contributor
    • Joined on Fri, Jul 4 2008
    • Posts 88
    • Points 4,910
    RE: N unique stable data vectors Reply

    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.


    Originally posted in cdnusers.org by foster
    • Post Points: 0
  • Mon, Mar 5 2007 6:57 AM

    • archive
    • Top 75 Contributor
    • Joined on Fri, Jul 4 2008
    • Posts 88
    • Points 4,910
    RE: N unique stable data vectors Reply

    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


    Originally posted in cdnusers.org by weberrm
    • Post Points: 0
  • Fri, Mar 23 2007 8:01 AM

    • archive
    • Top 75 Contributor
    • Joined on Fri, Jul 4 2008
    • Posts 88
    • Points 4,910
    RE: N unique stable data vectors Reply

    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


    Originally posted in cdnusers.org by weberrm
    • Post Points: 0
Page 1 of 1 (4 items)
Sort Posts:
Started by archive at 04 Mar 2007 03:34 PM. Topic has 3 replies.