Sciweavers

Share
IEICET
2006

Synchronization Verification in System-Level Design with ILP Solvers

11 years 1 months ago
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 behaviors, making design and verification difficult tasks. In this work, we propose a synchronization verification method for system-level designs described in the SpecC language. Instead 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 equalities/inequalities that can be solved by integer linear programming (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 evaluate the timing constraints along the path. This approach can drastically increase the sizes of the designs that can be . Abstraction and ab...
Thanyapat Sakunkonchak, Satoshi Komatsu, Masahiro
Added 12 Dec 2010
Updated 12 Dec 2010
Type Journal
Year 2006
Where IEICET
Authors Thanyapat Sakunkonchak, Satoshi Komatsu, Masahiro Fujita
Comments (0)
books