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:
- what does this error mean?
- is there a different way to design properties for pipeline modules?
thanks!