| Abstract
|
<p>Cell libraries often contain a si … <p>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.</p>g only a certain local property.</p>
|
| Author
|
Matthias Raffelsieper +
, Mohammad Reza Mousavi +
, Jan-Willem Roorda +
, Chris Strolenberg +
, Hans Zantema +
|
| Conference
|
14th International Workshop on Formal Methods for Industrial Critical Systems, Eindhoven, NETHERLANDS, NOV 02-03, 2009
|
| DOI
|
http://dx.doi.org/10.1007/978-3-642-04570-7_11 +
|
| Diva
|
http://hh.diva-portal.org/smash/record.jsf?searchId=1&pid=diva2:584506
|
| EndPage
|
148 +
|
| HostPublication
|
Formal Methods for Industrial Critical Systems : 14th International Workshop, FMICS 2009, Eindhoven, The Netherlands, November 2-3, 2009. Proceedings +
|
| PublicationType
|
Conference Paper +
|
| Publisher
|
Springer Berlin/Heidelberg +
|
| Series
|
Lecture Notes in Computer Science ; 5825 +
|
| StartPage
|
133 +
|
| Title
|
Formal analysis of non-determinism in Verilog cell library simulation models +
|
| Volume
|
5825 +
|
| Year
|
2009 +
|
| Has queryThis property is a special property in this wiki.
|
Publications:Formal analysis of non-determinism in Verilog cell library simulation models +
, Publications:Formal analysis of non-determinism in Verilog cell library simulation models +
, Publications:Formal analysis of non-determinism in Verilog cell library simulation models +
, Publications:Formal analysis of non-determinism in Verilog cell library simulation models +
, Publications:Formal analysis of non-determinism in Verilog cell library simulation models +
, Publications:Formal analysis of non-determinism in Verilog cell library simulation models +
, Publications:Formal analysis of non-determinism in Verilog cell library simulation models +
, Publications:Formal analysis of non-determinism in Verilog cell library simulation models +
, Publications:Formal analysis of non-determinism in Verilog cell library simulation models +
, Publications:Formal analysis of non-determinism in Verilog cell library simulation models +
|
| Categories |
Publication +
|
| Modification dateThis property is a special property in this wiki.
|
26 June 2014 03:43:49 +
|
