Stats

  • Locked Locked
  • Replies 3
  • Subscribers 64
  • Views 13661
  • Members are here 0
This discussion has been locked.
You can no longer post new replies to this discussion. If you have a question you can start a new discussion

N unique stable data vectors

archive

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
Parents

  • 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
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
Children
No Data

Community Guidelines

The Cadence Design Communities support Cadence users and technologists interacting to exchange ideas, news, technical information, and best practices to solve problems and get the most from Cadence technology. The community is open to everyone, and to provide the most value, we require participants to follow our Community Guidelines that facilitate a quality exchange of ideas and information. By accessing, contributing, using or downloading any materials from the site, you agree to be bound by the full Community Guidelines.