hh.sePublications
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • 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, 133-148 p.Conference 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, 133-148 p.
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 5825
Keyword [en]
Cell library, Certain rule, Formal analysis, Global properties, Local property, Non-determinism, Simulation model, System design languages, Verilog
National Category
Computer and Information Science
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: 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: 2014-11-11Bibliographically approved

Open Access in DiVA

No full text

Other links

Publisher's full textScopus

Search in DiVA

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

Search outside of DiVA

GoogleGoogle Scholar

Altmetric score

Total: 64 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • 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