Question on system verilog " property"

Hello,
following is the excerpt from a book on Formal verification which I am reading:
“Let π = ν0, ν1, . . . denote a run, and πk = νk, νk+1, . . . denote the part
of π starting from νk. We will use the notation π |= f to denote that the
property f holds on the run π.
Given a run π, we will also use the notation
νk |= f to denote πk |= f. In other words, a property is said to be true at
an intermediate state of the run iff the fragment of the run starting from
that state satisfies the property. The formal semantics of the basic temporal
operators are as follows:”
Referring to the statement in boldface : “We will use the notation π |= f to denote that the
property f holds on the run π.”, I am not clear about the meaning of “property holds on a run” (according to the book, run is a path or trace consisting of states followed in a statemachine during transitions). So can someone please explain with an example what is the meaning of property holding on a path of state machine. (I can understand property holding a clock or state)

thanks
sunil puranik

In reply to puranik.sunil@tcs.com:

(according to the book, run is a path or trace consisting of states followed in a state machine during transitions).
Consider an FSM with the following possible paths:

  1. RUN1: ST1 → if(cond_a) → ST2 → if(cond_b) ST3
  2. RUN2: ST1 → if(cond_c) → ST4 → ST5 → ST1

Here, I see 2 runs starting from ST1. I believe that this is intent here.
What is the name of the book and the author?
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr

** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448

  1. SVA Package: Dynamic and range delays and repeats SVA: Package for dynamic and range delays and repeats | Verification Academy
  2. Free books: Component Design by Example FREE BOOK: Component Design by Example … A Step-by-Step Process Using VHDL with UART as Vehicle | Verification Academy
    Real Chip Design and Verification Using Verilog and VHDL($3) Amazon.com
  3. Papers:

Hi Ben,
thanks for the reply. Book name is
“ARoadmap for Formal Property Verification by
PALLAB DASGUPTA
Indian Institute of Technology, Kharagpur, India”

I am still not clear what is meant by property holding on a path. Does it mean that property is satisfied on SOME subset of the states of a path or it needs to be satisfied by ALL the states of a path.
Consider the transition given by you above -
RUN2: ST1 → if(cond_c) → ST4 → ST5 → ST1

and property:
assert property ((@posedge clk)$rose (cond_c) => d);

assuming cond_c goes high in ST1 and d in ST4, does it mean the path given above satisfies the property and property holds on path. Or does it mean the property has to be satisfied on all states of a path?
regards,
-sunil puranik

In reply to puranik.sunil@tcs.com:
RUN2: ST1 → if(cond_c) → ST4 → ST5 → ST1
ap_condc2d: assert property ((@posedge clk)$rose(cond_c) => d && state==ST4);

Above property just take care of that one 2-cyle path.
YES on Assuming cond_c goes high in ST1 and d in ST4, does it mean the path given above satisfies the property and property holds on path.

NO *on Or does it mean the property has to be satisfied on all states of a path?
*
Obviously, ST4 → ST5 → ST1 is not covered by the assertion.

In reply to ben@SystemVerilog.us:

*In reply to
RUN2: ST1 → if(cond_c) → ST4 → ST5 → ST1
ap_condc2d: assert property ((@posedge clk)$rose(cond_c) => d && state==ST4);
NO [i]on Or does it mean the property has to be satisfied on all states of a path?

Obviously, ST4 → ST5 → ST1 is not covered by the assertion.

Hi Ben,
thanks for your reply. Just one question :
Why have you added (state == ST4) condition there? Anyways if cond_c is high, state machine will always land into ST4 from ST1.
regards,
-sunil

In reply to puranik.sunil@tcs.com:

Anyways if cond_c is high, state machine will always land into ST4 from ST1.

$rose(cond_c) => d && state==ST4) makes that (cond_c then ST4) a requirement to be verified. Maybe there is a path where $rose(cond_c) => d yet state!=ST4 in that cycle. As they say, all roads lead to Rome; there are many paths.
:)