Abstraction techniques for verification of multiple tightly coupled counters, registers and comparators

We present new non-deterministic finite state machine (NFSM) abstraction techniques for comparators based on the comparison difference of the two operands (e.g., counters) instead of the comparison order. One of the major advantages of the comparison difference abstractions is the ability to model the comparison of multiple tightly coupled computers. The abstraction techniques are integral to our semantic model abstraction methodology, where abstract models are generated based on semantic matching of behavioral VHDL models with known abstraction templates. Using NFSM models for counters, comparators, and registers, we have shown our approach can yield many orders of magnitude (10²-10¹¹) reductions in state space size and substantial improvements in performance of formal verification runs