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 条

[1] Assured VLSI design with formal verification
Kim, JD
Chin, SK
COMPASS '97 - ARE WE MAKING PROGRESS TOWARDS COMPUTER ASSURANCE?, 1997, : 13 - 22
[2] Formal correctness of supply chain design
Leukel, Joerg
Sugumaran, Vijayan
DECISION SUPPORT SYSTEMS, 2013, 56 : 288 - 299
[3] FORMAL VERIFICATION OF HARDWARE CORRECTNESS - INTRODUCTION AND SURVEY OF CURRENT RESEARCH
CAMURATI, P
PRINETTO, P
COMPUTER, 1988, 21 (07) : 8 - 19
[4] Scalable Effort Hardware Design
Chippa, Vinay Kumar
Mohapatra, Debabrata
Roy, Kaushik
Chakradhar, Srimat T.
Raghunathan, Anand
IEEE TRANSACTIONS ON VERY LARGE SCALE INTEGRATION (VLSI) SYSTEMS, 2014, 22 (09) : 2004 - 2016
[5] A Scalable Approach to Evolvable Hardware
Jim Torresen
Genetic Programming and Evolvable Machines, 2002, 3 (3) : 259 - 282
[6] A Formal Approach to Identifying Hardware Trojans in Cryptographic Hardware
Ito, Akira
Ueno, Rei
Homma, Naofumi
2021 IEEE 51ST INTERNATIONAL SYMPOSIUM ON MULTIPLE-VALUED LOGIC (ISMVL 2021), 2021, : 154 - 159
[7] Formal correctness of a passive testing approach for timed systems
Andres, Cesar
Merayo, Mercedes G.
Nunez, Manuel
ICSTW 2009: IEEE INTERNATIONAL CONFERENCE ON SOFTWARE TESTING, VERIFICATION, AND VALIDATION WORKSHOPS, 2009, : 67 - 76
[8] A mixed approach for the formal correctness proof of distributed programs
Manduchi, G
INFORMATION AND SOFTWARE TECHNOLOGY, 1996, 38 (08) : 521 - 538
[9] A Scalable Formal Verification Methodology for Data-Oblivious Hardware
Deutschmann, Lucas
Mueller, Johannes
Fadiheh, Mohammad Rahmani
Stoffel, Dominik
Kunz, Wolfgang
IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS, 2024, 43 (09) : 2551 - 2564
[10] A formal technique for hardware interface design
Baganne, A
Philippe, JL
Martin, E
ISCAS '97 - PROCEEDINGS OF 1997 IEEE INTERNATIONAL SYMPOSIUM ON CIRCUITS AND SYSTEMS, VOLS I - IV: CIRCUITS AND SYSTEMS IN THE INFORMATION AGE, 1997, : 1592 - 1595

← 1 2 3 4 5 →