This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Verification of Register Transfer Level Parallel Control Sequences
August 1985 (vol. 34 no. 8)
pp. 761-765
V. Pitchumani, Department of Electrical and Computer Engineering, Syracuse University
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.
Index Terms:
verification condition, Assertion, auxiliary variable, clock cycle, critical region, parallel control sequence, register transfer level, shared resource
Citation:
V. Pitchumani, E.P. Stabler, "Verification of Register Transfer Level Parallel Control Sequences," IEEE Transactions on Computers, vol. 34, no. 8, pp. 761-765, Aug. 1985, doi:10.1109/TC.1985.1676625
Usage of this product signifies your acceptance of the Terms of Use.