FMCAD
2000
Springer
14 years 3 months ago
2000
Springer
Abstract. Behavior tables are a design formalization intended to support interactive design derivation for hardware and embedded systems. It is a reformulation of the DDD transform...
FMCAD
2000
Springer
14 years 3 months ago
2000
Springer
Bus protocols are hard to specify correctly, and yet it is often critical and highly beneficial that their specifications are correct, complete, and unambiguous. The informal speci...
FMCAD
2000
Springer
14 years 3 months ago
2000
Springer
We take a fresh look at the problem of how to check safety properties of finite state machines. We are particularly interested in checking safety properties with the help of a SAT-...
FMCAD
2000
Springer
14 years 3 months ago
2000
Springer
Abstract. We have formal verified a number of algorithms for evaluating transcendental functions in double-extended precision floating point arithmetic in the Intel
FMCAD
2000
Springer
14 years 3 months ago
2000
Springer
Image computation nds wide application in VLSI CAD, such as state reachability analysis in formal veri cation and synthesis, combinational veri cation, combinational and sequential...
FMCAD
2000
Springer
14 years 3 months ago
2000
Springer
Abstract. In this paper we describe the formal specification and verification of the efficient algorithm for real-time model checking implemented in the model checker RAVEN. It was...
FMCAD
2000
Springer
14 years 3 months ago
2000
Springer
Abstract. Since the advent of model checking it is becoming more common for languages to be given a semantics in terms of transition systems. Such semantics allow to model check pr...
FMCAD
2000
Springer
14 years 3 months ago
2000
Springer
We propose a model for modular synchronous systems with combinational dependencies and define consistency using this model. We then show how to derive this model from a modular spe...
FMCAD
2000
Springer
14 years 3 months ago
2000
Springer
We present a symbolic algorithm for strongly connected component decomposition. The algorithm performs (n log n) image and preimage computations in the worst case, where n is the n...
FMCAD
2000
Springer
14 years 3 months ago
2000
Springer
Abstract. This paper presents a scalable method for parallel symbolic on-the-fly model checking in a distributed memory environment. Our method combines a scheme for on-the-fly mod...