Title :
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
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;
Conference_Titel :
System Sciences, 1993, Proceeding of the Twenty-Sixth Hawaii International Conference on
Print_ISBN :
0-8186-3230-5
DOI :
10.1109/HICSS.1993.270634
