Proving Correctness Of Regular Expression Accelerators

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 mode led 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.