Transfer-Resource Graph and Petri-net for System-on-Chip Verification

1.1 The VLSI Verification Problem Verification of integrated circuit design is a process that checks the implementation of the design against its specification and identifies design bugs. The view that design verification is subservient to design implementation has soon become invalid when designs become just moderately complex. It has been claimed that the verification complexity is growing at a double-exponential rate (Saleh, 2004), i.e., exponential with respect to Moore’s law. Consequently, nowadays, about 50%-80% of the design time and efforts are spent in verylarge-scale-integration (VLSI) design verification. It becomes well known that verification is the biggest single bottleneck (Goering, 2008) in VLSI design. There are two categories of verification methods. • Simulation-based methods. In this category, the verification engineers develop a set of tests to stress a given design; the design is therefore often called the design-under-test or DUT. A test can be an abstract description about the control and observation applied upon the DUT. To actually apply the control and observation, a structure called test-bench (TB) needs to be constructed and simulated together with the DUT. The TB concretizes the abstract tests into “0/1” signals and directly interact with the DUT in these signals. • Formal methods. In formal methods, verification engineers don’t provide tests, but design properties – properties that a correct design should or should not have. Meanwhile, the design usually needs to be represented as a finite-state-machine (FSM) model. Then some model-checking tool computes whether the model abides by the properties. Formal methods form useful supplement to simulation in verifying control-intensive and FSM-based designs.