Awards

Best Paper Award

Lift-off: Trustworthy ARMv8 semantics from formal specifications by Kait Lam and Nicholas Coughlin.

Congratulations to the authors! Below is an explanation by Ziyad Hanna why the selected paper matters:

According to analysts, the electronic industry’s annual revenue is estimated to double by 2030, reaching one trillion USD. Chip design is a crucial driver of this growth, spanning various electronic and system markets such as smart devices, computer servers and cloud computing, mobile phones, AI accelerators, Internet-of-things, automotive, and embedded systems. However, chip design costs are rapidly increasing, and the number of chip design projects is expected to increase fourfold in the next decade. AI and Generative AI have a great potential to boost design and verification productivity by orders of magnitude. Verification consumes almost two third of the total cost. The rapidly growing cost of verification is required for the design’s functional, low power, safety, and security aspect. Therefore, further innovations in new technologies and methodologies are crucial to significantly cut costs and boost the chip design.

A precise formal specification is a crucial step to capture the system’s required behavior for achieving comprehensive verification in all phases of the chip design process. A key specification challenge is capturing the precise semantics of architecture and micro-architecture behaviors of the fast-evolving and complex CPU designs that industry leaders like ARM offer for the fast-emerging and widespread chip design market.

This paper presents advancements in the state-of-the-art for enhancing the benefits and applications of a canonical, accurate, and comprehensive ISA specification. The authors leverage the architecture specifications provided by ARM to establish a robust and reliable foundation for binary disassembly and lifting from binary programs. Through partial evaluation techniques, they can condense these semantics into a concise internal representation, facilitating seamless integration with other analysis tools. This approach enables the exploration of new applications and addresses the intricate challenges associated with verification. By paving the way for innovative solutions, this research advances the field and opens up new possibilities for addressing complex verification challenges of chip designs.