Check the transcation

SystemVerilog
1

Hi All,
I want to use SVA to check the behavior of ID.
For example: ck0, receive ID=10, ck1, receive ID=5, ck2, receive ID=10. it is illegal case.
ck0, receive ID=10, ck1, receive ID=5, ck2, receive ID=5. it is legal case.
I want to check the transaction with different ID can not appear in clk1.
How to check it using SVA?
Thanks a lot!!

2

I’m not sure if I understood your problem correctly. But it seems this is not a task for SVA. Because SVA is used for checking temporal behavior of several signals.
Back to your problem:
what is ck=, ck1, etc.
what is ID is it a data member of a sequence_item?

3

Your question is not clear. What is the timing relationship between ck1, ck2, and ck3? If they are not synchronous, how do you establish a relationship between them? It’s also not clear which cases are legal or illegal. You should make a test stimulus that shows us the two cases.

4

I believe that your question is:

  1. I have a stream of IDs arriving in different registers each clocked with different clocks.
  2. The stream has a particular signature; for example:
    ID==10 clocked with ck0 should arrive first,
    ID==5 clocked with ck1 is next in time,
    ID==5 clocked with ck2 is third.
    Any other sequence pattern is in error.
  3. The 2nd ID shouldnot be the same as the 1st ID.
    The 3rd ID should be the same as the 2nd ID
  4. There are many IDs clocked by CK1 that are illegal.
    NOTE: What is poorly specificed is:
    a)When is the start of IDs checked?
    [Ben] I’ll assume a “go” trigger computed with support logic.
    b) Is it just a sequence of 3 IDS?
    c) What are the many IDs clocked by CK1 that are illegal.
bit go, ck0, ck1, ck2; 
int id[0:2]; 
property p_id; 
  int v[0:1];
  @(posedge ck0) (go, v[0]=id[0]) |->  
       @(posedge ck1) (v[0] != id[1], v[1]=id[1]) ##0 
       @(posedge ck2) (v[1] != id[2]);
endproperty; 
ap_id: assert property(p_id);

Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.

5

sorry, only one clk in this problem. actually, my problem is like this.
I have a stream of same ID arriving first, and then another ID arriving next.
for example: ID=0,ID=0,ID=0,ID=0(last=1),ID=2,ID=2,ID=2,ID=2,(last=1)
I want to make sure there are no other ID between ID=0 .
for example :ID=0,ID=5,ID=5,ID=0,(last=1),ID=2,ID=2,ID=2,ID=2,(last=1)
In this example , ID=5 is illegal, because ID=0 not finish the transaction. I suppose ID should be 0 instead of 5. how to use SVA to check it?
Thank you

6

That clears up a few things. ck0, c1, and ck2 were ordered clock cycle sof the same clock, not different clocks. But now you have introduce a new signal last. You could save people a lot of time by writing a small, simple verilog code declaring all the signals you need with some stimulus that we could test it with.

Maybe what you want is

property p_id; 
  @(posedge clk) $past(last) ==0 |-> $stable(ID);
endproperty; 
ap_id: assert property(p_id);