Verification properties

Most STGs should satisfy the following properties (can be checked via Verification menu):

• Consistency – for all signals z, z+ and z- must alternate in each possible trace, always starting with the same sign. This is necessary for the encodings of the reachable states to be binary.

• Deadlock freeness – each reachable marking enables at least one transition.

• Input properness – an input must not be triggered by an internal signal (as the environment must be oblivious to internal signals) and must not be disabled by a local (i.e. output or internal) signal; it is ok (and in fact common) for an input to be disabled by another input. This property can currently be verified only for STGs without dummy transitions.

• 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 the Mutex place implementability property.

• Output determinacy – 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) w in two different ways, reaching two different markings. If one of these markings enables some output o and the other does not, there is a contradiction: The STG simultaneously requires the circuit to produce o after w, 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.

• Handshake wizard helps to formulate and verify the properties of handshake protocol, as explained in Handshakes Verification tutorial.

• Custom properties – 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):

• Conformation – 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 z+, a transition labelled by z+ must be enabled in the environment STG.

• Deadlock freeness – in every reachable state the circuit or the environment (or both) can fire some transition.

• Output persistency – an excited gate in the circuit cannot be disabled.

• Binate consensus – a gate implementing a binate Boolean function, i.e. a function depending on some variable x such that both x and ~x occur in its sum-of-products representation, does not glitch when x changes its value. More detail is provided here.

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.