Generator-based Verification

ABSTRACT

To prove system correctness, assumptions made in verifying a blockmust be cleared by verifying that the block's environment guaranteesthem. Conversely, guarantees enforced by a block may be usedas assumptions for its environment. Block level interface specificationsthus serve as both assumptions and guarantees in compositionalverification. Traditionally, such specifications have beenrepresented as monitors or checkers. In this paper, we propose analternative representation using generators. Novel algorithms arepresented for simulation and formal verification. We argue that forsimulation, representation as a generator can be more efficient thanas a checker - both asymptotically and practically. We also identifya subset of generators that can be efficiently handled using formaltechniques. Experimental results are given for some benchmarkexamples and industrial case studies.

REFERENCES

• 1: Rajeev Alur , Thomas A. Henzinger , Freddy Y. C. Mang , Shaz Qadeer , Sriram K. Rajamani , Serdar Tasiran, MOCHA: Modularity in Model Checking, Proceedings of the 10th International Conference on Computer Aided Verification, p.521-525, June 28-July 02, 1998
• 2: Randal E. Bryant, Graph-Based Algorithms for Boolean Function Manipulation, IEEE Transactions on Computers, v.35 n.8, p.677-691, August 1986 [doi>10.1109/TC.1986.1676819]
• 3: David L. Dill, Trace theory for automatic hierarchical verification of speed-independent circuits, Carnegie Mellon University, Pittsburgh, PA, 1987
• 4: James H. Kukula , Thomas R. Shiple, Building Circuits from Relations, Proceedings of the 12th International Conference on Computer Aided Verification, p.113-123, July 15-19, 2000
• 5: Zohar Manna , Amir Pnueli, The temporal logic of reactive and concurrent systems, Springer-Verlag New York, Inc., New York, NY, 1992
• 6: [6] K. McMillan. http://www-cad.eecs.berkeley.edu/ kenmcmil/smv/.
• 7: Kenneth L. McMillan, A Compositional Rule for Hardware Design Refinement, Proceedings of the 9th International Conference on Computer Aided Verification, p.24-35, June 22-25, 1997
• 8: Orna Grumberg , David E. Long, Model checking and modular verification, ACM Transactions on Programming Languages and Systems (TOPLAS), v.16 n.3, p.843-871, May 1994 [doi>10.1145/177492.177725]
• 9: Kanna Shimizu , David L. Dill, Deriving a simulation input generator and a coverage metric from a formal specification, Proceedings of the 39th conference on Design automation, June 10-14, 2002, New Orleans, Louisiana, USA [doi>10.1145/513918.514118]
• 10: Kanna Shimizu , David L. Dill , Alan J. Hu, Monitor-Based Formal Specification of PCI, Proceedings of the Third International Conference on Formal Methods in Computer-Aided Design, p.335-353, November 01-03, 2000
• 11: L. J. Stockmeyer , A. R. Meyer, Word problems requiring exponential time(Preliminary Report), Proceedings of the fifth annual ACM symposium on Theory of computing, p.1-9, April 30-May 02, 1973, Austin, Texas, United States [doi>10.1145/800125.804029]
• 12: Dong Wang , Pei-Hsin Jiang , James Kukula , Yunshan Zhu , Tony Ma , Robert Damiano, Formal property verification by abstraction refinement with formal, simulation and hybrid engines, Proceedings of the 38th conference on Design automation, p.35-40, June 2001, Las Vegas, Nevada, United States [doi>10.1145/378239.378260]
• 13: Jun Yuan , Kurt Shultz , Carl Pixley , Hillel Miller , Adnan Aziz, Modeling design constraints and biasing in simulation using BDDs, Proceedings of the 1999 IEEE/ACM international conference on Computer-aided design, p.584-590, November 07-11, 1999, San Jose, California, United States

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Formal methods

Additional Classification:
  D. Software
  D.4 OPERATING SYSTEMS
      D.4.5 Reliability
          Subjects: Verification
      D.4.8 Performance
          Subjects: Simulation

General Terms:
Algorithms, Reliability, Verification