Topic of PhD thesis

Advisor:Vojnar Tomáš, prof. Ing., Ph.D.
Student:Charvát Lukáš, Ing.
Topic:Automated Verification in Hardware Design and Hardware/Software Codesign -- co-supervised by dr. A. Smrcka
Start:2011/2012
PhD thesis subject:

Předmětem práce je výzkum efektivních metod automatické verifikace pro potřeby ověřování vlastností hardware vyvíjeného s využitím současných návrhových technik (např. rekonfigurovatelný hardware, vyvíjející se hardware apod.) a systémů vyvíjených v rámci tzv. souběžného vývoje technického a programového vybavení (tj. systémů vyvíjených v prostředí tzv. "hardware/software codesign"). Zkoumány mohou být jak metody inteligentního testování tak různých forem formální verifikace (statická analýza, abstraktní interpretace, model checking), příp. jejich vhodných kombinací.

Zvláštní pozornost si v rámci uvedeného tématu zaslouží rozvoj formálních metod pro ověřování jednotlivých fází souběžného návrhu technického a programového vybavení. Jedná se např. o vývoj podpory automatického ověřování korektnosti a ekvivalence návrhů hardware generovaných z různě abstraktních modelů (což zasahuje i do oblasti souvisejících s verifikací překladačů), vývoj metod pro analýzu časových omezení modelů hardware (např. pro usnadnění návrhu komunikačních protokolů nebo řízení souběžného přístupu ke sdíleným prostředkům) a návrh metod kombinace formální verifikace a testování (konkrétně automatického generování testovacích případů) s cílem co nejvíce zefektivnit ověřovací fázi návrhu. Téma zahrnuje i možnost rozvoje efektivity současných technik automatické verifikace pomocí jejich akcelerace v hardware.

Práce bude řešena ve spolupráci s týmem VeriFIT (zejména pak dr. A. Smrčkou) zabývajícím se na FIT VUT automatizovanou verifikací. Je zde také možnost spolupracovat s týmem projektu Lissom.

[1] Ulrich Kuhne, Sven Beyer, Christian Pichler. Generating an Efficient Instruction Set Simulator from a Complete Property Suite. In Proc. of (RSP'09) the 2009 IEEE/IFIP International Symposium on Rapid System Prototyping. Paris, 2009. pp. 109-115. doi:10.1109/RSP.2009.19
[2] Xavier Leroy. A Formally Verified Compiler Back-end. Journal of Automated Reasoning 43(4), pp. 363-446, 2009. doi:10.1007/s10817-009-9155-4
[3] Shunsuke Sasaki, Tasuku Nishihara, Daisuke Ando, Masahiro Fujita. Hardware/Software Co-design and Verification Methodology from System Level Based on System Dependence Graph. Journal of Universal Computer Science 13(13), 2007. doi:10.3217/jucs-013-13-1972
[4] Shai Fine, Avi Ziv. Coverage Directed Test Generation for Functional Verification using Bayesian Networks. In Proc. of the 40th annual Design Automation Conference, pp. 286-291, 2003.
[5] Shmuel Ur and Yaov Yadin. 1999. Micro architecture coverage directed generation of test programs. In Proceedings of the 36th annual ACM/IEEE Design Automation Conference (DAC'99), Mary Jane Irwin (Ed.). ACM, New York, NY, USA, 175-180. DOI=10.1145/309847.309909

Part of research project:
Related publications:
2010KŘENA Bohuslav, LETKO Zdeněk, UR Shmuel and VOJNAR Tomáš. A Platform for Search-Based Testing of Concurrent Software. In: PADTAD '10. Trento: Association for Computing Machinery, 2010, p. 11. ISBN 978-1-60558-823-0.
 SMRČKA Aleš and VOJNAR Tomáš. Verification of Asynchronous and Parametrized Hardware Designs. Brno: Faculty of Information Technology BUT, 2010. ISBN 978-80-214-4214-6.
2008SMRČKA Aleš and VOJNAR Tomáš. Verifying Parametrised Hardware Designs Via Counter Automata. In: Hardware and Software, Verification and Testing. Heidelberg: Springer Verlag, 2008, pp. 51-68. ISSN 0302-9743.
2007SMRČKA Aleš, ŘEHÁK Vojtěch, VOJNAR Tomáš, ŠAFRÁNEK David, MATOUŠEK Petr and ŘEHÁK Zdeněk. Verifying VHDL Design with Multiple Clocks in SMV. In: Formal Methods: Applications and Technology. Bonn: Springer Verlag, 2007, pp. 148-164. ISSN 0302-9743.