Paper Info
Title
Integrating formal verification and high-level processor pipeline synthesis
Abstract
When a processor implementation is synthesized from a specification using an automatic framework, this implementation still should be verified against its specification to ensure the automatic framework introduced no error. This paper presents our effort in integrating fully automated formal verification with a high-level processor pipeline synthesis framework. As an integral part of the pipeline synthesis, our framework also emits SMV models for checking the functional equivalence between the output pipelined processor implementation and its input non-pipelined specification. Well known compositional model checking techniques are automatically applied to curtail state explosion during model checking. The paper reports case studies of applying this integrated framework to synthesize and formally verify pipelined RISC and CISC processors.
Year
DOI
Venue
2011
10.1109/SASP.2011.5941073
Application Specific Processors
Keywords
Field
DocType
emits smv model,output pipelined processor implementation,processor implementation,model checking,integrated framework,input non-pipelined specification,cisc processor,high-level processor pipeline synthesis,automatic framework,formal verification,compositional model checking technique,registers,register transfer level,formal specification,reduced instruction set computing,hazards,pipelines,high level synthesis,intermediate representation,radio frequency,risc processor,semantics
Pipeline transport,Model checking,Computer science,High-level synthesis,Parallel computing,Real-time computing,Formal specification,Reduced instruction set computing,Complex instruction set computing,Semantics,Formal verification
Conference
ISBN
Citations 
PageRank 
978-1-4577-1212-8
0
0.34
References 
Authors
8
4
Name
Order
Citations
PageRank
Eriko Nurvitadhi139933.08
James C. Hoe22048141.34
Timothy Kam318617.26
Shih-Lien L. Lu4555.39