5

I have some data from a 1 bit serial port which comes in multiples of bytes of variant lengths as such:

byte expected_1 [$] = {8'hBA, 8'hDD, 8'hC0, 8'hDE};
byte expected_2 [$] = {8'h01, 8'h23, 8'h45, 8'h67, 8'h89, 8'hAB, 8'hCD, 8'hEF};

At each positive clock edge, one bit is sent. I need to testbench hundereds of sequences ( maybe thousand in the future ) so I want to automate the process with assertions in system verilog. The new 2012 standard allows for queues to be passed to properties, but can the queues be sent though a recursive property? I received some error about hierarchical ref.

This is what I have so far (with help from @Greg here): 

default clocking sck @(posedge sck); endclocking : sck  

sequence seq_serial(logic signal, logic [7:0] expected); // check each bit
  byte idx = 7;
  (signal == expected[idx], idx--)[*8];
endsequence : seq_serial

property recurring_queue(bit en, logic data, byte data_e [$])
  int queue_size = data_e.size;
  logic [7:0] expected = data_e.pop_front(); 

  if(queue_size != 0) (
    !en throughout (seq_serial(data, expected) ##1 recurring_queue(en, data, data_e))
  );

endproperty : recurring_queue

`define ez_assert(exp)
   assert property (recurring_queue(en, data, exp))
   else $error("Bad Sequence @ time: %t. Info: %m", $time);

Calling the assertion in my testbench should be as easy as this:

A1 : `ez_assert(expected_1);

The error messages read: 

1) passing hierarchical ref to be used in another hierarchical ref is not supported 
2) Illegal SVA property in RHS of'##' expression 
3) Local variable queue_size referenced in expression before getting initialized

I'm open to other ideas for asserting long variable-length serial sequences.

Community
  • 1
  • 1
N8TRO
  • 3,348
  • 3
  • 22
  • 40
  • these error messages would be easier to follow if added to the end of the question. – Morgan Jun 17 '13 at 15:28
  • 1
    Small errors need to be cleaned up before getting to the real problem. Assignment to a whole queue needs a single quote before the curly bracket (e.g. `q[$]='{...};`). Multi-line macro needs a backslash ('\') at the end of each line except the final line. Are sure passing a queue to a property is supported by your simulator? – Greg Jun 17 '13 at 18:27
  • 1
    I need to correct myself for the single quote for full queue assignment. Queues are apparently the exception as there are clear examples in [IEEE Std 1800-2012](http://standards.ieee.org/getieee/1800/download/1800-2012.pdf) section 7.10 Queues, but is allowed (10.10.3). Structure literals (5.10), array literals (5.10), unpacked arrays (7.4), dynamic arrays (7.5), and associative arrays(7.8) use `'{` for full assignments. – Greg Jun 17 '13 at 21:47

1 Answers1

1

Try the same strategy as seq_serial:

sequence seq_queue_pattern(bit en, logic data, byte expt_queue [$]);
    int qidx = 0;
    ( !en throughout (seq_serial(data,expt_queue[qidx]), qidx++)[*] )
    ##1 (qidx==expt_queue.size);
endsequence : seq_queue_pattern

asrt_expected_1 : assert property ( $fell(en) |-> seq_queue_pattern(en,data,expected_1));
asrt_expected_2 : assert property ( $fell(en) |-> seq_queue_pattern(en,data,expected_2));

This assertion will fail if en is high or the seq_serial chain does not match expected. Do not that parenthicy location matters:

  • en is don't care one clock after final seq_serial completes:
    • ( !en throughout (seq_serial(data,expt_queue[qidx]), qidx++)[*] ) ##1 (qidx==expt_queue.size)
  • en must be low one clock after final seq_serial completes or failes and don't care after that
    • !en throughout ( (seq_serial(data,expt_queue[qidx]), qidx++)[*] ##1 (qidx==expt_queue.size) )
  • en must be low one clock after final seq_serial completes and don't care after that
    • !en throughout ( (seq_serial(data,expt_queue[qidx]), qidx++)[*] ##1 (qidx==expt_queue.size) ) ##1 (qidx==expt_queue.size)

Queues within sequences and properties are new and may not be fully supported by all simulators yet. To work around this limitation, use a parametrized macro to create a sequence for each expected queue stream:

`define asrt_qpat(en,monitor, expt_queue) \
    sequence seq_queue_pattern__``expt_queue (bit en, logic data); \
        int qidx = 0; \
        (!en throughout (seq_serial(data,expt_queue[qidx]), qidx++)[*]) \
        ##1 (qidx==expt_queue.size); \
    endsequence : seq_queue_pattern__``expt_queue \
    \
    asrt_``expt_queue : assert property( @(posedge clk) \
        $fell(en) |=> seq_queue_pattern__``expt_queue (en,monitor) ) \
    else $error("Bad Sequence @ time: %t. Info: %m", $time);

`asrt_qpat(en,data[0],expected_1)
`asrt_qpat(en,data[1],expected_2)
Greg
  • 18,111
  • 5
  • 46
  • 68
  • I have it up and running but by a different route.. I ended up having to use fork-join and give the number of bytes to expect. (Something about unbounded range) I'll give you're method a try when I get a chance. Thanks for the great answers. – N8TRO Jun 17 '13 at 23:08
  • I'm curious to see your approach. How does a fork-join help? – Greg Jun 18 '13 at 00:20
  • Fork-join ended up not helping.. Your code almost works, but it is 1 byte offset (assert checks 1 byte late) – N8TRO Jun 18 '13 at 17:16
  • You mean one bit late? Change `|=>` to `|->` if that is the case. – Greg Jun 18 '13 at 17:30
  • Sorry, the assertion starts at the correct time, but fails 1 byte later.. Could it be `(seq_ser(..),qidx++)[*] ##1 (qidx==expt_queue.size)` The message says that qidx = 0 at the time of the failure. I've never seen `[*]` by itself.. How does that work? – N8TRO Jun 18 '13 at 17:58
  • `[*]` is short for `[*0:$]` (zero to infinite) [IEEE Std 1800-2012](http://standards.ieee.org/getieee/1800/download/1800-2012.pdf) 16.9.2. It might be your test vector. Are you putting gaps between bytes? I'm using `en<=1;fork ##1 cb.en<=0; foreach(expected_1[i,j]) ##1 cb.data[0]<=expected_1[i][j]; foreach(expected_2[i,j]) ##1 cb.data[1] <= expected_2[i][j]; join` Can you share your test-bench code or provide a waveform? – Greg Jun 18 '13 at 18:51
  • let us [continue this discussion in chat](http://chat.stackoverflow.com/rooms/31967/discussion-between-nathan-g-and-greg) – N8TRO Jun 18 '13 at 19:35