Word level bitwidth reduction for unbounded hardware model checking |
| |
Authors: | Per Bjesse |
| |
Affiliation: | (1) Synopsys Inc., 2025 NW Cornelius Pass Rd., Hillsboro, OR 97124, USA |
| |
Abstract: | In this paper we present a word-level model checking method that attempts to speed up safety property checking of industrial
netlists. Our aim is to construct an algorithm that allows us to check both bounded and unbounded properties using standard
bit-level model checking methods as back-end decision procedures, while incurring minimum runtime penalties for designs that
are unsuited to our analysis. We do this by combining modifications of several previously known techniques into a static abstraction
algorithm which is guaranteed to produce bit-level netlists that are as small or smaller than the original bitblasted designs.
We evaluate our algorithm on several challenging hardware components. |
| |
Keywords: | Word level Model checking Static analysis Formal methods |
本文献已被 SpringerLink 等数据库收录! |