Sökning: id:"swepub:oai:DiVA.org:hh-20511" >
Formal analysis of ...
Formal analysis of non-determinism in Verilog cell library simulation models
-
- Raffelsieper, Matthias (författare)
- Department of Computer Science, TU Eindhoven, P.O. Box 513, Eindhoven, The Netherlands
-
- Mousavi, Mohammad Reza (författare)
- Department of Computer Science, TU Eindhoven, P.O. Box 513, Eindhoven, The Netherlands
-
- Roorda, Jan-Willem (författare)
- Fenix Design Automation, P.O. Box 920, Eindhoven, The Netherlands
-
visa fler...
-
- Strolenberg, Chris (författare)
- Fenix Design Automation, P.O. Box 920, Eindhoven, The Netherlands
-
- Zantema, Hans (författare)
- Department of Computer Science, TU Eindhoven, P.O. Box 513, Eindhoven, The Netherlands
-
visa färre...
-
Department of Computer Science, TU Eindhoven, PO. Box 513, Eindhoven, The Netherlands Fenix Design Automation, P.O. Box 920, Eindhoven, The Netherlands (creator_code:org_t)
- Berlin : Springer Berlin/Heidelberg, 2009
- 2009
- Engelska.
-
Ingår i: Formal Methods for Industrial Critical Systems. - Berlin : Springer Berlin/Heidelberg. - 9783642045691 - 9783642045707 - 3642045693 ; , s. 133-148
- Relaterad länk:
-
https://urn.kb.se/re...
-
visa fler...
-
https://doi.org/10.1...
-
visa färre...
Abstract
Ämnesord
Stäng
- 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.
Ämnesord
- NATURVETENSKAP -- Data- och informationsvetenskap (hsv//swe)
- NATURAL SCIENCES -- Computer and Information Sciences (hsv//eng)
Nyckelord
- Cell library
- Certain rule
- Formal analysis
- Global properties
- Local property
- Non-determinism
- Simulation model
- System design languages
- Verilog
Publikations- och innehållstyp
- ref (ämneskategori)
- kon (ämneskategori)
Hitta via bibliotek
Till lärosätets databas