FMCAD
2004
Springer
13 years 8 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
13 years 8 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
13 years 8 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
13 years 8 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
13 years 8 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
13 years 8 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
13 years 8 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
13 years 10 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
13 years 10 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
13 years 10 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...