Skip to main content
Log in

An Erratum to this article was published on 01 December 1993

Abstract

Bedroc is a digital hardware synthesis system that automatically translates a behavioral description written in a hardware description language to field programmable gate arrays.Bedroc allows designers to specify their designs at a very high level of abstraction, and compile them into designs that can be realized in one of many different technologies. It can synthesize a wide variety of synchronous designs including signal processing applications, arithmetic applications, and general purpose processors. An additional aim of theBedroc project is to incorporate formal methods into the hardware synthesis process. By verifying the algorithms used for synthesis instead of the synthesized designs, we give the designer many of the benefits of formal methods without their having to learn new techniques. We have usedBedroc to synthesize several circuits from the High Level Synthesis Workshop benchmarks, including a wave digital elliptic filter.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Similar content being viewed by others

References

  1. Paul Stanford and Paul Mancuso,Electronic Design Interchange Format Version 2 00, Electronic Industries Organization, second edition, 1989.

  2. High Level Synthesis Workshop, “High level synthesis workshop benchmark set,” 1991, Obtained by ftp from mcnc .org.

  3. Chia-Jeng Tseng and Daniel P. Siewiorek, “Automated synthesis of data paths in digital systems,”IEEE Transaction on Computer-Aided Design, vol. CAD-5, pp. 379–395, 1986.

    Article  Google Scholar 

  4. P. Dewilde, E. Deprettere and R. Nouta, “Parallel and pipelined VLSI implementation of signal processing algorithms,” S.Y. Kung, H.J. Whitehouse and T. Kailath, eds.,VLSI and Modern Signal Processing, Englewood Cliffs, NJ: Prentice-Hall, 1985, Chap. 15, pp. 257–275.

    Google Scholar 

  5. Houria Oudghiri and Bozena Kaminska, “Global weighted scheduling and allocation algorithms,”Proceedings of 1992 European Design Automation Conference, IEEE Computer Society Press, Los Alamitas, CA, March 1992.

    Google Scholar 

  6. Srinivas Devadas and Richard Newton, “Algorithms for hardware allocation in datapath synthesis,”IEEE Transactions on CAD, CAD-7, pp. 768–781, 1989.

    Article  Google Scholar 

  7. L. Claesen, F. Cathoor, D. Lanneer, G. Goossens, S. Note, J. Van Neerbergen and H. De Man, “Automatic synthesis of signal processing benchmark using the CATHEDRAL silicon compilers,”Custom Integrated Circuits Conference, pp. 14.7.1–14.7.4 IEEE Press, New York, NY, 1988.

    Google Scholar 

  8. R.L. Constableet al, Implementing Mathematics with the Nuprl Proof Development System, Englewood Cliffs, NJ: Prentice Hall, 1986.

    Google Scholar 

  9. M.J.C. Gordon, “Why higher-order logic is a good formalism for specifying and verifying hardware,” G.J. Milne and P.A. Subrahmanyam, eds.,Formal Aspects of VLSI Design, Amsterdam: North-Holland, 1986.

    Google Scholar 

  10. Michael C. McFarland, “A practical application of verification to high-level synthesis,” P.A. Subramanyam, ed.,International Workshop on Formal Methods in VLSI Design, ACM, New York, NY, 1991.

    Google Scholar 

  11. M.E. Leeser and G.M. Brown,Proceedings of the MSI Workshop on Hardware Specification, Verification and Synthesis: Mathematical Aspects, Berlin/New York: Springer Verlag, 1990.

    Book  Google Scholar 

  12. Richard Chapman, Geoffrey Brown, and Miriam Leeser, “Verified high-level synthesis in BEDROC,”Proceedings of the 1992 European Design Automation Conference, IEEE Computer Society Press, Los Alamitas, CA, March 1992.

    Google Scholar 

  13. Mark Aagaard and Miriam Leeser, “Verifying a logic synthesis tool in Nuprl,”Workshop on Computer-Aided Verification, June 1992.

  14. Michael C. McFarland, Alice C. Parker and Raul Camposano, “The high-level synthesis of digital systems,”Proceedings of the IEEE, vol. 78, pp. 301–318, 1990.

    Article  MATH  Google Scholar 

  15. R. Camposano and W. Rosenstiel, “Synthesizing circuits from behavioral descriptions,”IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, vol. CAD-8, pp. 171–180, 1989.

    Article  Google Scholar 

  16. Giovanni De Micheli, David Ku, Frederic Mailhot and Thomas Truang, “The Olympus synthesis system,”IEEE Design and Test of Computers, pp. 37–53, October 1990.

  17. D.E. Thomas, E.M. Dirkes, R.A. Walker, J.V. Rajan, J.A. Nestor and R.L. Blackburn, “The system architect's workbench,”25th Design Automation Conference, pp. 337–343. IEEE Computer Society Press, Los Alamitas, CA, 1988.

    Google Scholar 

  18. J. Rabaey, H. De Man, J. Vanhoof, G. Goossens and F. Catthoor, “Cathedral II: A synthesis system for multiprocessor DSP systems,” Daniel D. Gajski, ed.,Silicon Compilation, Reading, MA: Addison-Wesley, 1988.

    Google Scholar 

  19. Chee-Keng Chang, Geoffrey Brown and Miriam Leeser, “EDISYN: A language-based editor for high-level synthesis,”Tenth International Symposium on Computer Hardware Description Languages, April 1991.

  20. I. Page and W. Luk, “Compiling Occam into FPGAs,” W. Moore and W. Luk, eds.,FPGAs, pp. 271–283, Abingdon: EE & CS Books, 1991.

    Google Scholar 

  21. Keshav Pingali, Micah Beck, Richard Johnson, Mayan Moudgill and Paul Stodghill, “Dependence Flow Graphs: An algebraic approach to program dependencies,”Proceedings of the 18th ACM Symposium on Principles of Programming Languages, 1991.

  22. M.C. McFarland, “The Value Tree: A database for automated digital design,” Master's thesis, Carnegie-Mellon University, December 1978.

  23. Alex Orailoglu and Daniel Gajski, “Flow graph representation,”Proceedings of 23rd Design Automation Conference, pp. 503–509. IEEE, 1986.

  24. Mark Genoe, Luc Claesen, Eric Verlind, Frank Proesmans, and Hugo De Man, “Automatic formal verification of Cathedral-II circuits from transistor switch level implementation up to high level behavioral specifications by thesfg tracing methodology,”Proceedings of the 1992 European Design Automation Conference, IEEE Press, March 1992.

  25. Luc Claesen, Frank Proesmans, Eric Verlind and Hugo De Man, “SFG-Tracing: a methodology for the automatic verification of MOS transistor level implementations from high level behavioral specifications,” P.A. Subrahmanyam, ed., 1992International Workshop on Formal Methods in VLSI Design, 1991.

  26. Jos T.V. Eijndhoven and Leon Stok, “A data flow graph exchange format,”Proceedings of 1992 European Design Automation Conference, IEEE Press, March 1992.

  27. Miriam Leeser, Mark Aagaard, Mark Linderman, Richard Chapman, Richard Johnson and Stephan Meier, “The BEDROC high level synthesis system,”ASIC'91. IEEE, September 1991.

  28. P. Marwedel, “A new synthesis algorithm for the MIMOLA software system,” 23rd Design Automation Conference, pp. 271–277. ACM/IEEE, 1986.

  29. M.C. McFarland, “BUD: Bottom-up design of digital systems,” 23rd Design Automation Conference, pp. 474–479. ACM/IEEE, 1986.

  30. Alice C. Parker, Jorge Pizarro and Mitch Mlinar, “MAHA: A program for datapath synthesis,”23rd Design Automation Conference, pp. 461–466. ACM/IEEE, 1986.

  31. P.G. Paulin and J.P. Knight, “Force-directed scheduling in automatic datapath synthesis,”24th Design Automation Conference, pp. 195–202. ACM/IEEE, 1987.

  32. W.F.J. Verhaegh, E.H.L. Aarts, J.H.M. Korst and P.E.R. Lip-pens, “Improved force-directed scheduling,” InProceedings of the 1992 European Design Automation Conference, IEEE Press, March 1992.

  33. Pierre G. Paulin and John P. Knight, “Scheduling and binding algorithms for high-level synthesis,” 26th Design Automation Conference, ACM/IEEE, 1989.

  34. Richard E. Korf, “Real-time heuristic search: First results,”AAA1-87 Sixth National Conference on Artificial Intelligence, pp. 133–138, 1987.

  35. Miriam Leeser and Stephan Meier, “Hardware scheduling with Real-Time A* search, “Proceedings of the Fifth International Workshop on High-Level Synthesis, 1991.

  36. R.K. Brayton and C. McMullen, “Decomposition and factorization of Boolean expressions,”International Symposium on Circuits and Systems, 1982.

  37. Mark Aagaard and Miriam Leeser, “The implementation and proof of a Boolean simplification system,” Geraint Jones and Mary Sheeran, eds.,Designing Correct Circuits, Oxford 1990, Berlin/New York: Springer-Verlag, 1991.

    Google Scholar 

  38. Mark Aagaard and Miriam Leeser, “A formally verified system for logic synthesis,”International Conference on Computer Design, IEEE, October 1991.

  39. R.K. Brayton, R. Rudell, et al., “MIS: A multiple-level logic optimization system,”IEEE Transactions on Computer-Aided Design, vol. CAD-6, 1987.

  40. G. Hachtel, R. Jacoby, K. Keutzer and C. Morrison, “On the relationship between area optimization and multifault testability of multilevel logic,”International Conference on Computer Aided Design, pp. 316–319, ACM/IEEE, 1989.

  41. W. Luk and I. Page, “Parametrising designs for Field-Programmable Gate Arrays,” W. Moore and W. Luk, eds., FPGAs, pp. 284–295, Abingdon: EE & CS Books, 1991.

    Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Additional information

An erratum to this article is available at http://dx.doi.org/10.1007/BF01608541.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Leeser, M., Chapman, R., Aagaard, M. et al. High level synthesis and generating FPGAs with the BEDROC system. J VLSI Sign Process Syst Sign Image Video Technol 6, 191–214 (1993). https://doi.org/10.1007/BF01607881

Download citation

  • Received:

  • Revised:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/BF01607881

Keywords

Navigation