Most STGs should satisfy the following four properties (can be checked via Verification menu):
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.
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.
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.
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.