Property Specification Language: Difference between revisions

Revision as of 23:48, 6 January 2018

Revision as of 06:39, 6 February 2019

Line 197:

=== Sampling operator===

Sometimes it is desirable to change the definition of the ''next time-point'', for instance in multiply-clocked designs, or when a higher leverlevel of abstraction is desired. The ''sampling operator'' (a.k.a. ''the clock operator''), denoted {{mono|@}}, is used for this purpose. The formula {{mono| p @ c }} where {{mono| p}} is a PSL formula and {{mono|c}} a PSL Boolean expressions holds on a given path if {{mono| p}} on that path projected on the cycles in which {{mono| c}} holds, as exemplified in the figures to the right.

[[File:Need for multiple clocks.jpg|thumb|path and formula showing need for a sampling operator]]

Line 217:

{| class="wikitable"

| <code> p async_abort b </code>

| either p holds or p does not fail up until b holds, or p does not fail;

* b recognized asynchronously

|-

| <code> p sync_abort b </code>

| either p holds or p does not fail up until b holds, or p does not fail;

* b recognized synchronously

|-