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 f or all legal input circuits, PBS generates an output circuit that is f unctionally correct and has minimal size. PBS runs on large examples i n reasonable time for a prototype system. PBS, was verified using the Nuprl proof development system. The proof of PBS, which required sever al months, was well worth the effort since the benefits are realized e very 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 verying each design produced.