Cited By
View all- Nicoli FPierre LMermet J(1994)Formal verification of behavioral VHDL specificationsProceedings of the conference on European design automation10.5555/198174.198328(560-565)Online publication date: 23-Sep-1994
Correct interactive transformational synthesis of DSP hardware
Abstract
We present a new interactive tool for the guided synthesis of digital signal processing hardware. The tool is driven from a HDL. It will suggest different ways of implementing different architectures for the same specification, maintaining the correctness of implementations during the design process. The tool will automatically generate input for the Boyer Moore theorem prover from the HDL specification in order to verify the correctness of the implementations.
References
[1]
{Bo88} Boyer, R. S., Moore, J. S. A Computational Logic Handbook. Academic Press, 1988.
[2]
{Br88} Brayton, R. K., Camposano, R., DeMicheli, G., Otten, R. H, vanEijndhoven, J. The Yorktown Silicon Compiler. In: "Silicon Compilation", Gajski, (Ed), Addison Wesley, 1988.
[3]
{Ca84} Campbell, R. H., Koelmans, A. M., McLauchlan, M. R. STRICT: a design language for strongly typed recursive integrated circuits. IEE Proc. Vol 132, Pts E and I, No 2, 1985.
[4]
{Ca88} Camposano, R. Behavior-preserving transformations for High Level Synthesis, Lecture Notes in Computer Science 408, Springer Verlag, pp. 106--128.
[5]
{De86} DeMan, H., Rabaey, J., Six, P., Claesen, L. Cathedral II: A Silicon Compiler for Digital Signal Processing. IEEE Design and Test, Vol 3, No 6, Dec. 1986.
[6]
{De89} Denyer, B. P. SAGE, A Methodology and Toolset for Architectural Synthesis. Technical Report, Department of Electrical Engineering, Edinburgh University, 1989.
[7]
{E189} Elmasry, M. I., Buset, O. A. ACE, A Hierarchical Graphical Interface for Architectural Synthesis. Proc. 26th ACM/IEEE Design Aut. Conf., 1989.
[8]
{Fi89} Finn, M., Fourman, M. P., Francis, M., Harris, R. Formal System Design-Interactive synthesis based on Computer-Assisted Formal Reasoning. Proc. IFIP workshop "Applied Formal Methods for Correct VLSI Design", Belgium, 1989.
[9]
{Hu85} Hunt, W. FM8501: A Verified Microprocessor. PhD Thesis, University of Texas at Austin, 1985.
[10]
{IE87} IEEE Standard VHDL Language Reference Manual, IEEE Press, 1987.
[11]
{Ka88}. Kalker, T. HOL Semantics for DSP, Philips Research Labs Technical Report, Eindhoven, The Netherlands, 1988.
[12]
{Mc88} McFarland, S. J., Parker, A. C., Camposano, R. Tutorial on High Level Synthesis. Proc. 25th ACM/IEEE Design Aut. Conf., IEEE, 1988.
[13]
{Pi89a} Pierre, L. The formal proof of the "min-max" sequential benchmark described in CASCADE using the Boyer--Moore theorem prover. Proc. IFIP workshop "Applied Formal Methods for Correct VLSI Design", Belgium, 1989.
[14]
{Pi89b} Pierre, L. The formal proof of sequential circuits described in CASCADE using the Boyer-Moore Theorem Prover. Proc. IFIP workshop "Applied Formal Methods for Correct VLSI Design", Belgium, 1989.
[15]
{Ve88} Verkest, D., Johannes, P., Claesen, L., DeMan, H. Formal Techniques for Proving Correctness of Parameterized Hardware using Correctness Preserving Transformations. In Proc. IFIP workshop "The Fusion of Hardware Design and Verification". North Holland, 1988.
- Correct interactive transformational synthesis of DSP hardware
Recommendations
Hardware/software co-design for DSP applications via the HMS framework
ICASSP '96: Proceedings of the Acoustics, Speech, and Signal Processing, 1996. on Conference Proceedings., 1996 IEEE International Conference - Volume 02The design of computer systems that incorporate both standardized off-the-shelf processors, or software, as well as specialized hardware is referred to as hardware/software (hw/sw) co-design. This paper studies the problem and presents a system, the ...
Synthesis of pipelined DSP accelerators with dynamic scheduling
ISSS '95: Proceedings of the 8th international symposium on System synthesisAbstract: To construct complete systems on silicon, application specific DSP accelerators are needed to speed up the execution of high throughput DSP algorithms. In this paper, a methodology is presented to synthesize high throughput DSP functions into ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
February 1991
577 pages
ISBN:0818621303
- Conference Chair:
- Tony Ambler,
- General Chair:
- Jochen Jess,
- Program Chair:
- Hugo De Man
Sponsors
- EDAC Association
- SIGDA: ACM Special Interest Group on Design Automation
Publisher
IEEE Computer Society Press
Washington, DC, United States
Publication History
Published: 25 February 1991
Check for updates
Qualifiers
- Article
Upcoming Conference
DAC '25
- Sponsor:
- sigda
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- View Citations1Total Citations
- 104Total Downloads
- Downloads (Last 12 months)13
- Downloads (Last 6 weeks)2
Reflects downloads up to 26 Sep 2024
Other Metrics
Citations
Cited By
View all- Nicoli FPierre LMermet J(1994)Formal verification of behavioral VHDL specificationsProceedings of the conference on European design automation10.5555/198174.198328(560-565)Online publication date: 23-Sep-1994
View Options
Get Access
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in