FMCAD
2004
Springer
14 years 4 months ago
2004
Springer
This work presents a memory-efficient All-SAT engine which, given a propositional formula over sets of important and non-important variables, returns the set of all the assignments...
FMCAD
2004
Springer
14 years 4 months ago
2004
Springer
We present a functional approach, based on the ACL2 logic, for the specification of system on a chip communication architectures. Our decomposition of the communications allows the...
FMCAD
2004
Springer
14 years 4 months ago
2004
Springer
The main challenge in BDD-based verification is dealing with the memory explosion problem during reachability analysis. In this paper we advocate a methodology to handle this probl...
FMCAD
2004
Springer
14 years 4 months ago
2004
Springer
Abstract. Probabilistic techniques for verification of finite-state transition systems offer huge memory savings over deterministic techniques. The two leading probabilistic scheme...
FMCAD
2004
Springer
14 years 4 months ago
2004
Springer
In this paper we demonstrate a potential extension of formal verification methodology in order to deal with time-domain properties of analog and mixed-signal circuits whose dynamic...
FMCAD
2004
Springer
14 years 4 months ago
2004
Springer
Abstract. We present a simple method for verifying the safety properties of cache coherence protocols with arbitrarily many nodes. Our presentation begins with two examples. The fi...
FMCAD
2004
Springer
14 years 4 months ago
2004
Springer
Abstract. Transformation-based verification has been proposed to synergistically leverage various transformations to successively simplify and decompose large problems to ones whic...
FMCAD
2004
Springer
14 years 5 months ago
2004
Springer
Abstract. We relate two well-studied methodologies in deductive verification of operationally modeled sequential programs, namely the use of inductive invariants and clock functio...
FMCAD
2004
Springer
14 years 5 months ago
2004
Springer
We consider the problem of checking whether an incomplete design can still be extended to a complete design satisfying a given CTL formula and whether the property is satisfied fo...
FMCAD
2004
Springer
14 years 5 months ago
2004
Springer
This paper describes a new method that is useful in combinational equivalence checking with very challenging industrial designs. The method does not build a miter; instead it build...