User Tools

Site Tools


help:verification

Verification properties

STG properties

Most STGs should satisfy the following four 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.
  • Output persistency – a local 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.

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.

Circuit properties

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 – 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. This is essentially output persistency.

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.