Imperial College London
Professor Wayne Luk

ProfessorWayneLuk

Faculty of Engineering, Department of Computing

Professor of Computer Engineering
 
 
 
//

Contact

 

+44 (0)20 7594 8313w.luk Website

 
 
//

Location

 

434Huxley BuildingSouth Kensington Campus

//

Summary

 

Publications

Citation

BibTex format

@inproceedings{Susanto:2011:10.1109/FPT.2011.6132692,
author = {Susanto, KW and Luk, W},
doi = {10.1109/FPT.2011.6132692},
title = {Automating formal verification of customized soft-processors},
url = {http://dx.doi.org/10.1109/FPT.2011.6132692},
year = {2011}
}
Download

RIS format (EndNote, RefMan)

TY  - CPAPER
AB  - 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 paper 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. © 2011 IEEE.
AU  - Susanto,KW
AU  - Luk,W
DO  - 10.1109/FPT.2011.6132692
PY  - 2011///
TI  - Automating formal verification of customized soft-processors
UR  - http://dx.doi.org/10.1109/FPT.2011.6132692
ER  -
Download