Verification of Register Transfer Level Parallel Control Sequences

Author

Pitchumani, Vijay ; Stabler, Edward P.

Author_Institution

Department of Electrical and Computer Engineering, Syracuse University

Issue

8

fYear

1985

Firstpage

761

Lastpage

765

Abstract

This correspondence presents a method for proof of correctness of register transfer level (RTL) parallel control sequences that describe hardware behavior. An RTL language endowed with parallel constructs is presented and its semantics is defined. The semantics includes temporal behavior. An assertion-based proof method is presented for verification of parallel control sequences described in this language. An example is given and comparisons are drawn between proofs of parallel register transfer level sequences and parallel programs. The temporal semantics associated with the language permits the construction and proof of parallel sequences that are not possible with parallel programs. Accessing shared resources outside critical regions is possible and is illustrated.

Keywords

Assertion; auxiliary variable; clock cycle; critical region; parallel control sequence; register transfer level; shared resource; verification condition; Added delay; Computer errors; Condition monitoring; Delay effects; Feedback circuits; Feedback loop; Input variables; Registers; Sequential circuits; Signal design; Assertion; auxiliary variable; clock cycle; critical region; parallel control sequence; register transfer level; shared resource; verification condition;

fLanguage

English

Journal_Title

Computers, IEEE Transactions on

Publisher

ieee

ISSN

0018-9340

Type

jour

DOI

10.1109/TC.1985.1676625

Filename

1676625