Formal Techniques for Effective Co-verification of Hardware/Software Co-designs

  • Authors:
    Rajdeep Mukherjee (Oxford), Mitra S. Purandare (IBM), Raphael Polig (IBM), Daniel Kroening (Oxford)
    Publication ID:
    P091133
    Publication Type:
    Paper
    Received Date:
    19-Jun-2017
    Last Edit Date:
    20-Jun-2017
    Research:
    2707.001 (University of Oxford)

Abstract

Verification is indispensable for building reliable of hardware/software co-designs. However, the scope of formal methods in this domain is limited. This is attributed to the lack of unified property specification languages, the semantic gap between hardware and software components, and the lack of verifiers that support both C and Verilog/VHDL. To address these limitations, we present an approach that uses a bounded co-verification tool, HW-CBMC, for formally validating hardware/software co-designs written in Verilog and C. Properties are expressed in C enriched with special-purpose primitives that capture temporal correlation between hardware and software events. We present an industrial case-study, proving bounded safety properties as well as discovering critical co-design bugs on a large and complex text analytics FPGA accelerator from IBM.

4819 Emperor Blvd, Suite 300 Durham, NC 27703 Voice: (919) 941-9400 Fax: (919) 941-9450

Important Information for the SRC website. This site uses cookies to store information on your computer. By continuing to use our site, you consent to our cookies. If you are not happy with the use of these cookies, please review our Cookie Policy to learn how they can be disabled. By disabling cookies, some features of the site will not work.