Constraint satisfaction for HW/SW verification

• Thesis title in Czech: Použití programování s omezujícími podmínkami pro verifikaci HW/SW
• Thesis title in English: Constraint satisfaction for HW/SW verification
• Academic year of topic announcement: 2006/2007
• Thesis type: diploma thesis
• Thesis language: angličtina
• Department: Department of Theoretical Computer Science and Mathematical Logic (32-KTIML)
• Supervisor: prof. RNDr. Roman Barták, Ph.D.
• Author: hidden - assigned and confirmed by the Study Dept.
• Date of registration: 08.11.2006
• Date of assignment: 08.11.2006
• Date and time of defence: 26.05.2008 00:00
• Date of electronic submission: 26.05.2008
• Date of proceeded defence: 26.05.2008
• Opponents: Mgr. Marta Vomlelová, Ph.D.

Guidelines

Student will familiarise himself with constraint satisfaction techniques and HW/SW verification problems. The goal of thesis is
- to study possible application of constraint satisfaction technology in HW/SW verification,
- to identify particular sub-problems of HW/SW verification problem where this technology is appropriate,
- to propose necessary extensions of constraint satisfaction techniques for solving these sub-problems.

References

1) R. Dechter: Constraint Processing, Morgan Kaufmann Publishers (Elsevier Science), 2003.

2) E. Bin, R. Emek, G. Shurek, A. Ziv: Using a constraint satisfaction formulation and solution techniques for random test program generation, IBM Systems Journal, Vol. 41, No. 3, pp. 386-402, 2002.

3) Yehuda Naveh, Michal Rimon, Itai Jaeger, Yoav Katz, Michael Vinov, Eitan Marcus, and Gil Shurek: Constraint-Based Random Stimuli Generation for Hardware Verification, Proceedings of IAAI-06, pp. 1720-1727, AAAI Press, 2006.

4) Vibhav Gogate and Rina Dechter: A New Algorithm for Sampling CSP Solutions Uniformly at Random, Proceedings of CP 2006, pp. 711-715, LNCS 4204, Springer Verlag, 2006.

Preliminary scope of work

Constraint satisfaction technology is used to solve combinatorial optimisation problems where a solution satisfying all constraints and, in some cases, optimizing a given objective function is searched for among the large number of candidate variable assignments. Part of HW/SW verification is generating a random code or data that fulfil some constraints, so constraint satisfaction techniques seem appropriate here. Nevertheless, the nature of HW/SW verification problems may require some extensions of traditional constraint satisfaction techniques like modelling huge domains or random distribution of solutions. The work deals with these extended techniques of constraint satisfaction.