Abstract

In the last years, great improvement of the microelettronics technology has been very important for the grow of VLSI (very large scale integration) circuits and ASIC (application specific integrated circuit) components.
CAD (computer aied design) system play a key role to make a product bug-free under the contrain that no error of construction will be present.
Formal verification means having a mathematic model of a system, a language for specifying desired properties of the system im a concise, comprehensible and unambiguos way, and a method of proof to verify that the specified properties are satisfied.
On the other hand, in recently years, function, set and relation are rapresentated by BDD (Binary Decision Diagram).
They have improved the grow of symbolic tecnics. We speak of symbolic verification when the formal verification is join to BDD.
The goal of thesis is deal with some problems in this field, both teorich and pratical approach.