Verifying logic design of a processor with an instruction pipeline by comparing the output from first and second instances of the design

摘要: A logic design for a processor execution unit includes an instruction pipeline 10 with one or more stages 12 executing plurality of instructions. method formal verification the involves selecting from instructions and may verify processing that using model checking. under test is created by first 30 second 32 instance design. The initialized defined values in each stage random initial stage. then simultaneously issued to instance, executed comparison results output pipelines made 16. If was verified checking, approving correctness if result true. not verifiable sequenced computation