Hardware/Software Co-verification Using Path-based Symbolic Execution

Mukherjee, Rajdeep and Joshi, Saurabh and O'Leary, John and et al, . (2020) Hardware/Software Co-verification Using Path-based Symbolic Execution. arXiv.org.


Download (200kB) | Preview


Conventional tools for formal hardware/software co-verification use bounded model checking techniques to construct a single monolithic propositional formula. Formulas generated in this way are extremely complex and contain a great deal of irrelevant logic, hence are difficult to solve even by the state-of-the-art Satisfiability (SAT) solvers. In a typical hardware/software co-design the firmware only exercises a fraction of the hardware state-space, and we can use this observation to generate simpler and more concise formulas. In this paper, we present a novel verification algorithm for hardware/software co-designs that identify partitions of the firmware and the hardware logic pertaining to the feasible execution paths by means of path-based symbolic simulation with custom path-pruning, propertyguided slicing and incremental SAT solving. We have implemented this approach in our tool COVERIF. We have experimentally compared COVERIF with HW-CBMC, a monolithic BMC based co-verification tool, and observed an average speed-up of 5× over HW-CBMC for proving safety properties as well as detecting critical co-design bugs in an open-source Universal Asynchronous Receiver Transmitter design and a large SoC design.

[error in script]
IITH Creators:
IITH CreatorsORCiD
Item Type: Article
Subjects: Computer science
Divisions: Department of Computer Science & Engineering
Depositing User: Team Library
Date Deposited: 13 Jan 2020 11:27
Last Modified: 13 Jan 2020 11:27
URI: http://raiith.iith.ac.in/id/eprint/7315
Publisher URL:
Related URLs:

Actions (login required)

View Item View Item
Statistics for RAIITH ePrint 7315 Statistics for this ePrint Item