Cited By
View all- Berthet CCerny E(2019)An Algebraic Model for Asynchronous Circuits VerificationIEEE Transactions on Computers10.1109/12.222937:7(835-847)Online publication date: 4-Jan-2019
A model for hardware description and verification
Abstract
Integrated circuit verification is required to establish the correctness of a circuit design before fabrication. This paper proposes CIRCAL as a model in which to describe the behaviour of devices in a natural, concise and accurate manner. CIRCAL supports a number of verification techniques which allow for the formal analysis of circuit behaviour. Properties of the model are outlined while simulation and proof techniques using CIRCAL are presented.
References
[1]
Gordon, M., A very simple model of sequential behaviour of nMOS, Proc. VLSI '81, Edinburgh (Academic Press, New York, 1981).
[2]
Gordon, M., Proving a computer correct, Rept.42, Computer Laboratory, University of Cambridge, 1983.
[3]
Hayes, J., A unified switching theory with applications to VLSI design, Proc. IEEE 70, Oct. 1982.
[4]
Hoare, C.A.R., Communicating sequential processes, Comm. ACM 21 (8)(1978).
[5]
Mead, C. and Conway, L., Introduction to VLSI Systems (Addison-Wesley, Reading, MA, 1980).
[6]
Milne, G., The representation of communication and concurrency, Rept. 4088, Dept. of Computer Science, California Institute of Technology, 1980.
[7]
Milne, G., Abstraction and nondeterminism in concurrent systems, Proc. 3rd Internat. Conf. on Distributed Systems, Florida (IEEE Computer Society Press, 1982).
[8]
Milne, G., The correctness of a simple silicon compiler, Proc. 6th Internat. Symp. on Computer Hardware Description Languages and their Applications, Pittsburgh (North-Holland, Amsterdam, 1983).
[9]
Milne, G., A formal basis for the analysis of circuit timing, Rept. CSR-138-83, Dept. of Computer Science, University of Edinburgh, 1983.
[10]
Milne, G., CIRCAL: a calculus for circuit description, INTEGRATION 1, Nos 2 and 3, 1983.
[11]
Milne, G., CIRCAL and the representation of communication, concurrency and time, Rept. CSR-151-83, Dept. of Computer Science, University of Edinburgh, 1983.
[12]
Milner, R., A calculus of communicating systems, Lecture Notes in Computer Science 92 (Springer, Berlin, 1980).
[13]
Traub, N., A Lisp based CIRCAL environment, Rept. CSR-152-83, Dept. of Computer Science, University of Edinburgh, 1983.
Index Terms
- A model for hardware description and verification
Recommendations
Formal verification in hardware design: a survey
In recent years, formal methods have emerged as an alternative approach to ensuring the quality and correctness of hardware designs, overcoming some of the limitations of traditional validation techniques such as simulation and testing.
There are two ...
The Formal Description and Verification of Hardware Timing
A formalism in which timing properties of digital hardware may be specified, derived, and formally verified is introduced as a rigorous theory for hardware timing. A rigorous modeling framework has been used to create a family of related verification ...
Model checking for ACL compliance verification
AAMAS '03: Proceedings of the second international joint conference on Autonomous agents and multiagent systemsThe problem of checking that agents correctly implement the semantics of an agent communication language has become increasingly important as agent technology makes its transition from the research laboratory to field-tested applications. In this paper, ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
June 1984
715 pages
ISBN:0818605421
Sponsors
- SIGDA: ACM Special Interest Group on Design Automation
- IEEE: Institute of Electrical and Electronics Engineers
- IEEE-CS: Computer Society
Publisher
IEEE Press
Publication History
Published: 25 June 1984
Check for updates
Qualifiers
- Article
Acceptance Rates
DAC '84 Paper Acceptance Rate 116 of 290 submissions, 40%;
Overall Acceptance Rate 1,770 of 5,499 submissions, 32%
Upcoming Conference
DAC '25
- Sponsor:
- sigda
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- View Citations1Total Citations
- 129Total Downloads
- Downloads (Last 12 months)9
- Downloads (Last 6 weeks)1
Reflects downloads up to 26 Sep 2024
Other Metrics
Citations
Cited By
View all- Berthet CCerny E(2019)An Algebraic Model for Asynchronous Circuits VerificationIEEE Transactions on Computers10.1109/12.222937:7(835-847)Online publication date: 4-Jan-2019
View Options
Get Access
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in