Invited: A Scalable Formal Approach for Correctness-Assured Hardware Design

被引：0
|
作者：
Yang, Jin [1 ]
Casas, Jeremy [1 ]
Yang, Zhenkun [1 ]
机构：
[1] Intel Corp, Intel Labs, Hillsboro, OR 97124 USA
来源：
2023 60TH ACM/IEEE DESIGN AUTOMATION CONFERENCE, DAC | 2023年
关键词：
D O I：
10.1109/DAC56929.2023.10247673
中图分类号：
TP18 [人工智能理论];
学科分类号：
081104 ; 0812 ; 0835 ; 1405 ;
摘要：
Correctness must be a first principle in hardware/-software co-design, especially for security and safety critical applications. We will give an overview of our scalable approach for correctness-assured hardware/software design at behavioral level, based on formalizing microarchitecture features as program transformations in an incremental compiler design and microprocessor correctness as a refined notation of compiler correctness. We will show how our approach is applied to designing a formally verified FHE (Fully Homomorphic Encryption) accelerator.
引用
收藏
页数：4
相关论文
共 50 条
  • [41] A novel formal verification approach for RTL hardware IP cores
    Djemal, R
    Dhouib, MA
    Dellacherie, S
    Tourki, R
    COMPUTER STANDARDS & INTERFACES, 2005, 27 (06) : 637 - 651
  • [42] On the Design of Scalable and Reusable Accelerators for Big Data Applications (invited paper)
    Pilato, Christian
    Xu, Qirui
    Mantovani, Paolo
    Di Guglielmo, Giuseppe
    Carloni, Luca P.
    PROCEEDINGS OF THE ACM INTERNATIONAL CONFERENCE ON COMPUTING FRONTIERS (CF'16), 2016, : 406 - 411
  • [43] Safety-Assured Formal Model-Driven Design of the Multifunction Vehicle Bus Controller
    Jiang, Yu
    Liu, Han
    Song, Houbing
    Kong, Hui
    Gu, Ming
    Sun, Jiaguang
    Sha, Lui
    FM 2016: FORMAL METHODS, 2016, 9995 : 757 - 763
  • [44] Formal design verification for correctness of pipelined microprocessors with out-of-order instruction execution
    Takenaka, T
    Kitamichi, J
    Higashino, T
    Taniguchi, K
    PROCEEDINGS OF ASP-DAC '99: ASIA AND SOUTH PACIFIC DESIGN AUTOMATION CONFERENCE 1999, 1999, : 177 - 180
  • [45] AN EXASCALE APPROACH TO SOFTWARE AND HARDWARE DESIGN
    Kramer, William
    Skinner, David
    INTERNATIONAL JOURNAL OF HIGH PERFORMANCE COMPUTING APPLICATIONS, 2009, 23 (04): : 389 - 391
  • [46] Formal approach to specifications in conceptual design
    Kusiak, A.
    Szczerbicki, E.
    Journal of Mechanical Design - Transactions of the ASME, 1992, 114 (04): : 659 - 666
  • [47] Invited Paper: Software/Hardware Co-design for LLM and Its Application for Design Verification
    Wan, Lily Jiaxin
    Huang, Yingbing
    Li, Yuhong
    Ye, Hanchen
    Wang, Jinghua
    Zhang, Xiaofan
    Chen, Deming
    29TH ASIA AND SOUTH PACIFIC DESIGN AUTOMATION CONFERENCE, ASP-DAC 2024, 2024, : 435 - 441
  • [48] Deductive hardware design:: A functional approach
    Möller, B
    PROSPECTS FOR HARDWARE FOUNDATIONS, 1998, 1546 : 421 - 468
  • [49] A formal object approach to the design of ZML
    Sun, J
    Dong, JS
    Liu, J
    Wang, H
    ANNALS OF SOFTWARE ENGINEERING, 2002, 13 (1-4) : 329 - 356
  • [50] A formal approach to optimizing the groove design
    Kinzin D.I.
    Kinzin, D. I., 1600, Allerton Press Incorporation (44): : 144 - 148
12345