Automatic trace analysis for logic of constraints

ABSTRACT

Verification of system designs continues to be a major challenge today. Simulation remains the primary tool for making sure that implementations perform as they should. We present algorithms to automatically generate trace checkers from formulas written in the formal quantitative constraint language, Logic Of Constraints (LOC), to analyze the simulation traces for functional and performance constraint violations. For many interesting formulas, the checkers exhibit linear time complexity and constant memory usage. We illustrate the usefulness and efficiency of this approach with large designs and traces.

REFERENCES

• 1: Openvera assertions white paper. Synopsys, Inc, 2002.
• 2: http://www.systemc.org, Mar. 2003.
• 3: A. Aziz, F. Balarin, R. Brayton, and A. Sangiovanni-Vincentelli. Sequential synthesis using S1S. IEEE Trans. on Computer-Aided Design of Integrated Circuits and Systems, 19(10):1149--62, Oct. 2000.
• 4: F. Balarin, L. Lavagno, C. Passerone, A. Sangiovanni-Vincentelli, M. Sgroi, and Y. Watanabe. Modeling and designing heterogeneous systems. Technical Report 2001/01 Cadence Berkeley Laboratories, Nov. 2001.
• 5: Felice Balarin , Jerry Burch , Luciano Lavagno , Yosinori Watanabe , Roberto Passerone , Alberto Sangiovanni-Vincentelli, Constraints Specification at Higher Levels of Abstraction, Proceedings of the Sixth IEEE International High-Level Design Validation and Test Workshop (HLDVT'01), p.129, December 07-09, 2001
• 6: Xi Chen , Fang Chen , H. Hsieh , F. Balarin , Y. Watanabe, Formal verification of embedded system designs at multiple levels of abstraction, Proceedings of the Seventh IEEE International High-Level Design Validation and Test Workshop (HLDVT'02), p.125, October 27-29, 2002
• 7: C. Eisner and D. Fisman. Sugar 2.0 proposal presented to the accellera formal verification technical committee. Mar. 2002.
• 8: Patrice Godefroid , Gerard J. Holzmann, On the Verification of Temporal Properties, Proceedings of the IFIP TC6/WG6.1 Thirteenth International Symposium on Protocol Specification, Testing and Verification XIII, p.109-124, May 25-28, 1993
• 9: Gerard J. Holzmann, The Model Checker SPIN, IEEE Transactions on Software Engineering, v.23 n.5, p.279-295, May 1997 [doi>10.1109/32.588521]
• 10: K. Keutzer, S. Malik, A. R. Newton, J. Rabaey, and A. Sangiovanni-Vincentelli. System level design: orthogonalization of concerns and platform-based design. IEEE Trans. on Computer-Aided Design, 19(12):1523--1543, Dec. 2000.
• 11: E. A. de Kock , W. J. M. Smits , P. van der Wolf , J.-Y. Brunel , W. M. Kruijtzer , P. Lieverse , K. A. Vissers , G. Essink, YAPI: application modeling for signal processing systems, Proceedings of the 37th conference on Design automation, p.402-405, June 05-09, 2000, Los Angeles, California, United States [doi>10.1145/337292.337511]
• 12: E. J. McCluskey. Logic Design Principles. Prentice Hall, 1986.

INDEX TERMS

Primary Classification:
  B. Hardware
  B.8 Performance and Reliability
      B.8.2 Performance Analysis and Design Aids

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Assertion checkers

General Terms:
Verification

Keywords:
logic of constraints, performance constraint, simulation checker, trace analysis