Paper Info
Title
Proving Functional Correctness of Weakly Programmable IPs - A Case Study with Formal Property Checking
Abstract
In recent years, designing Systems-on-Chip (SoCs) with domain specific and customizable embedded processors (ASIPs) has become standard practice. When compared with general purpose processors on the one hand and dedicated hardwired accelerators on the other hand, these processor cores provide new trade-offs between flexibility, energy and performance. Since they are intended to only run a restricted set of application-specific programs this knowledge is often exploited to further optimize the architecture resulting in weakly programmable IP cores. Such weakly programmable systems raise new challenges for hardware and software verification. The conventional separation of hardware and software verification based on a generic and well-defined instruction set is no longer sustainable. In this paper, we present a case study applying formal property checking to state-of-the-art designs of two weakly programmable IP blocks. A methodology is presented which is oriented at the operations of the ASIP rather than its instructions. As a by-product of our methodology for hardware verification we formalize the software restrictions exploited for optimization of the micro-architecture. We show that an automatic compliance check is feasible which certifies that the software complies with these restrictions. To our best knowledge, this is the first time that functional correctness of ASIP hardware and HW/SW compliance for a realistic design was completely verified using a formal methodology.
Year
DOI
Venue
2008
10.1109/SASP.2008.4570785
Anaheim, CA
Keywords
Field
DocType
software restriction,weakly programmable ips,formal methodology,case study,proving functional correctness,formal property checking,weakly programmable system,weakly programmable ip core,weakly programmable ip block,hardware verification,software complies,asip hardware,software verification,sw compliance,application software,computer architecture,system on chip,reduced instruction set computing,software performance,hardware,process design,pipelines,integrated circuit design,embedded processor,energy efficiency
Model checking,Instruction set,Computer science,Correctness,Real-time computing,Software performance testing,Software,Multi-core processor,Computer architecture,System on a chip,Parallel computing,Software verification,Embedded system
Conference
ISBN
Citations 
PageRank 
978-1-4244-2334-7
1
0.37
References 
Authors
10
6
Name
Order
Citations
PageRank
Sacha Loitz110.37
Markus Wedler27712.44
Christian Brehm3151.90
Timo Vogt4778.09
Norbert Wehn51165137.17
Wolfgang Kunz623633.71