Verification of Register Transfer Level Parallel Control Sequences
- 1 August 1985
- journal article
- Published by Institute of Electrical and Electronics Engineers (IEEE) in IEEE Transactions on Computers
- Vol. C-34 (8), 761-765
- https://doi.org/10.1109/tc.1985.1676625
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
This publication has 8 references indexed in Scilit:
- An Inductive Assertion Method for Register Transfer Level Design VerificationIEEE Transactions on Computers, 1983
- An exercise in proving parallel programs correctCommunications of the ACM, 1977
- Formal verification of parallel programsCommunications of the ACM, 1976
- Verifying properties of parallel programsCommunications of the ACM, 1976
- A consistent and complete deductive system for the verification of parallel programsPublished by Association for Computing Machinery (ACM) ,1976
- An axiomatic proof technique for parallel programs IActa Informatica, 1976
- An axiomatic basis for computer programmingCommunications of the ACM, 1969
- Assigning meanings to programsPublished by American Mathematical Society (AMS) ,1967