hh.sePublications
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Formal analysis of non-determinism in Verilog cell library simulation models
Department of Computer Science, TU Eindhoven, P.O. Box 513, Eindhoven, The Netherlands.
Department of Computer Science, TU Eindhoven, P.O. Box 513, Eindhoven, The Netherlands.ORCID iD: 0000-0002-4869-6794
Fenix Design Automation, P.O. Box 920, Eindhoven, The Netherlands.
Fenix Design Automation, P.O. Box 920, Eindhoven, The Netherlands.
Show others and affiliations
2009 (English)In: Formal Methods for Industrial Critical Systems: 14th International Workshop, FMICS 2009, Eindhoven, The Netherlands, November 2-3, 2009. Proceedings / [ed] MarĂ­a Alpuente, Byron Cook, Christophe Joubert, Berlin: Springer Berlin/Heidelberg, 2009, Vol. 5825, p. 133-148Conference paper, Published paper (Refereed)
Abstract [en]

Cell libraries often contain a simulation model in a system design language, such as Verilog. These languages usually involve non-determinism, which in turn, poses a challenge to their validation. Simulators often resolve such problems by using certain rules to make the specification deterministic. This however is not justified by the behavior of the hardware that is to be modeled. Hence, simulation might not be able to detect certain errors. In this paper we develop a technique to prove whether non-determinism does not affect the behavior of the simulation model, or whether there exists a situation in which the simulation model might produce different results. To make our technique efficient, we show that the global property of equal behavior for all possible evaluations is equivalent to checking only a certain local property.

Place, publisher, year, edition, pages
Berlin: Springer Berlin/Heidelberg, 2009. Vol. 5825, p. 133-148
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 5825
Keywords [en]
Cell library, Certain rule, Formal analysis, Global properties, Local property, Non-determinism, Simulation model, System design languages, Verilog
National Category
Computer and Information Sciences
Identifiers
URN: urn:nbn:se:hh:diva-20511DOI: 10.1007/978-3-642-04570-7_11ISI: 000278580300011Scopus ID: 2-s2.0-70549094324ISBN: 978-3-642-04569-1 ISBN: 978-3-642-04570-7 ISBN: 3642045693 OAI: oai:DiVA.org:hh-20511DiVA, id: diva2:584506
Conference
14th International Workshop on Formal Methods for Industrial Critical Systems, Eindhoven, NETHERLANDS, NOV 02-03, 2009
Available from: 2013-01-09 Created: 2013-01-08 Last updated: 2018-01-11Bibliographically approved

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full textScopus

Authority records BETA

Mousavi, Mohammad Reza

Search in DiVA

By author/editor
Mousavi, Mohammad Reza
Computer and Information Sciences

Search outside of DiVA

GoogleGoogle Scholar

doi
isbn
urn-nbn

Altmetric score

doi
isbn
urn-nbn
Total: 70 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf