Formal Boolean manipulations for the verification of sequential machines

The paper addresses the problem of verifying synchronous sequential machines. It first shows that there is a certain class of temporal properties that can be verified by proving two sequential machines equivalent. It then explains that the equivalence of two sequential machines can be checked without building any state diagram. It is sufficient to observe all the valid states of a machine, which can be done by traversing its state diagram. It finally presents the symbolic manipulation used to perform the traversal of a state diagram in a more efficient way than the usual traversal technique based on enumeration