Proving the correctness of digital hardware design using Prolog