Lecture by Dr Wayne Luk
Published：2012-09-24
ASIC and System State Key Laboratory Lecture Series XI
Automating Formal Verification of Customized Soft-Processors
Dr Wayne Luk （British Imperial College）
Time & Date : 9:30-11:00 am on 25 Sep, 2012
Places：Room 369 , Microelectronics Building, Zhangjiang Campus
Abstract
Soft–processors, instruction processors implemented in FPGA technology, are often customizable to support domain-specific optimization. However the correctness of customized soft-processors, executing the associated machine code, is often not obvious. This talk proposes a novel approach for verifying the implementation of an application program for a customized soft-processor, based on the ACL2 theorem prover. The correctness proof involves verifying a machine code program executing on the target hardware device against a high-level specification of the application program. We illustrate the proposed approach with several case studies, showing how processors with different custom instructions and with different number of pipelined stages can be automatically produced and verified. Such processors have a range of trade-offs in performance, size, power and energy consumption to meet different requirements.
Biography
Dr Wayne Luk is Professor of Computer Engineering at Imperial College London. He founded and leads the Computer Systems Section and the Custom Computing Group in Department of Computing, and was Visiting Professor at Stanford University and Queen's University Belfast. His research interests include reconfigurable computing, field-programmable technology, and design automation. He developed hardware compilation techniques based on syntax-directed translation, pipeline vectorization, and source-level transformation; he contributed to optimizations for run-time reconfiguration, custom instruction processors, and programmable embedded-block architecture for field-programmable devices. He received many awards at international conferences, including FPL (2004, 2007, 2008, 2010), ERSA (2004), FPT (2005, 2008), ASAP (2008), SAMOS (2008), and SPL (2008, 2009). He led a team winning two Platform Grants from UK Engineering and Physical Sciences Research Council, and a Research Excellence Award from Imperial College. He is a Fellow of the IEEE and a Fellow of the BCS, and is Editor-in-Chief for ACM Transactions on Reconfigurable Technology and Systems. He received his MA, MSc and DPhil degrees from University of Oxford.
Dr Wayne Luk （British Imperial College）
Time & Date : 9:30-11:00 am on 25 Sep, 2012
Places：Room 369 , Microelectronics Building, Zhangjiang Campus
Abstract
Soft–processors, instruction processors implemented in FPGA technology, are often customizable to support domain-specific optimization. However the correctness of customized soft-processors, executing the associated machine code, is often not obvious. This talk proposes a novel approach for verifying the implementation of an application program for a customized soft-processor, based on the ACL2 theorem prover. The correctness proof involves verifying a machine code program executing on the target hardware device against a high-level specification of the application program. We illustrate the proposed approach with several case studies, showing how processors with different custom instructions and with different number of pipelined stages can be automatically produced and verified. Such processors have a range of trade-offs in performance, size, power and energy consumption to meet different requirements.
Biography
Dr Wayne Luk is Professor of Computer Engineering at Imperial College London. He founded and leads the Computer Systems Section and the Custom Computing Group in Department of Computing, and was Visiting Professor at Stanford University and Queen's University Belfast. His research interests include reconfigurable computing, field-programmable technology, and design automation. He developed hardware compilation techniques based on syntax-directed translation, pipeline vectorization, and source-level transformation; he contributed to optimizations for run-time reconfiguration, custom instruction processors, and programmable embedded-block architecture for field-programmable devices. He received many awards at international conferences, including FPL (2004, 2007, 2008, 2010), ERSA (2004), FPT (2005, 2008), ASAP (2008), SAMOS (2008), and SPL (2008, 2009). He led a team winning two Platform Grants from UK Engineering and Physical Sciences Research Council, and a Research Excellence Award from Imperial College. He is a Fellow of the IEEE and a Fellow of the BCS, and is Editor-in-Chief for ACM Transactions on Reconfigurable Technology and Systems. He received his MA, MSc and DPhil degrees from University of Oxford.