Interactive presentation: Automatic hardware synthesis from specifications: a case study

ABSTRACT

We propose to use a formal specification language as a high-level hardware description language. Formal languages allow for compact, unambiguous representations and yield designs that are correct by construction. The idea of automatic synthesis from specifications is old, but used to be completely impractical. Recently, great strides towards efficient synthesis from specifications have been made. In this paper we extend these recent methods to generate compact circuits and we show their practicality by synthesizing an arbiter for ARM's AMBA AHB bus and a generalized-buffer from specifications given in PSL. These are the first industrial examples that have been synthesized automatically from their specifications.

REFERENCES

• 1: ARM Ltd. AMBA Specification (Rev. 2). Available from www.arm.com, 1999.
• 2: J. Büchi and L. Landweber. Solving sequential conditions by finite-state strategies. Trans. Amer. Math. Soc., 138:295--311, 1969.
• 3: A. Church. Logic, arithmetic and automata. In Proc. 1962 Int. Congr. Math., pages 23--25, 1963.
• 4: Cindy Eisner , Dana Fisman, A Practical Introduction to PSL (Series on Integrated Circuits and Systems), Springer-Verlag New York, Inc., Secaucus, NJ, 2006
• 5: A. Harding, M. Ryan, and P. Schobbens. A new algorithm for strategy synthesis in LTL games. In Tools and Algorithms for the Construction and the Analysis of Systems, pages 477--492, 2005.
• 6: Barbara Jobstmann , Roderick Bloem, Optimizations for LTL Synthesis, Proceedings of the Formal Methods in Computer Aided Design, p.117-124, November 12-16, 2006 [doi>10.1109/FMCAD.2006.22]
• 7: 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
• 8: O. Kupferman , M. Y. Vardi, Freedom, Weakness, and Determinism: From Linear-Time to Branching-Time, Proceedings of the 13th Annual IEEE Symposium on Logic in Computer Science, p.81, June 21-24, 1998
• 9: I. Pill , S. Semprini , R. Cavada , M. Roveri , R. Bloem , A. Cimatti, Formal analysis of hardware requirements, Proceedings of the 43rd annual conference on Design automation, July 24-28, 2006, San Francisco, CA, USA [doi>10.1145/1146909.1147119]
• 10: N. Piterman, A. Pnueli, and Y. Sa'ar. Synthesis of reactive(1) designs. In Conference on Verification, Model Checking, and Abstract Interpretation, pages 364--380, 2006.
• 11: A. Pnueli , R. Rosner, On the synthesis of a reactive module, Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.179-190, January 11-13, 1989, Austin, Texas, United States [doi>10.1145/75277.75293]
• 12: Michael Oser Rabin, Automata on Infinite Objects and Church's Problem, American Mathematical Society, Boston, MA, 1972
• 13: Ellen Sentovich , Kanwar Jit Singh , Cho W. Moon , Hamid Savoj , Robert K. Brayton , Alberto L. Sangiovanni-Vincentelli, Sequential Circuit Design Using Synthesis and Optimization, Proceedings of the 1991 IEEE International Conference on Computer Design on VLSI in Computer & Processors, p.328-333, October 11-14, 1992
• 14: F. Somenzi. CUDD: CU Decision Diagram Package. University of Colorado at Boulder, ftp://vlsi.colorado.edu/pub/.
• 15: Fabio Somenzi , Roderick Bloem, Efficient Büchi Automata from LTL Formulae, Proceedings of the 12th International Conference on Computer Aided Verification, p.248-263, July 15-19, 2000