Verification of Out-Of-Order Processor Designs Using Model Checking and a Light-Weight Completion Function