Synchronization verification in system-level design with ilp solvers

Concurrency is one of the most important issues in system-level design. Interleaving among parallel processes can cause an extremely large number of different behav-iors, making design and verification difficult tasks. In this work, we propose a synchronization verification method for system-level designs described in the SpecC language. In-stead of modeling the design with timed FSMs and using a model checker for timed automata (such as UPPAAL or KRONOS), we formulate the timing constraints with equal-ities/inequalities that can be solved by integer linear pro-gramming (ILP) tools. Verification is conducted in two steps. First, similar to other software model checkers, we compute the reachability of an error state in the absence of timing constraints. Then, if a path to an error state exists, its feasibility is checked by using the ILP solver to evalu-ate the timing constraints along the path. This approach can drastically increase the sizes of the designs that can be verified. Abstraction and abstraction refinement techniques based on the Counterexample-Guided Abstraction Refine-ment (CEGAR) paradigm are applied. The proposed verifi-cation flow is introduced and some preliminary results are presented here. 1