Hi Ben,
the book says the FV tools in their internal implementation eliminate the intersect operator and generate all the possible combinations of events. One of the exercises given in the book is as follows :
- Write the following property without Intersect operator:
a1: assert property (
command |-> write_cmpl [-> 1] intersect read_cmpl [-> 2]);
Now with goto repetition operator, at the last clock tick one read_cmpl and one write_cmpl (the only one) should happen at the same time. (read_cmpl && write_cmpl). Considering all combinations of remaining events, (one read_cmpl, !read_cmpl, !write_cmpl), we need to consider all following possibilities.
- read_cmpl && !write_cmpl followed by some indefinite number ([*0:$]) of !read_cmpl && !write_cmpl followed by read_cmpl && write_cmpl;
or
- indefinite number of times ([*0:])!write_cmpl&& !read_cmpl, followed by read_cmpl && !write_cmpl followed by indefinite number of times ([*0:])!write_cmpl&& !read_cmpl, followed by read_cmpl && write_cmpl;
If we combine sequence 1 and 2 above using OR operator shall we get the logic described in property a1 that is - write_cmpl [-> 1] intersect read_cmpl [-> 2]?
Can the similar approach be followed for my earlier question given below if we need to re-write it without intersect operator ?
assert property (sop |-> read [=2] intersect write [=3] intersect eop [-> 1]);
rgs,
-sunil