Formal Verification of a System-on-a-Chip using BINGO


In this talk, we present a case study applying our model checking tool, BINGO to a system-on-a-chip. The design under verification is a co-processor for SPARClite including a multimedia accelerator, an SDRAM interface, and a graphic display controller. The chip adopts a complex bus system with four bus bridges, and there were some bugs reported related to bus controls after fabrication. We applied BINGO to the synthesizable RTL description to check if it could find the overlooked bugs.

First we extracted designs concerning bus controls, and applied manual abstraction. The resultant model still contained about 500 registers. Then we wrote scripts that navigated state traversal dynamically in order to avoid state explosion. Through this process, BINGO could successfully find the bugs, and yet one unknown bug was uncovered.

©2002-2018 U.C. Regents