Assumptions for pipeline DUT

SystemVerilog
, ,
1

hi all,
I’m writing SVA for formal verification environment. the DUT is an arbiter with a pipeline behavior.
In order to describe the pipeline, I used a simple always block sampling the inputs and updating a “status” signal for each request, if the inputs are received out of order, then “status=4”, like so:


always (posedge clk)
...
if (in1)
  if(status==0)
    status=status+1;
  else
    status=4;
if (in2)
  if(status==1)
    status=status+1;
  else
    status=4;
...
...

and the property (status shall not be ‘4’=inputs should be only in the expected order):


assume property (status!=4);

this assumption fails, with the following message:
“concurrent or Immediate assertions can not include another concurrent assertion”

my question is:

  1. what does this error mean?
  2. is there a different way to design properties for pipeline modules?

thanks!

2

In reply to gidon:
Your error message maybe caused by the blocking assignment of status and the concurrent assertion (the assume) that uses a sampling of the status at the clk edge. Try the following instead:


always (posedge clk) begin 
  static int status;  //  Local to the always
  ...
  if (in1)
    if(status==0)  status=status+1;
    else status=4;
  if (in2) if(status==1) status=status+1;
  else status=4;
  ...
  ...    
  assume (status!=4);
end

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr

See Paper: VF Horizons:PAPER: SVA Alternative for Complex Assertions | Verification Academy