About cookies on this site Our websites require some cookies to function properly (required). In addition, other cookies may be used with your consent to analyze site usage, improve the user experience and for advertising. For more information, please review your options. By visiting our website, you agree to our processing of information as described in IBM’sprivacy statement. To provide a smooth navigation, your cookie preferences will be shared across the IBM web domains listed here.
Publication
DAC 2012
Conference paper
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.