A verifier for network decompositions of command-based specifications

Author

Ebergen, Jo C. ; Gingras, Sylvain

Author_Institution

Dept. of Comput. Sci., Waterloo Univ., Ont., Canada

fYear

1993

Firstpage

310

Abstract

An automatic verifier for speed-independent circuits is discussed. All specifications of components are given in a CSP-like notation called commands. Specifications are implemented by networks of components. Implementations can be verified against four correctness criteria: two structural conditions for the network, one safety condition, and a progress condition. The main advantages of the verifier include the use of commands as a specification language, the verification of a progress condition, and the possible avoidance of state explosion by means of two structured verification methods: stepwise verification and partwise verification. The verifier is illustrated by means of some examples.

Keywords

asynchronous sequential logic; communicating sequential processes; logic design; logic testing; CSP-like notation; asynchronous circuits; command-based specifications; commands; network decompositions; partwise verification; progress condition; specification language; speed-independent circuits; state explosion; stepwise verification; verification; Circuit analysis; Circuits; Computer science; Councils; Error correction; Explosions; Information technology; Safety; Specification languages; System recovery; User interfaces;

fLanguage

English

Publisher

ieee

Conference_Titel

System Sciences, 1993, Proceeding of the Twenty-Sixth Hawaii International Conference on

Print_ISBN

0-8186-3230-5

Type

conf

DOI

10.1109/HICSS.1993.270634

Filename

270634