Proving correctness of regular expression accelerators

Abstract

A popular technique in regular expression matching accelerators is to decompose a regular expression and communicate through instructions executed by a post-processor. We present a complete verification method that leverages the success of sequential equivalence checking (SEC) to proving correctness of the technique. The original regular expression and the system of decomposed regular expressions are modeled as net-lists and their equivalence is proved using SEC. SEC proves correct handling of 840 complex patterns from the Emerging Threats open rule set in 50 hours, eliminating altogether informal simulation and testing. © 2012 ACM.