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

Full description

Saved in:
Bibliographic Details
Main Authors: Purandare, Mitra, Atasu, Kubilay, Hagleitner, Christoph
Format: Conference Proceeding
Language:English
Subjects:
Doped fiber amplifiers
Engines
Formal Verification
Hardware
Hardware > Hardware validation > Functional verification
Impedance matching
Optimization
Registers
Regular Expression Accelerators
Testing
Online Access:Request full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:0738-100X
DOI:10.1145/2228360.2228424