Verify: A program for proving correctness of digital hardware designs

摘要

verify is a prolog program that attempts to prove the correctness of a digital design. It does so by showing that the behavior inferred from the interconnection of its parts and their behaviors is equivalent to the specified behavior. It has successfully verified large designs involving many thousands of transistors.