DocumentCode
2561086
Title
Distinguishing formulas for free
Author
Margaria, Tiziana ; Steffen, Bernhard
Author_Institution
Lehrstuhl fuer Inf. II, RWTH Aachen, Germany
fYear
1993
fDate
22-25 Feb 1993
Firstpage
105
Lastpage
110
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;
fLanguage
English
Publisher
ieee
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
Type
conf
DOI
10.1109/EDAC.1993.386492
Filename
386492
Link To Document