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