The Compositional Far Side of Image Computation

ABSTRACT

Symbolic image computation is the most fundamental computationin BDD-based sequential system optimization and formal verification.In this paper, we explore the use of over-approximationand BDD minimization with donýt cares during image computation.Our new method, based on the partitioned representation ofthe transition relation, consists of three phases: First, the model istreated as a set of loosely coupled components, and over-approximateimages are computed to minimize the transition relation ofeach component. A refined overall image is then computed usingthe simplified transition relation. Finally, the exact image isobtained by a clipping operation that recovers all previous over-approximations.Since BDD minimization employs constraints on thenext-state variables of the transition relation, instead of the customaryconstraints on the present-state variables, we call the resultingmethod far side image computation.The new method can be implemented on top of any image computationalgorithm that is based on the partitioned transition relation.(For example, IWLS95, MLP, and Fine-Grain.)We demonstrate the effectiveness of our approach by experimentson models ranging from easy to hard: The new method wins significantlyover the best known algorithms so far in both CPU timeand memory usage, especially on the hard models.

REFERENCES

• 1: Robert K. Brayton , Gary D. Hachtel , Alberto L. Sangiovanni-Vincentelli , Fabio Somenzi , Adnan Aziz , Szu-Tsung Cheng , Stephen A. Edwards , Sunil P. Khatri , Yuji Kukimoto , Abelardo Pardo , Shaz Qadeer , Rajeev K. Ranjan , Shaker Sarwary , Thomas R. Shiple , Gitanjali Swamy , Tiziano Villa, VIS: A System for Verification and Synthesis, Proceedings of the 8th International Conference on Computer Aided Verification, p.428-432, August 03, 1996
• 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: [3] J. Burch. Using BDD's to verify multipliers. In 1991 International Workshop on Formal Methods in VLSI Design, Miami, FL, Jan. 1991.
• 4: Pankay Chauhan , Edmund M. Clarke , Somesh Jha , James H. Kukula , Helmut Veith , Dong Wang, Using Combinatorial Optimization Methods for Quantification Scheduling, Proceedings of the 11th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods, p.293-309, September 04-07, 2001
• 5: Pankaj Chauhan , Edmund M. Clarke , Somesh Jha , Jim Kukula , Tom Shiple , Helmut Veith , Dong Wang, Non-linear quantification scheduling in image computation, Proceedings of the 2001 IEEE/ACM international conference on Computer-aided design, November 04-08, 2001, San Jose, California
• 6: Hyunwoo Cho , Gary D. Hachtel , Enrico Macii , Bernard Plessier , Fabio Somenzi, Algorithms for approximate FSM traversal, Proceedings of the 30th international conference on Design automation, p.25-30, June 14-18, 1993, Dallas, Texas, United States [doi>10.1145/157485.164555]
• 7: [7] H. Cho and F. Somenzi. Sequential logic optimization based on state space decomposition. In Proceedings of the European Conference on Design Automation, pages 200-204, Paris, France, Feb. 1993.
• 8: Olivier Coudert , Christian Berthet , Jean Christophe Madre, Verification of Synchronous Sequential Machines Based on Symbolic Execution, Proceedings of the International Workshop on Automatic Verification Methods for Finite State Systems, p.365-373, June 12-14, 1989
• 9: [9] O. Coudert, C. Berthet, and J. C. Madre. Verification of sequential machines using Boolean functional vectors. In L. Claesen, editor, Proceedings IFIP International Workshop on Applied Formal Methods for Correct VLSI Design, pages 111-128, Leuven, Belgium, Nov. 1989.
• 10: [10] O. Coudert and J. C. Madre. A unified framework for the formal verification of sequential circuits. In Proceedings of the IEEE International Conference on Computer Aided Design, pages 126-129, Nov. 1990.
• 11: Daniel Geist , Ilan Beer, Efficient Model Checking by Automated Ordering of Transition Relation Partitions, Proceedings of the 6th International Conference on Computer Aided Verification, p.299-310, June 21-23, 1994
• 12: Shankar G. Govindaraju , David L. Dill , Alan J. Hu , Mark A. Horowitz, Approximate reachability with BDDs using overlapping projections, Proceedings of the 35th annual conference on Design automation, p.451-456, June 15-19, 1998, San Francisco, California, United States [doi>10.1145/277044.277169]
• 13: Ramin Hojati , Sriram C. Krishnan , Robert K. Brayton, Early Quantification and Partitioned Transition Relations, Proceedings of the 1996 International Conference on Computer Design, VLSI in Computers and Processors, p.12-19, October 07-09, 1996
• 14: Youpyo Hong , Peter A. Beerel , Luciano Lavagno , Ellen M. Sentovich, Don't care-based BDD minimization for embedded software, Proceedings of the 35th annual conference on Design automation, p.506-509, June 15-19, 1998, San Francisco, California, United States [doi>10.1145/277044.277183]
• 15: [15] Iscas benchmarks. URL: http://www.cbl.ncsu.edu/CBL- _Docs/iscas89.html.
• 16: HoonSang Jin , Andreas Kuehlmann , Fabio Somenzi, Fine-Grain Conjunction Scheduling for Symbolic Reachability Analysis, Proceedings of the 8th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, p.312-326, April 08-12, 2002
• 17: In-Ho Moon , Gary D. Hachtel , Fabio Somenzi, Border-Block Triangular Form and Conjunction Schedule in Image Computation, Proceedings of the Third International Conference on Formal Methods in Computer-Aided Design, p.73-90, November 01-03, 2000
• 18: In-Ho Moon , Jae-Young Jang , Gary D. Hachtel , Fabio Somenzi , Jun Yuan , Carl Pixley, Approximate reachability don't cares for CTL model checking, Proceedings of the 1998 IEEE/ACM international conference on Computer-aided design, p.351-358, November 08-12, 1998, San Jose, California, United States [doi>10.1145/288548.289053]
• 19: [19] I.-H. Moon, J. Kukula, T. Shiple, and F. Somenzi. Least fix-point MBM: Improved technique for approximate reachability. Presented at IWLS99, Lake Tahoe, CA, June 1999.
• 20: In-Ho Moon , James H. Kukula , Kavita Ravi , Fabio Somenzi, To split or to conjoin: the question in image computation, Proceedings of the 37th conference on Design automation, p.23-28, June 05-09, 2000, Los Angeles, California, United States [doi>10.1145/337292.337305]
• 21: [21] R. K. Ranjan, A. Aziz, R. K. Brayton, B. F. Plessier, and C. Pixley. Efficient BDD algorithms for FSM synthesis and verification. Presented at IWLS95, Lake Tahoe, CA, May 1995.
• 22: Richard Rudell, Dynamic variable ordering for ordered binary decision diagrams, Proceedings of the 1993 IEEE/ACM international conference on Computer-aided design, p.42-47, November 07-11, 1993, Santa Clara, California, United States
• 23: Thomas R. Shiple , Ramin Hojati , Alberto L. Sangiovanni-Vincentelli , Robert K. Brayton, Heuristic minimization of BDDs using don't cares, Proceedings of the 31st annual conference on Design automation, p.225-231, June 06-10, 1994, San Diego, California, United States [doi>10.1145/196244.196360]
• 24: [24] H. Touati, H. Savoj, B. Lin, R. K. Brayton, and A. Sangiovanni-Vincentelli. Implicit enumeration of finite state machines using BDD's. In Proceedings of the IEEE International Conference on Computer Aided Design, pages 130-133, Nov. 1990.
• 25: [25] Vis verification benchmarks. URL: http://vlsi.colorado.edu/~vis

INDEX TERMS

Primary Classification:
  I. Computing Methodologies
  I.4 IMAGE PROCESSING AND COMPUTER VISION
      I.4.0 General
          Subjects: Image processing software

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Model checking

  I. Computing Methodologies
  I.4 IMAGE PROCESSING AND COMPUTER VISION
        I.4.10 Image Representation
            Subjects: Hierarchical

General Terms:
Algorithms, Design, Performance

Keywords:
Model checking, image computation, Binary Decision Diagrams, Symbolic