A methodology for generating verified combinatorial circuits

Oleg Evgenievich Kiselyov, Kedar N. Swadi, Walid Taha

研究成果: Conference contribution

35 被引用数 (Scopus)

抄録

High-level programming languages offer significant expressivity but provide little or no guarantees about resource use. Resource-bounded languages - such as hardware-description languages provide strong guarantees about the runtime behavior of computations but often lack mechanisms that allow programmers to write more structured, modular, and reusable programs. To overcome this basic tension in language design, recent work advocated the use of Resource-aware Programming (RAP) languages, which take into account the natural distinction between the development platform and the deployment platform for resource-constrained software. This paper investigates the use of RAP languages for the generation of combinatorial circuits. The key challenge that we encounter is that the RAP approach does not safely admit a mechanism to express a posteriori (post-generation) optimizations. The paper proposes and studies the use of abstract interpretation to overcome this problem. The approach is illustrated using an in-depth analysis of the Fast Fourier Transform (FFT). The generated computations are comparable to those generated by FFTW.

本文言語English
ホスト出版物のタイトルEMSOFT 2004 - Fourth ACM International Conference on Embedded Software
ページ249-258
ページ数10
出版ステータスPublished - 2004 12 1
外部発表はい
イベントEMSOFT 2004 - Fourth ACM International Conference on Embedded Software - Pisa, Italy
継続期間: 2004 9 272004 9 29

出版物シリーズ

名前EMSOFT 2004 - Fourth ACM International Conference on Embedded Software

Other

OtherEMSOFT 2004 - Fourth ACM International Conference on Embedded Software
CountryItaly
CityPisa
Period04/9/2704/9/29

ASJC Scopus subject areas

  • Engineering(all)

フィンガープリント 「A methodology for generating verified combinatorial circuits」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

引用スタイル