When I was reading the checker section of LRM, I came across the following passage:
“Empty assume sets shall be considered to have an implicit assume set clock event in every time step before
the Observed region. Active variables in checkers with empty assume sets are called implicitly clocked
active free variables; those with nonempty assume sets are explicitly clocked. Implicitly clocked active
variables may be updated with unconstrained random values at every time step. Once updated, the variables
stay constant until the end of the time step
Active variables that do not appear in any property in a nonempty assume set are unconstrained but
explicitly clocked. They may be updated with random values at every assume set clock event.”
There are three points that I do not understand:
- What is an empty assume? Can you give an example?
- Whether an assume set has the same clock event?
- If answer for 2 is no, then how to decide which clock event to use for active variables that do not appear in any property in a nonempty assume set