
376 CHAPTER 10 Verifi cation and Security Issues
Figure 10.3 shows the verifi cation setup for the arbiter core, which included
master and slave modules written in the RuleBase EDL. Properties of the arbiter
such as arbitration, bus-locking, timeout, and pipeline transfers were checked for
compliance with the specifi cation document. Several bugs were found in the arbi-
ter core as a result of the verifi cation effort. Most of these bugs were traced back
to problems in the specifi cation document, which were classifi ed as:
(i) Ambiguity : Some statements could be interpreted in different ways.
(ii) Incompleteness: The behavior of ...