Most STGs should satisfy the following properties (can be checked via Verification menu):
Mutex place implementability – surrounding signals of an arbitrating choice place that is tagged as a mutex must follow the MUTEX protocol. (In this case the place can be implemented by a MUTEX that can correctly handle the metastable behaviour associated with arbitration.) Essentially, Worckcraft looks at the transitions around a mutex place, and tries to work out which signals are the grants and which signals are the requests. Then it tries to verify whether the grants can be correctly implemented by a mutex taking the requests (and no other signals!) as inputs. E.g. suppose the tool speculates that the requests are r1 and r2 and the grants are g1 and g2. Then it formally verifies the following properties, where ⇒ is logic implication and
nxt is the next-state function of a signal, i.e.
nxt(g1) = g1 xor enabled(g1):
// if r1 is high and g2 is low than g1 is either
// already high or enabled to become high
r1&~g2 ⇒ nxt(g1)
// if r1 is low then g1 is either low or enabled to become low
~r1 ⇒ ~nxt(g1)
// if r2 and g2 are high then g1 is either low or
// enabled to become low - note that this allows
// for both early-release and late-release protocols
r2&g2 ⇒ ~nxt(g1)
// the symmetric properties for nxt(g2):
r2&~g1 ⇒ nxt(g2)
~r2 ⇒ ~nxt(g2)
r1&g1 ⇒ ~nxt(g2)
// the mutual exclusion of the critical sections
~( (r1&g1) & (r2&g2) )
Output persistency – a local (i.e. output or internal) signal must not be disabled by any other signal (such disabling would cause a hazard on the output of the gate producing this local signal). This property can currently be verified only for STGs without dummy transitions. The notable exceptions are MUTEX and WAIT – they violate output persistency. It is possible to model them by “factoring out” them into the environment, turning these violations into input/input conflicts which are ok; however, the preferred way in Workcraft is to use Mutex places, see below.
– The STG
is not self-contradictory. This property trivially holds for deterministic STGs (i.e. ones without dummies and without choices between transitions labelled by the same signal). However, for non-deterministic STGs it is possible to execute the same trace (sequence of signal edges)
in two different ways, reaching two different markings. If one of these markings enables some output
and the other does not, there is a contradiction: The STG
simultaneously requires the circuit to produce
, and forbids to do so.
Delay insensitive interface
– If in some reachable marking the STG
can fire one input transition after another, then it should be possible to fire these inputs in the reverse order as well, i.e. these inputs should be concurrent. Intuitively, such inputs can be reordered without breaking the circuit.
Normalcy – This property ensures that it is possible to implement each local signal by a gate without input ‘bubbles’, i.e. by a (perhaps negated) monotonic Boolean function. This condition in particular implies CSC. This property is mostly of theoretical interest, it is often violated in practice.
Redundancy of selected places
– Check if the selected places can be removed without changing the behaviour of the STG
N-way conformation – If several STGs sharing signals represent a decomposition of a system into components, this property ensures that no component can produce an output that another component (that has it as an input) does not expect. In other words, if there is a reachable state in the overall system where some component can fire a transition labelled by some output
o, but some other component that has this signal as an input
o does not enable any transition labelled by
o then this property is violated.
helps to formulate and verify the properties of handshake protocol, as explained in Handshakes Verification
– The user can specify custom properties using REACH language
. For example, a custom property that PMOS and NMOS are never ON at the same time is specified and verified in buck tutorial
Most speed-independent circuits should satisfy the following properties (can be checked via Verification menu):
– the circuit will never break the environment by sending an output that the environment does not expect. In other words, if a circuit produces an output, say
, a transition labelled by
must be enabled in the environment STG
Note that circuits must be verified with the STG modelling the environment, and during verification it is assumed that the environment fulfils its contract specified by this STG.
Again, non-persistency in MUTEX and WAIT have to be handled specially – in Workcraft there is a gate property allowing to treat a gate as a part of the environment.
These properties are rather weak – e.g. a circuit accepting all inputs and not producing any outputs conforms to any specification with the same signals! They do not constitute transcendental “correctness” – there is no such thing. So set your expectations accordingly – a circuit that passes all these verification checks can still be very wrong.