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.
Similar content being viewed by others
References
Paul Stanford and Paul Mancuso,Electronic Design Interchange Format Version 2 00, Electronic Industries Organization, second edition, 1989.
High Level Synthesis Workshop, “High level synthesis workshop benchmark set,” 1991, Obtained by ftp from mcnc .org.
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.
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.
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.
Srinivas Devadas and Richard Newton, “Algorithms for hardware allocation in datapath synthesis,”IEEE Transactions on CAD, CAD-7, pp. 768–781, 1989.
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.
R.L. Constableet al, Implementing Mathematics with the Nuprl Proof Development System, Englewood Cliffs, NJ: Prentice Hall, 1986.
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.
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.
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.
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.
Mark Aagaard and Miriam Leeser, “Verifying a logic synthesis tool in Nuprl,”Workshop on Computer-Aided Verification, June 1992.
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.
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.
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.
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.
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.
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.
I. Page and W. Luk, “Compiling Occam into FPGAs,” W. Moore and W. Luk, eds.,FPGAs, pp. 271–283, Abingdon: EE & CS Books, 1991.
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.
M.C. McFarland, “The Value Tree: A database for automated digital design,” Master's thesis, Carnegie-Mellon University, December 1978.
Alex Orailoglu and Daniel Gajski, “Flow graph representation,”Proceedings of 23rd Design Automation Conference, pp. 503–509. IEEE, 1986.
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.
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.
Jos T.V. Eijndhoven and Leon Stok, “A data flow graph exchange format,”Proceedings of 1992 European Design Automation Conference, IEEE Press, March 1992.
Miriam Leeser, Mark Aagaard, Mark Linderman, Richard Chapman, Richard Johnson and Stephan Meier, “The BEDROC high level synthesis system,”ASIC'91. IEEE, September 1991.
P. Marwedel, “A new synthesis algorithm for the MIMOLA software system,” 23rd Design Automation Conference, pp. 271–277. ACM/IEEE, 1986.
M.C. McFarland, “BUD: Bottom-up design of digital systems,” 23rd Design Automation Conference, pp. 474–479. ACM/IEEE, 1986.
Alice C. Parker, Jorge Pizarro and Mitch Mlinar, “MAHA: A program for datapath synthesis,”23rd Design Automation Conference, pp. 461–466. ACM/IEEE, 1986.
P.G. Paulin and J.P. Knight, “Force-directed scheduling in automatic datapath synthesis,”24th Design Automation Conference, pp. 195–202. ACM/IEEE, 1987.
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.
Pierre G. Paulin and John P. Knight, “Scheduling and binding algorithms for high-level synthesis,” 26th Design Automation Conference, ACM/IEEE, 1989.
Richard E. Korf, “Real-time heuristic search: First results,”AAA1-87 Sixth National Conference on Artificial Intelligence, pp. 133–138, 1987.
Miriam Leeser and Stephan Meier, “Hardware scheduling with Real-Time A* search, “Proceedings of the Fifth International Workshop on High-Level Synthesis, 1991.
R.K. Brayton and C. McMullen, “Decomposition and factorization of Boolean expressions,”International Symposium on Circuits and Systems, 1982.
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.
Mark Aagaard and Miriam Leeser, “A formally verified system for logic synthesis,”International Conference on Computer Design, IEEE, October 1991.
R.K. Brayton, R. Rudell, et al., “MIS: A multiple-level logic optimization system,”IEEE Transactions on Computer-Aided Design, vol. CAD-6, 1987.
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.
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.
Author information
Authors and Affiliations
Additional information
An erratum to this article is available at http://dx.doi.org/10.1007/BF01608541.
Rights 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
Received:
Revised:
Published:
Issue Date:
DOI: https://doi.org/10.1007/BF01607881