Thesis (Selection of subject)Thesis (Selection of subject)(version: 336)
Assignment details
   Login via CAS
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
Type of assignment: 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
Reviewers: Mgr. Marta Vomlelová, Ph.D.
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.
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.
Charles University | Information system of Charles University |