Functional abstraction and formal proof of digital circuits

A discussion is given on the set of tools that has been developed at Bull for functional verification of VLSI circuits. The functional verification process is based on two key concepts. The first one is functional abstraction which consists of automatically producing a functional view of a circuit from a lower level of description that can be either a structural or a layout description. The second one is formal verification that consists of automatically proving that the abstracted view of a circuit is correct with respect to its functional specification given by the circuit designer. The set of tools implementing these concepts is intensively used at Bull by all VLSI circuit designers