From VHDL to efficient and first-time-right designs: a formal approach

ABSTRACT

In this article we provide a practical transformational approach to the synthesis of correct synchronous digital hardware designs from high-level specifications. We do this while taking into account the complete life cycle of a design from early prototype to full custom implementation. Besides time-to-market, both flexibility with respect to target architecture and efficiency issues are addressed by the methodology. The utilization of user-selected behavior-preserving transformation steps ensures first-time-right design while exploiting the experience, flexibility, and creativity of the designer.To ensure that design transformations are indeed behavior-preserving a novel mechanized approach to the specification and verification of design transformations on control data flow graphs which is independent of a specific behavioral model or graph size has been developed.As a demonstration of an industrial application we use a video processing algorithm needed for the conversion from a line-interlaced to progressively scanned video format. Both a video signal processor-based prototype implementation as well as a very efficient full custom implementation are developed starting from a single high-level behavioral specification of the algorithm in VHDL. Results are compared with those previously obtained using different tools and methodologies.

REFERENCES

• 1: AELTEN, F. V., ALLEN, J., AND DEVADAS, S. 1994. Event-based verification of synchronous globally controlled, logic designs against signal flow graphs. IEEE Trans. CAD of ICs. 13, (Jan.) 122-134.
• 2: Alfred V. Aho , Ravi Sethi , Jeffrey D. Ullman, Compilers: principles, techniques, and tools, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1986
• 3: ANGELO, C. 1994. Formal hardware verification in a silicon compilation enviroment by means of theorem proving. PhD Thesis, IMEC, Leuven.
• 4: Praveen Asthana, Jumping the technology s-curve, IEEE Spectrum, v.32 n.6, p.49-54, June 1995 [doi>10.1109/6.387142]
• 5: Carlo Basile , Alan P. Cavallerano , Michael S. Deiss , Robert Keeler , Jae S. Lim , Wayne C. Luplow , Woo H. Paik , Eric Petajan , Robert Rast , Glenn Reitmeier , Terrence R. Smith , Craig Todd, The U.S. HDTV standard—the grand alliance, IEEE Spectrum, v.32 n.4, p.36-45, April 1995 [doi>10.1109/6.375998]
• 6: Karl S. Brace , Richard L. Rudell , Randal E. Bryant, Efficient implementation of a BDD package, Proceedings of the 27th ACM/IEEE conference on Design automation, p.40-45, June 24-27, 1990, Orlando, Florida, United States [doi>10.1145/123186.123222]
• 7: BRAYTON, R. K., CAMPOSANO, R., DE MICHELI, G., OTTEN, R. H. J. M., AND VAN EIJNDHOVEN, J. T. J. 1988. The Yorktown Silicon Compiler System, D. Gajski, Ed. Addison-Wesley, Reading, MA.
• 8: Robert W. Brodersen, Anatomy of a Silicon Compiler, Kluwer Academic Publishers, Norwell, MA, 1992
• 9: R. Camposano, Behavior-preserving transformations for high-level synthesis, Proceedings of the Mathematical Sciences Institute workshop on Hardware specification, verification and synthesis: mathematical aspects, p.106-128, February 1990, Ithaca, New York, United States
• 10: CAMPOSANO, R., AND TABET, R.M. 1989. Design representation for the synthesis of behavioral VHDL models. In Proceedings of the 9th International Conference on CHDL, J. A. Darringer and F. J. Ramming, Eds. Elsevier Science, Amsterdam, 49-58.
• 11: Viraphol Chaiyakul , Daniel D. Gajski , Loganath Ramachandran, High-level transformations for minimizing syntactic variances, Proceedings of the 30th international conference on Design automation, p.413-418, June 14-18, 1993, Dallas, Texas, United States [doi>10.1145/157485.164956]
• 12: CHANDRAKASAN, A., POTKONJAK, M., RABAEY, J., AND BRODERSON, R. 1992. An approach for power minimization using transformations, In Proceedings of the IEEE VLSI Signal Processing Workshop, 41-50.
• 13: CHANDRAKASAN, A. P., POTKONJAK, M., MEHRA, R., RABAEY, J., AND BRODERSON, R. W. 1995. Optimizing power using transformations. In IEEE Trans. Comput. Aided Des. Int. Circuits Syst. 14, (Jan.) 12-31.
• 14: COMPUTER GENERAL ELECTRONIC DESIGN, 1990. The ELLA Language Reference Manual, The New Church, Henry St. Bath, U.K., Issue 4.0.
• 15: David Cyrluk , S. Rajan , Natarajan Shankar , Mandayam K. Srivas, Effective Theorem Proving for Hardware Verification, Proceedings of the Second International Conference on Theorem Provers in Circuit Design - Theory, Practice and Experience, p.203-222, September 26-28, 1994
• 16: CYRLUK, D. 1993. Microprocessor Verification in PVS: A methodology and simple example, SRI-CSL-93-12, Tech. Rep. Computer Sci. Lab., SRI International, Menlo Park, CA, Dec.
• 17: DE MAN, H., RABAEY, J., SIX, P., AND CLAESEN, L. 1986. Cathedral-II: A silicon compiler for digital signal processing. IEEE Des. Test 3, 6 (Dec.), 13-125.
• 18: ENGELEN, W., MIDDELHOEK, P. F. A., HuIJS, C., HOFSTEDE, J., AND KROL, T. 1993. Applying Software Transformations to SIL. SPRITE deliverable LS.a.5.2/UT/Y5/M6/1A, June.
• 19: EVEKING, H. 1987. Verification, synthesis and correctness-preserving transformations-- Cooperative approaches to correct hardware design. In HDL Descriptions to Quaranteed Correct Circuit Designs, S. Borrione, Ed. Elsevier Science, Amsterdam.
• 20: FOURMAN, M. P. 1990. Formal system design, In Formal Methods for VLSI Design, J. Staunstrup, Ed. North-Holland, Amsterdam.
• 21: FRANSSEN, F., NACHTERGAELE, L., SAMSOM, H., CATTHOOR, F., AND DE MAN, H. 1994. Control flow optimization for fast system simulation and storage minimization, In Proceedings of EDTC 1994, (Paris, Feb.) 20-24.
• 22: Daniel D. Gajski , Loganath Ramachandran, Introduction to High-Level Synthesis, IEEE Design & Test, v.11 n.4, p.44-54, October 1994 [doi>10.1109/54.329454]
• 23: HALLBERG, g., AND PENG, Z. 1995. Synthesis under local timing constraints in the CAMAD high-level synthesis system. In Proceedings of IEEE EUROMICRO 95 (Como, Italy, Sept. 4-7), 650-655.
• 24: HANNA, F. K., LONGLEY, M., AND DAECHE, N. 1990. Formal synthesis of digital systems. In Formal VLSI Specification and Synthesis. L. J. M. Claesen, Ed. VLSI Design Methods, I, Elsevier, New York.
• 25: HENNESSY, g. 1995. Hardware/software codesign of processors: Concepts and example, Lecture notes NATO/ASI course on hardware software co-design, part I, Tremezzo, Italy, June.
• 26: HILFINGER, P.N. 1985. Silage: a high-level language and silicon compiler for digital signal processing. In Proceedings of IEEE Custom Integrated Circuits Conference, (Portland, OR, May) 213-216.
• 27: HuIJS, C., HOFSTEDE, J., AND KROL, T. 1992. SIL: a useful interface between specifications and silicon compilers. In Proceedings of the ProRISC / IEEE Workshop on CSSP (Houthalen, April) 99-104.
• 28: HuIJS, C., AND KROL, TH. 1994. A formal semantic model to fit SIL for transformational design. In Proceedings of2Oth Euromicro Conference, (Liverpool, Sept.) 100-107.
• 29: Zia Iqbal , Miodrag Potkonjak , Sujit Dey , Alice Parker, Critical path minimization using retiming and algebraic speed-up, Proceedings of the 30th international conference on Design automation, p.573-577, June 14-18, 1993, Dallas, Texas, United States [doi>10.1145/157485.165046]
• 30: JANSSEN, G. 1993. ROBDD software. Dept. of Electrical Engineering, Technical Univ. of Eindhoven, Eindhoven, Netherlands, Oct.
• 31: Martin Janssen , Francky Catthoor , Hugo De Man, A specification invariant technique for operation cost minimisation in flow-graphs, Proceedings of the 7th international symposium on High-level synthesis, p.146-151, May 18-20, 1994, Niagra-on-the-Lake, Ontario, Canada
• 32: Steven D. Johnson, Synthesis of Digital Design from Recursive Equations, MIT Press, Cambridge, MA, 1984
• 33: JONES, G., AND SHEERAN, M. 1990. Circuit design in Ruby, formal methods for VLSI design. (Summer School, Lyngby, Denmark, Sept.), North-Holland, Amsterdam.
• 34: JOZWIAK, L. 1995. An efficient verification method for application in transformational design. In Proceedings of Euromicro 95, (Como, Italy, Sept.) 118-129.
• 35: KLOOSTERHUIS, W. E. H., EYCKMANS, M. M. R., HOFSTEDE, J., HuIJS, C., KROL, TH., MCARDLE, O. P., SMITE, W. J. M., AND SVENSSON, L. G. L. 1993. SIL-2 language report. SPRITE deliverable LS.a.a/Philips/Y3-M 12/2.
• 36: KLOOSTERHUIS, W. E. H., EYCKMANS, M. M. R., KROL, TH., MCARDLE, O. P., AND SMITE, W. J. M. 1993. SIL-2 language report. SPRITE deliverable LS.a.2/Philips/Y3-M12/1.
• 37: KROL, T., VAN MEERBERGEN, J., NIESSEN, C., EMITS, W., AND HUISKEN, J. 1992. The Sprite input language: An intermediate format for high-level synthesis. In Proceedings of EDAC 92, (Brussels, Mar.) 186-192.
• 38: S. Y. Kung, VLSI array processors, Prentice-Hall, Inc., Upper Saddle River, NJ, 1987
• 39: LEE, E. A., AND PARKS, T.M. 1995. Dataflow process networks. In Proceedings of the IEEE, 83, (May) 773-799.
• 40: LEE, M.H., KIM, J. H., LEE, J. S., RYU, K. K., AND SONG, D.I. 1994. A new algorithm for interlaced to progressive scan conversion based on directional correlations and its IC design. IEEE Trans. Consumer Elec., 40, 2, (May) 119-125.
• 41: LINCOLN, P., OWRE, S., RUSHBY, J., SHANKAR, N., AND VON HENKE, F. 1993. Eight papers on formal verification. Tech. Rep. SRI-CSL-93-4, Computer Science Lab., SRI International, Menlo Park, CA, May.
• 42: P. E. R. Lippens , J. L. van Meerbergen , A. van der Werf , W. F. J. Verhaegh , B. T. McSweeney , J. O. Huisken , O. P. McArdle, PHIDEO: a silicon compiler for high speed algorithms, Proceedings of the conference on European design automation, February 25-28, 1991, Amsterdam, The Netherlands
• 43: David B. Loveman, Program Improvement by Source-to-Source Transformation, Journal of the ACM (JACM), v.24 n.1, p.121-145, Jan. 1977 [doi>10.1145/321992.322000]
• 44: Michael C. McFarland, Formal analysis of correctness of behavioral transformations, Formal Methods in System Design, v.2 n.3, p.231-257, June 1993 [doi>10.1007/BF01384133]
• 45: MCFARLAND, M. C., AND PARKER, A.C. 1983. An abstract model of behavior for hardware descriptions. IEEE Trans. Comput. C-32, 7, (July)621-636.
• 46: MEKENKAMP, G. E., MIDDELHOEK, P. F. A., MOLENKAMP, E., HOFSTEDE, J., AND KROL, TH. 1996. A Syntax based VHDL to CDFG translation model for high-level synthesis. In Proceedings of VHDL International Users Forum (VIUF) (Santa Clara, Feb. 28) 89-97.
• 47: MIDDELHOEK, P. F.A. 1994a. Transformational design of digital signal processing applications. In Proceedings of the ProRISC/IEEE Workshop on CSSP, (Arnhem, Netherlands, Mar.) 176-180.
• 48: MIDDELHOEK, P. F. A. 1994b. Transformational design of a direction detector for the progressive scan conversion processor. CS Memorandum 94-64, Univ. of Twente, Netherlands, Oct.
• 49: P. F. A. Middelhoek, Arbitrary hardware software trade-offs, Proceedings of the Sixth IEEE International Workshop on Rapid System Prototyping (RSP'95), p.19, June 07-09, 1995
• 50: MIDDELHOEK, P. F.A. 1996. Transformations on loops and arrays. CS Memorandum 96, Univ. of Twente, Netherlands, to be published, 1996.
• 51: MIDDELHOEK, P. F. A., MEKENKAMP, G. E., MOLENKAMP, E., AND KROL, TH. 1995. A transformational approach to VHDL and CDFG based high-level synthesis: a case study. In Proceedings of the CICC 95, (Santa Clara, CA, May) 37-40.
• 52: DE MICHELI, G., Ku, D., MAILHOT, F., AND TRUONG, T. 1991. The Olympus synthesis system for digital design. Internal Report, Center for Integrated Systems, Stanford Univ., Stanford, CA.
• 53: MOLENKAMP, E., MEKENKAMP, G. E., HOFSTEDE, J., KROL, TH. 1995. SIL: an intermediate for syntax based VHDL synthesis. In Proceedings of the VIUF Spring 95, (San Diego, CA, Apr.) 5.5-5.9.
• 54: MUSGRAVE, a., AND HUGHES, R.B. 1995. Review of verification techniques. Lecture notes NATO/ASI course on hardware software codesign, part II, Tremezzo, Italy, June.
• 55: OWRE, S., SHANKAR, N., AND RUSHBY, J.M. 1993. User guide for the PVS specification and verification system, language, and proof checker (Beta release). Computer Science Laboratory, SRI International, Menlo Park, CA, Feb.
• 56: PENG, Z., KUCHCINSKI, K., AND LYLES, B. 1989. CAMAD: A unified data path/control synthesis environment, design methodologies for VLSI and computer architecture. D.A. Edwards, Ed. 53-67.
• 57: PENG, Z., AND KUCHCINSKI, K. 1994. Automated transformation of algorithms into registertransfer level implementations. IEEE Trans. Comput.-Aided Des. Integrated Circuits Syst. 13, 2, 150-166.
• 58: PIGUET, C. 1989. Design methodologies and CAD tools. In Proceedings of the CICC 89 (San Diego, CA, May 15-19) 19.3.1-19.3.4.
• 59: POTKONJAK, M., AND RABAEY, g. 1994. Optimizing resource utilization using transformations. IEEE Trans. Comput.-Aided Des. Integrated Circuits Syst. 13, 3 (Mar.).
• 60: Roger S. Pressman, Software engineering (3rd ed.): a practitioner's approach, McGraw-Hill, Inc., New York, NY, 1992
• 61: RABAEY, J., AND HOANG, P. 1990. HYPER flowgraph policy, Version 1.2. Internal document Univ. of California, Berkeley, Mar.
• 62: RAJAN, S.P. 1995. Correctness of transformations in high-level synthesis. In Proceedings of the IFIP International Conference on CHDL (Chiba, Japan, Aug.) 597-603
• 63: Sreeranga Prasannakumar Rajan, Transformations on dependency graphs: formal specification and efficient mechanical verification, University of British Columbia, Vancouver, BC, Canada, 1996
• 64: S. Rajan , Natarajan Shankar , Mandayam K. Srivas, An Integration of Model Checking with Automated Proof Checking, Proceedings of the 7th International Conference on Computer Aided Verification, p.84-97, July 03-05, 1995
• 65: ROSSEN, L. 1990. Formal Ruby. Formal Methods for VLSI Design, J. Staunstrup, Ed., North-Holland, Amsterdam.
• 66: SAHRAOUI, Z., AND RIJNDERS, L. 1992. Report on the DIRDET experiments. Internal Report IMEC.
• 67: SAMSOM, H., CLAESEN, L., AND DE MAN, H. 1993. SynGuide: An environment for doing interactive correctness preserving transformations. In Proceedings of VLSI Signal Processing VI, L. D. J. Eggermont, P. Dewilde, E. Deprettere and J. van Meerbergen, Eds. IEEE, 269-277.
• 68: SAMSOM, H. 1995. Formal verification and transformation of video and image specifications, Ph.D. Thesis, IMEC/Univ. of Leuven.
• 69: SAMSOM, H., FRANSSEN, F., CATTHORR, F., AND DE MAN, H. 1994. Verification of loop transformations for real time signal processing applications. In Proceedings of VLSI Signal Processing VII (La Jolla, CA, Oct. 26-28), IEEE, 208-217.
• 70: SHANKAR, N., OWRE, S., AND RUSHBY, J. M. 1993. The PVS proof checker: A reference manual (Beta Release). Computer Science Laboratory, SRI International, Menlo Park, CA, Feb.
• 71: STOY, E., AND PENG, Z. 1994. A design representation for hardware/software co-synthesis. In Proceedings of IEEE Euromicro (Liverpool, Sept.) 192-199.
• 72: D. E. Thomas , E. M. Dirkes , R. A. Walker , J. V. Rajan , J. A. Nestor , R. L. Blackburn, The system architect's workbench, Proceedings of the 25th ACM/IEEE conference on Design automation, p.337-343, June 12-15, 1988, Atlantic City, New Jersey, United States
• 73: W. D. Tiedemann , S. Lenk , C. Grobe , W. Grass, Introducing structure into behavioural descriptions obtained from timing diagram specifications, Nineteenth EUROMICRO symposium on microprocessing and microprogramming on Open system design : hardware, software and applications: hardware, software and applications, p.581-588, September 1993, Barcelona, Spain
• 74: VAN ROERMUND; A. H. M., SNIJDER, P. J., DIJKSTRA, H., HEMERYCK, C. G., HUIZER, C. M., SCHMITZ, J. M. P. SLNIJTER, R. J. 1989. A general-purpose programmable video signal processor. IEEE Trans, Cons. Elec., 35, 3, Aug., 249-258.
• 75: VEMURI, R. 1990. How to proof the completeness of a set of register level design transformations, In Proceedings of the 27th DAC, ACM/IEEE, June, 207-212.
• 76: THE INSTITUTE OF ELECTRICAL AND ELECTRONICS ENGINEERS, 1988. IEEE Standard VHDL Language Reference Manual, IEEE std. IEEE Press, New York. 1076-1088.
• 77: Robert A. Walker , Samit Chaudhuri, Introduction to the Scheduling Problem, IEEE Design & Test, v.12 n.2, p.60-69, June 1995 [doi>10.1109/54.386007]
• 78: WALKER, R. A., AND THOMAS, D.E. 1989. Behavioral transformation for algorithmic level IC design. IEEE Trans. CAD 8, 10 (Oct.), 1115-1128.
• 79: WOUDSMA, R., BEENKER, F., VAN MEERBERGEN, J., AND NIESSEN, C. 1990. Piramid: an architecture-driven silicon compiler for complex DSP applications. In Proceedings of IEEE International Symposium on Circuits and Systems, 2696-2700.

INDEX TERMS

Primary Classification:
  B. Hardware
  B.6 LOGIC DESIGN
      B.6.3 Design Aids

          Nouns: VHDL

Additional Classification:
  B. Hardware
  B.5 REGISTER-TRANSFER-LEVEL IMPLEMENTATION
      B.5.1 Design
          Subjects: Data-path design; Styles (e.g., parallel, pipeline, special-purpose); Control design; Arithmetic and logic units
      B.5.2 Design Aids
          Subjects: Verification; Optimization; Automatic synthesis; Hardware description languages
  B.6 LOGIC DESIGN
      B.6.3 Design Aids
          Subjects: Optimization; Automatic synthesis; Hardware description languages; Verification

  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Correctness proofs
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications
          Subjects: Data-flow languages; Applicative (functional) languages

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Mechanical verification
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Mechanical theorem proving

  J. Computer Applications
  J.6 COMPUTER-AIDED ENGINEERING
      Subjects: Computer-aided design (CAD)

General Terms:
Design, Human Factors, Languages, Theory, Verification

Keywords:
CDFG, SFG, VHDL, correctness by construction, design methodology, rapid system prototyping, transformational design