Synthesis of Sequential Extended Regular Expressions for Verification
Synthesis techniques take realizable Linear Temporal Logic specifications and produce correct cir- cuits that implement the specifications. The generated circuits can be used directly, or as miters that check the correctness of a logic design. Typically, those techniques generate non-deterministic finite state automata, which can be determinized at a possibly exponential cost. Recent results show multiple advantages of using deterministic automata in symbolic and bounded model checking of LTL safety properties. In this paper, we present a technique with a supporting tool that takes a sequential extended regular expression specification Φ, and a logic design implementation S, and generates a sequential circuit C, expressed as an And-Inverted-Graph, that checks whether S satisfies Φ. The technique passes the generated circuit C to ABC, a bounded model checker, to validate correctness. We use free input variables to encode the non- determinism in Φ and we obtain a number of states in miter linear in the size of Φ. Our technique succeeds to generate the input to the model checker while other techniques fail because of the exponential blowup, and in most cases, ABC succeeds to either find defects in the design that was otherwise uncheckable, or validate the design. We evaluated our technique against several industrial benchmarks including the IBM arbiter, a load balancer, and a traffic light system, and compared our results with the NuSMV framework. Our method found defects and validated systems NuSMV could not validate.