FMCAD
14 years 1 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
14 years 1 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
14 years 3 months ago
2004 Springer 
We present a new and very simple translation of the bounded model checking problem which is linear both in the size of the formula and the length of the bound. The resulting CNF-fo...
FMCAD
14 years 3 months ago
2004 Springer 
Most symbolic model checkers are based on either Binary Decision Diagrams (BDDs), which may grow exponentially large, or Satisfiability (SAT) solvers, whose time requirements rapi...
FMCAD
14 years 1 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...
|
Formal Methods