Most STGs should satisfy the following properties (can be checked via Verification menu):
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.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) )
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.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.Most speed-independent circuits should satisfy the following properties (can be checked via Verification menu):
z+
, a transition labelled by z+
must be enabled in the environment STG.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.
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.