Mohamad Noureddine, Fadi A. Zaraket, American University of Beirut
Ali S. Elzein, IBM Systems and Technology, elzein@us.ibm.com
Synthesis techniques take realizable Linear Temporal Logic specifications and produce correct circuits that implement the specifications. The generated circuits can be used directly in logic designs, and can also be used as miters that check the correctness of a design. Typically, those techniques generate a non-deterministic finite state automata and translate it into a finite state automata resulting in an exponential blowup in the number of state elements. In this paper, we focus on the problem of generating an And-Inverted-Graph sequential circuit C out of an LTL specification F, expressed in sequential extended regular expressions, for the goal of using C in symbolic and bounded model checkers to validate the correctness of S; an existing circuit implementation of F. We directly encode the non-determinism in F using free input variables resulting in a sequential circuit C with a number of states linear in the size of the formula F. While our technique does not reduce the size of the symbolic and bounded model checking problem, it succeeds to generate the input to the model checker where other techniques fail, and in most cases the model checker succeeds to either find defects in the design that was otherwise uncheckable, or validates the design. We evaluated our technique against existing synthesis techniques with several benchmarks generated from existing LTL synthesis tools and industrial benchmarks including the IBM arbiter, a load balancer, and a traffic light system. Our method found defects and validated systems that we were unable to model check using NUSMV because LTL synthesis failed.