Title :
Distinguishing formulas for free
Author :
Margaria, Tiziana ; Steffen, Bernhard
Author_Institution :
Lehrstuhl fuer Inf. II, RWTH Aachen, Germany
Abstract :
A system for the efficient verification of the input/output correctness of finite state machines with data path and control unit is presented. This system, which is based on First-Order Logic theorem proving, automatically provides distinguishing formulas expressing all test patterns that witness a behavioral difference between two descriptions. Experimental results illustrate the test pattern generation feature for stuck-at faults, functional faults, and initialization faults, and the efficiency which results from the compositionality of the verification
Keywords :
fault diagnosis; finite state machines; formal verification; logic testing; theorem proving; First-Order Logic theorem proving; control unit; data path; efficient verification; finite state machines; functional faults; initialization faults; input/output correctness; stuck-at faults; test pattern generation; Automata; Automatic control; Automatic logic units; Circuit faults; Control systems; Hardware; Logic design; Logic testing; Registers; Test pattern generators;
Conference_Titel :
Design Automation, 1993, with the European Event in ASIC Design. Proceedings. [4th] European Conference on
Conference_Location :
Paris
Print_ISBN :
0-8186-3410-3
DOI :
10.1109/EDAC.1993.386492
