Towards verifiably correct VLSI design. (English) Zbl 0626.68042
Formal aspects of VLSI design, Proc. Workshop, Edinburgh/Scotl. 1985, 1-22 (1986).
[For the entire collection see Zbl 0607.00018.]
This paper presents a methodology for the verification of VLSI digital systems design. The hierarchical model, in which the description at the lower level may be abstracted to give a higher level description, is based on the dot calculus [see G. J. Milne, ACM Trans. Program. Lang. Syst. 7, 270-298 (1985; Zbl 0562.68017)]. The dot calculus is a term-rewriting system. The verification technique consists in proving that terms from the higher-level description are equivalent to those obtained after performing certain abstractions of the terms from the lower-level descriptions. The verification technique is illustrated by two examples - the model of a wire and a comparator circuit for two 8-bit buses.
This paper presents a methodology for the verification of VLSI digital systems design. The hierarchical model, in which the description at the lower level may be abstracted to give a higher level description, is based on the dot calculus [see G. J. Milne, ACM Trans. Program. Lang. Syst. 7, 270-298 (1985; Zbl 0562.68017)]. The dot calculus is a term-rewriting system. The verification technique consists in proving that terms from the higher-level description are equivalent to those obtained after performing certain abstractions of the terms from the lower-level descriptions. The verification technique is illustrated by two examples - the model of a wire and a comparator circuit for two 8-bit buses.
Reviewer: A.Michalski
