A system for the efficient verification of the input/outputncorrectness of finite state machines with data path and control unit isnpresented. This system, which is based on First-Order Logic theoremnproving, automatically provides distinguishing formulas expressing allntest patterns that witness a behavioral difference between twondescriptions. Experimental results illustrate the test patternngeneration feature for stuck-at faults, functional faults, andninitialization faults, and the efficiency which results from thencompositionality of the verification
展开▼
