Hybrid verification of a hardware modular reduction engine

Wide-operand modular math functions pose an enormous challenge for verification. We present a novel method to verify a modular reduction engine implemented as a finite state machine (FSM), leveraging a combination of model checking and theorem proving. As a first step of the verification, preconditions and post-conditions for each state transition of the FSM are identified. Next the implications from the pre-conditions to the post-conditions are verified using a model checker. The last step entails combining all the implications in a theorem prover to derive the overall correctness proof. We carried out this verification using a hybrid formal verification platform comprising the ACL2 theorem prover and IBM´s model checker SixthSense, along with numerous techniques to cope with the complexities of this verification task. To our knowledge, this is the first published method for the exhaustive verification of an RTL-implementation of a wide-operand industrial modular reduction engine.