L. Nowak
ABSTRACT
This paper proposes a new method for hardware verification. The basic idea is the application of a retargetable compiler as verification tool. A retargetable compiler is able to compile programs into the machine code of a specified hardware (target). If the program is the complete behavioural specification of the target, the compiler can be used to verify that a properly programmed structure implements the behaviour. Methods, algorithms and applications of an existing retargetable compiler are described.
- Anc86.F. Aneeau: FORCE: A Formal Checker for Executability, in: D. Borrione (ed.): From HDL Descriptions to Guaranteed Correct Circuit Designs, Proc. of IFIP WG 10.2 Working Conf., North Holland, 1987Google Scholar
- Bab81.T. Baba, H. Hagiwara: The MPG System: A Machine-Independent Efficient Microprogram Generator, IEEE Trans.Comp., Vol. C- 30, 6(1981), pp. 373-395Google Scholar
- Eve81.H. Eveking: The Application of CONLAN Assertions to the Correct Description of Hardware, in: M. Breuer, R. Hartenstein (eds.): Proc. 5th IFIP Conf. on Computer Hardware Description Languages and Their Applications, North Holland, 1981, pp. 37-50Google Scholar
- Gan82.M. Ganapathi, C.N. Fisher, J.L. Hennessy: Retargetable Compiler Code Generation, ACM Computing Surveys, Vol. 14, 4(1982), pp. 573-593 Google ScholarDigital Library
- Gra87.W. Grass, R. Rauscher: CAMILOD: A Program System for Designing Digital Hardware with Proven Correctness, in: D. Borrione (ed.): From HDL Descriptions to Guaranteed Correct Circuit Designs, Proc. of IFIP WG 10.2 Working Conf., North Holland, 1987Google Scholar
- Krü86.G. Kriiger: Automatic Generation of Self- Test Programs- A New feature of the MI- MOLA Design System, Proc. 23rd Design Automation Conference, 1986, pp. 378-384 Google ScholarDigital Library
- Krü88.G. Krfiger: A Tool For Hierarchical Test Generation, Proc. ICCAD, 1988Google Scholar
- Mar84.P. Marwedel: The MIMOLA Design System: Tools for the Design of Digital Processors, 21st Design Automation Conference, 1984, pp. 587-593 Google ScholarDigital Library
- Mar84a.P. Marwedel: A Retargetable Compiler For A High-Level Microprogramming Language, 17th Annual Workshop on Microprogramming (MICRO-17), 1984, pp.267-274 Google ScholarDigital Library
- Mar86.P. Marwedel: A New Synthesis Algorithm for the MIMOLA Software System, Pro~. 23rd Design Automation Conference, 1986, pp. 271-277 Google ScholarDigital Library
- Mil86.G. Milne: Towards verifiably correct VLSI design, in: Milne, Subrahmanyam (eds.): Formals Aspects of VLSI Design, Proc. Workshop on VLS}, North Holland, 1986Google Scholar
- Mue83.R.A. Mueller, J. Varghese : Flow Graph Machine Models in Microcode Synthesis, 16th Annual Microprogramming Workshop (MICRO-16), 1983, pp. 159-167Google ScholarDigital Library
- Mue84.R.A. Mueller, J. Varghese, V.H. Allan : Global Methods in the Flow Graph Approach to Retargetable Microcode Generation, 17th Annual Microprogramming Workshop (MICRO-17), 1984, pp. 275-284 Google ScholarDigital Library
- Now87.L.Nowak : SAMP: A General Purpose Processor Based on a Self-Timed VLIW Structure, ACM Comp. Arch. News, Vol.15, No.4, Sep. 1987, pp. 32-39 Google ScholarDigital Library
- Now87a.L.Nowak : Graph Based Retargetable Microcode Compilation in the MIMOLA Design System, Proc. 20th Annual Workshop on Microprogramming (MICRO-20), Dec.1987, pp. 126-132 Google ScholarDigital Library
- Sch88.W. Schenk: Eine Prologimplementierung f~ir einen Rechner sehr grot3er Befehlsbreite, master's thesis, Institut ffir Informatik und Praktische Mathematik der Universit~t Kiel, 1988Google Scholar
- Tak84.S. Takagi : Rule Based Synthesis, Verification and Compensation of Data Paths, Proc. IEEE Conf.Comp.Design (ICCD'84), New York, Oct.1984, pp. 133-138Google Scholar
- Ueh81.T. Uehara, F. Maruyama, T. Saito, N. Kawato DDL Verifier, in: M.Breuer, R.Hartenstein (eds.): Proc. 5th IFIP Conf. on Computer Hardware Description Languages and Their Applications, North Holland, 1981, pp. 51-61Google Scholar
- Veg82.S.R. Vegdahl: Local Code Generation and Compaction in Optimizing Microcode Compilers, PhD thesis and report CMUCS-82-153, Carnegie-Mellon University, Pittsburgh, 1982 Google ScholarDigital Library
- Zim80.G. Zimmermann: MDS- The MIMOLA Design Method, Journal of Digital Systems, Vol.4, 3(1980), pp. 337-369Google Scholar
Index Terms
- Verification of hardware descriptions by retargetable code generation
Recommendations
Retargetable code generation for application-specific processors
Special issue: Parallel computing technologiesAn approach of intelligent retargetable compiler is introduced to overcome the gap between hardware and software development and to increase performance of embedded systems. It focuses on knowledgeable treatment of code generation where knowledge about ...
Retargetable code optimization with SIMD instructions
CODES+ISSS '06: Proceedings of the 4th international conference on Hardware/software codesign and system synthesisRetargetable C compilers are nowadays widely used to quickly obtain compiler support for new embedded processors and to perform early processor architecture exploration. One frequent concern about retargetable compilers, though, is their lack of machine-...
Retargetable code optimization for predicated execution
DATE '08: Proceedings of the conference on Design, automation and test in EuropeRetargetable C compilers are key components of today's embedded processor design platforms for quickly obtaining compiler support and performing early processor architecture exploration. The inherent problem of the retargetable compilation approach, ...
Comments