A BMC-based formulation for the scheduling problem of hardware systems
| Autor: | Gianpiero Cabodi, Stefano Quer, Sergio Nocco, Yosinori Watanabe, Alex Kondratyev, Luciano Lavagno |
|---|---|
| Rok vydání: | 2005 |
| Předmět: |
Model checking
Theoretical computer science Job shop scheduling Computer science Binary decision diagram business.industry Concurrency Parallel computing Constraint satisfaction Scheduling (computing) Theory of computation Boolean satisfiability problem business Software Computer hardware Information Systems |
| Zdroj: | International Journal on Software Tools for Technology Transfer. 7:102-117 |
| ISSN: | 1433-2787 1433-2779 |
| DOI: | 10.1007/s10009-004-0170-9 |
| Popis: | Hardware scheduling is a well-known and well-studied problem. This paper defines a new SAT-based formulation of automata-based scheduling and proposes for the first time a completely new resolution algorithm based on SAT solvers and bounded model checking (BMC). The new formulation is specifically suited to control-dominated applications. Alternative executions are modeled as concurrency, where alternative behaviors are followed in parallel. This approach produces "single-path" scheduling traces instead of standard "treelike" solutions, thus enabling the use of BMC. This choice, however, creates the problem that resource bounds are treated incorrectly, due to the artificial concurrency modeling alternative behaviors. We then discuss how to take this into account, either by modifying the SAT solver or by adding extra clauses. Thus we are able to exploit SAT-based BMC to find the desired minimum latency schedule. Our method shows significant improvements in terms of both computational efficiency and modeling power, when compared to the BDD-based approach, and in terms of the optimality of the results when compared to heuristic methods. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full text from SpringerLink