Siemens central R\&D laboratories built a Circuit Verification Environment (CVE) on new principles.

The rapid development of VLSI technology forces companies to develop more and more complex digital circuits in less and less time. For this goal it is also necessary to ensure the newly developed circuits are logically correct.

CVE computes the output behaviour of a digital circuit as Boolean functions of the inputs. Sequential circuits are treated as finite automata. The computed functions are symbolically compared to the corresponding functions of a circuit specification using special, efficient algorithms which guarantee that all differences are detected.

CVE guarantees 100\% security since the symbolic comparison is equivalent to simulating a circuit with all possible input patterns and verifying all simulation outputs. CVE can also replace many time consuming logic simulations with one single automatic comparison and thus save valuable development time.

CVE is implemented in IF/Prolog V5.0 and C. (The IF/Prolog Newsbrief 95-10)