Cited By
View all- Wilsey P(1992)Developing a Formal Semantic Definition of VHDLVHDL for Simulation, Synthesis and Formal Proofs of Hardware10.1007/978-1-4615-3562-1_17(245-256)Online publication date: 1992
NES: the behavioral model for the formal semantics of a hardware design language UDL/I
Pages 8 - 13
Abstract
This paper describes a new behavioral model of hardware, named NES (Nondeterministic Event Sequence) model, which was developed for the purpose of defining formal semantics of the gate level and the register transfer level hardware description languages. The NES model is a generalization of the event driven simulation, and can be a basis of synthesis and verification as well as simulation. We introduce basic concepts, formal definition, and a description method of the NES model.
References
[1]
O. Karatsu: "VLSI Desiga Language Sta.adardization Effort in Japan ", Proc. 26th DAC, pp. 50-55, (1989).
[2]
H. Yasuura and N. Ishiura: "Semantics of a Hardware Design Language for Japanese Standardization, Proc. 26th DAC, pp. 836-839, (1989).
[3]
R. Piloty, M. Barbacci, D. Borrione, D. Dietmeyer, F. Hill and P. Skelly, "CONLAN Report", Lecture Notes in Computer Science 151, Springer-Verlag, (1983).
[4]
David R. Coelho: "The VHDL Handbook", Kluwer Academic Publishers, (1989).
[5]
R. W. Hertenstein, R. Hauck, K. Lemmert and A. Wodtko: KARL-III Manual, report AG Hartenstein, Kaiserslautern University, (1986).
[6]
D. Bjcrrter and C. B. Jones: The Vienna Development Method: The Meta Language, Lecture Notes in Computer Science 61, Springer-Verlag, (1978).
[7]
J. L. Carter, B. K. Rosen, G. L. Smith aatd V. Pichumani: "Restricted Symbolic Evaluation is Fast and Useful", Proc. ICCAD-89, pp. 38-41, (1989).
[8]
N. Ishiura, Y. Deguchi and S. Yajima: "Coded Time-Symbolic Simulation Using Shared Binary Decision Diagram", Proc. 27th DAC, (1990).
Index Terms
- NES: the behavioral model for the formal semantics of a hardware design language UDL/I
Recommendations
A Formal Framework for ASTRAL Intralevel Proof Obligations
ASTRAL is a formal specification language for real-time systems. It is intended to support formal software development, and therefore has been formally defined. This paper focuses on how to formally prove the mathematical correctness of ASTRAL ...
Faithfully formalizing OSEK/VDX operating system specification
SoICT '12: Proceedings of the 3rd Symposium on Information and Communication TechnologyOSEK/VDX has proposed a standard for operating systems used in automotive systems. This standard is described in the form of informal specification. The informal specification is not suitable for applying formal methods to the whole of the software ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
Copyright © 1991 ACM.
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]
Sponsors
- SIGDA: ACM Special Interest Group on Design Automation
- IEEE-CS: Computer Society
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 03 January 1991
Check for updates
Qualifiers
- Article
Conference
DAC90
Sponsor:
- SIGDA
- IEEE-CS
Acceptance Rates
DAC '90 Paper Acceptance Rate 125 of 427 submissions, 29%;
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
- 249Total Downloads
- Downloads (Last 12 months)69
- Downloads (Last 6 weeks)10
Reflects downloads up to 17 Dec 2024
Other Metrics
Citations
Cited By
View all- Wilsey P(1992)Developing a Formal Semantic Definition of VHDLVHDL for Simulation, Synthesis and Formal Proofs of Hardware10.1007/978-1-4615-3562-1_17(245-256)Online publication date: 1992
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in