PBS: proven Boolean simplification

We describe PBS, a formally proven implementation of multi-level logic synthesis based on the weak division algorithm. We have proved that for all legal input circuits, PBS generates an output circuit that is functionally correct and has minimal size. PBS runs on large examples in reasonable time for a prototype system. PBS, was verified using the Nuprl proof development system. The proof of PBS, which required several months, was well worth the effort since the benefits are realized every time the program is run. When engineers use a verified synthesis tool, they get the increased confidence of applying formal methods to their designs without the cost of varying each design produced