More Web Proxy on the site http://driver.im/

research-article

Public Access

Instruction-Level Abstraction (ILA): A Uniform Specification for System-on-Chip (SoC) Verification

Authors:

Pramod Subramanyan,

Sharad MalikAuthors Info & Claims

ACM Transactions on Design Automation of Electronic Systems (TODAES), Volume 24, Issue 1

Article No.: 10, Pages 1 - 24

https://doi.org/10.1145/3282444

Published: 21 December 2018 Publication History

Abstract

Modern Systems-on-Chip (SoC) designs are increasingly heterogeneous and contain specialized semi-programmable accelerators in addition to programmable processors. In contrast to the pre-accelerator era, when the ISA played an important role in verification by enabling a clean separation of concerns between software and hardware, verification of these “accelerator-rich” SoCs presents new challenges. From the perspective of hardware designers, there is a lack of a common framework for formal functional specification of accelerator behavior. From the perspective of software developers, there exists no unified framework for reasoning about software/hardware interactions of programs that interact with accelerators.

This article addresses these challenges by providing a formal specification and high-level abstraction for accelerator functional behavior. It formalizes the concept of an Instruction Level Abstraction (ILA), developed informally in our previous work, and shows its application in modeling and verification of accelerators. This formal ILA extends the familiar notion of instructions to accelerators and provides a uniform, modular, and hierarchical abstraction for modeling software-visible behavior of both accelerators and programmable processors. We demonstrate the applicability of the ILA through several case studies of accelerators (for image processing, machine learning, and cryptography), and a general-purpose processor (RISC-V). We show how the ILA model facilitates equivalence checking between two ILAs, and between an ILA and its hardware finite-state machine (FSM) implementation. Further, this equivalence checking supports accelerator upgrades using the notion of ILA compatibility, similar to processor upgrades using ISA compatibility.

References

[1]

Samar Abdi and Daniel Gajski. 2006. Verification of system level model transformations. International Journal of Parallel Programming 34, 1 (2006), 29--59.

Digital Library

[2]

Jade Alglave and Michael Tautschnig. 2014. Herding cats: Modelling, simulation, testing, and data-mining for weak memory. ACM Transactions on Programming Languages and Systems 36, 2 (2014), 7:1--7:74.

Digital Library

[3]

Rajeev Alur, Rastislav Bodik, Garvit Juniwal, Milo M. K. Martin, Mukund Raghothaman, Sanjit A. Seshia, Rishabh Singh, Armando Solar-Lezama, Emina Torlak, and Abhishek Udupa. 2013. Syntax-guided synthesis. In Proceedings of the Conference on Formal Methods in Computer-Aided Design. 1--8.

[4]

Rajeev Alur and Radu Grosu. 2000. Modular refinement of hierarchic reactive machines. In Proceedings of the Symposium on Principles of Programming Language. 390--402.

Digital Library

[5]

Ehsan K. Ardestani and Jose Renau. 2013. ESESC: A fast multicore simulator using time-based sampling. In Proceedings of the International Symposium on High-Performance Computer Architecture. 448--459.

Digital Library

[6]

ARM Ltd. 2010. Cortex-M3 Devices Generic User Guide. Retrieved November 11, 2017 from http://infocenter.arm.com/help/index.jsp?topic=/com.arm.doc.dui0552a/BABCAEDD.html.

[7]

Arvind and Xiaowei Shen. 1999. Using term rewriting systems to design and verify processors. IEEE Micro 19, 3 (May 1999), 36--46.

Digital Library

[8]

Krste Asanović, Rimas Avizienis, Jonathan Bachrach, Scott Beamer, David Biancolin, Christopher Celio, Henry Cook, Daniel Dabbelt, John Hauser, Adam Izraelevitz, Sagar Karandikar, Ben Keller, Donggyu Kim, John Koenig, Yunsup Lee, Eric Love, Martin Maas, Albert Magyar, Howard Mao, Miquel Moreto, Albert Ou, David A. Patterson, Brian Richards, Colin Schmidt, Stephen Twigg, Huy Vo, and Andrew Waterman. 2016. The Rocket Chip Generator. Technical Report UCB/EECS-2016-17. EECS Department, University of California, Berkeley. http://www2.eecs.berkeley.edu/Pubs/TechRpts/2016/EECS-2016-17.html

[9]

Francine Bacchini, Daniel D. Gajski, Laurent Maillet-Contoz, Haruhisa Kashiwagi, Jack Donovan, Tommi Makelainen, Jack Greenbaum, and R. S. Nikhil. 2007. TLM: Crossing over from buzz to adoption. In Proceedings of Design Automation Conference. 444--445.

Digital Library

[10]

Jonathan Bachrach, Huy Vo, Brian Richards, Yunsup Lee, Andrew Waterman, Rimas Avižienis, John Wawrzynek, and Krste Asanović. 2012. Chisel: Constructing hardware in a scala embedded language. In Proceedings of Design Automation Conference. 1212--1221.

Digital Library

[11]

Clark Barrett, Aaron Stump, and Cesare Tinelli. 2010. The SMT-LIB standard version 2.0. In Proceedings of the International Workshop on Satisfiability Modulo Theories. 14--112.

[12]

Mark Batty, Kayvan Memarian, Scott Owens, and Susmit Sarkar. 2012. Clarifying and compiling C/C++ concurrency: From C++ 11 to POWER. In Proceedings of the Annual Symposium on Principles of Programming Languages. ACM, New York, 509--520.

Digital Library

[13]

Mark Batty, Scott Owens, Susmit Sarkar, Peter Sewell, and Tjark Weber. 2011. Mathematizing C++ concurrency. In Proceedings of the Annual Symposium on Principles of Programming Languages. 55--66.

Digital Library

[14]

G. Berry, M. Kishinevsky, and S. Singh. 2003. System level design and verification using a synchronous language. In Proceedings of the International Conference on Computer-Aided Design. 433--439.

Digital Library

[15]

Armin Biere, Alessandro Cimatti, and Edmund M Clarke. 2003. Bounded model checking. Advances in Computers 58 (2003), 117--148.

[16]

Nathan Binkert, Somayeh Sardashti, Rathijit Sen, Korey Sewell, Muhammad Shoaib, Nilay Vaish, Mark D. Hill, David A. Wood, Bradford Beckmann, Gabriel Black, Steven K. Reinhardt, Ali Saidi, Arkaprava Basu, Joel Hestness, Derek R. Hower, and Tushar Krishna. 2011. The gem5 simulator. ACM SIGARCH Computer Architecture News 39, 2 (2011), 1--7.

Digital Library

[17]

Nikolaj Bjorner and Leonardo De Moura. 2011. Satisfiability modulo theories: Introduction and applications. Communications of the ACM 54, 9 (2011), 69--77.

Digital Library

[18]

James Bornholt and Emina Torlak. 2017. Synthesizing memory models from framework sketches and litmus tests. In Proceedings of the Conference on Programming Language Design and Implementation. 467--481.

Digital Library

[19]

Jerry R. Burch and David L. Dill. 1994. Automated verification of pipelined microprocessor control. In Proceedings of the International Conference on Computer Aided Verification. 68--84. https://dl.acm.org/citation.cfm?id=735662

Digital Library

[20]

Cadence Design Systems, Inc. 2018. JasperGold: Formal Property Verification App. Retrieved January 2, 2018 from http://www.jasper-da.com/products/jaspergold-apps/.

[21]

Andrew Canis, Jongsok Choi, Mark Aldham, and Victor Zhang. 2013. LegUp: An open-source high-level synthesis tool for FPGA-Based processor/accelerator systems. ACM Transactions on Embedded Computing Systems 13, 2 (2013), 24:1--24:27.

Digital Library

[22]

Wei Ting Jonas Chan, Andrew B. Kahng, Siddhartha Nath, and Ichiro Yamamoto. 2014. The ITRS MPU and SoC system drivers: Calibration and implications for design-based equivalent scaling in the roadmap. In Proceedings of the International Conference on Computer Design. 153--160.

[23]

Joonwon Choi, Muralidaran Vijayaraghavan, Benjamin Sherman, and Adam Chlipala. 2017. Kami: A platform for high-level parametric hardware specification and its modular verification. Proceedings of the ACM on Programming Languages 1, 24 (2017).

Digital Library

[24]

Edmund Clarke, Daniel Kroening, and Flavio Lerda. 2004. CBMC - A tool for checking ANSI-C programs. In Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Vol. 2988. 168--176.

[25]

Edmund M. Clarke, Orna Grumberg, and Doron Peled. 1999. Model Checking. MIT Press.

Digital Library

[26]

Fady Copty, Limor Fix, Ranan Fraer, Enrico Giunchiglia, Gila Kamhi, Armando Tacchella, and Moshe Y. Vardi. 2001. Benefits of bounded model checking at an industrial setting. In Proceedings of the International Conference on Computer Aided Verification. 436--453.

Digital Library

[27]

Emilio G. Cota, Paolo Mantovani, Giuseppe Di Guglielmo, and Luca P. Carloni. 2015. An analysis of accelerator coupling in heterogeneous architectures. In Proceedings of Design Automation Conference. 202:1--202:6.

Digital Library

[28]

Nirav Dave, Arvind, and Michael Pellauer. 2007. Scheduling as rule composition. In Proceedings of the IEEE/ACM International Conference on Formal Methods and Models for Codesign. IEEE, 51--60.

Digital Library

[29]

Nirav Dave, Michael Katelman, Myron King, Jose Arvind, and Jose Meseguer. 2011. Verification of microarchitectural refinements in rule-based systems. In Proceedings of the ACM/IEEE International Conference on Formal Methods and Models for Codesign. IEEE, 61--71.

Digital Library

[30]

Leonardo De Moura and Nikolaj Bjørner. 2008. Z3: An efficient SMT solver. In Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 337--340.

Digital Library

[31]

Rainer Dömer, Andreas Gerstlauer, Junyu Peng, Dongwan Shin, Lukai Cai, Haobo Yu, Samar Abdi, and Daniel D. Gajski. 2008. System-on-chip environment: A SpecC-based framework for heterogeneous MPSoC design. EURASIP Journal on Embedded Systems (2008), 5:1--5:13.

Digital Library

[32]

Shilpi Goel, Warren A. Hunt, Matt Kaufmann, and Soumava Ghosh. 2014. Simulation and formal verification of x86 machine-code programs that make system calls. In Proceedings of the International Conference on Formal Methods in Computer-Aided Design. 91--98.

Digital Library

[33]

Ashutosh Gupta, Corneliu Popeea, and Andrey Rybalchenko. 2011. Threader: A constraint-based verifier for multi-threaded programs. In Proceedings of the International Conference on Computer Aided Verification. 412--417.

Digital Library

[34]

David Harel and Amnon Naamad. 1996. The STATEMATE semantics of statecharts. ACM Transactions on Software Engineering and Methodology 5, 4 (1996), 293--333.

Digital Library

[35]

Paula Herber and Sabine Glesner. 2013. A HW/SW co-verification framework for systemC. ACM Transactions on Embedded Computing Systems 12, 1 (2013), 61:1--61:23.

Digital Library

[36]

James C. Hoe and Arvind. 2000. Synthesis of operation-centric hardware descriptions. In Proceedings of the International Conference on Computer-Aided Design. 511--519.

Digital Library

[37]

Gerard J. Holzmann. 1997. The model checker SPIN. IEEE Transactions on Software Engineering 23, 5 (1997), 279--295.

Digital Library

[38]

Homer Hsing. 2014. OpenCores.org: Tiny AES. Retrieved November 17, 2017 from https://opencores.org/project,tiny_aes.

[39]

Intel Corporation. 2016. Intel®64 and IA-32 Architectures Software Developer Manual: Vol. 2 Instruction Set Reference. Retrieved November 17, 2017 from https://software.intel.com/en-us/articles/intel-sdm.

[40]

Himanshu Jain, Daniel Kroening, Natasha Sharygina, and Edmund M. Clarke. 2005. Word level predicate abstraction and refinement for verifying RTL verilog. In Proceedings of Design Automation Conference. 445--450.

Digital Library

[41]

Susmit Jha, Sumit Gulwani, Sanjit A. Seshia, and Ashish Tiwari. 2010. Oracle-guided component-based program synthesis. In Proceedings of the International Conference on Software Engineering. 215--224.

Digital Library

[42]

Ranjit Jhala and Kenneth L. McMillan. 2001. Microarchitecture verification by compositional model checking. In Proceedings of the International Conference on Computer Aided Verification, Vol. 2102. 396--410.

Digital Library

[43]

Suho Lee and Karem A. Sakallah. 2014. Unbounded scalable verification based on approximate property-directed reachability and datapath abstraction. In Proceedings of the International Conference on Computer Aided Verification. 849--865.

Digital Library

[44]

Helger Lipmaa, David Wagner, and Phillip Rogaway. 2000. Comments to NIST Concerning AES Modes of Operation: CTR-Mode Encryption. Retrieved May 5, 2018 from http://kodu.ut.ee/ lipmaa/papers/lrw00/html/ctr.html.

[45]

Derek Lockhart, Gary Zibrat, and Christopher Batten. 2014. PyMTL: A unified framework for vertically integrated computer architecture research. In Proceedings of the International Symposium on Microarchitecture. 280--292.

Digital Library

[46]

Daniel Lustig, Michael Pellauer, and Margaret Martonosi. 2015. Pipe check: Specifying and verifying microarchitectural enforcement of memory consistency models. In Proceedings of the Annual International Symposium on Microarchitecture. 635--646.

Digital Library

[47]

Daniel Lustig, Geet Sethi, Margaret Martonosi, and Abhishek Bhattacharjee. 2016. COATCheck : Verifying memory ordering at the hardware-OS interface. In Proceedings of the International Conference on Architectural Support for Programming Languages and Operating Systems, Vol. 1. 233--247.

Digital Library

[48]

Kenneth L. Mcmillan. 1993. Symbolic Model Checking. Springer.

Digital Library

[49]

Robin Milner. 1989. Communication and Concurrency. Prentice Hall.

Digital Library

[50]

Razvan Nane, Vlad Mihai Sima, Christian Pilato, Jongsok Choi, Blair Fort, Andrew Canis, Yu Ting Chen, Hsuan Hsiao, Stephen Brown, Fabrizio Ferrandi, Jason Anderson, and Koen Bertels. 2016. A survey and evaluation of FPGA high-level synthesis tools. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 35, 10 (2016), 1591--1604.

Digital Library

[51]

R. Nikhil. 2004. Bluespec system verilog: Efficient, correct RTL from high-level specifications. In Proceedings of the International Conference on Formal Methods and Models for Co-Design. 69--70.

Digital Library

[52]

Susan Owicki and David Gries. 1976. An axiomatic proof technique for parallel programs. Acta Informatica 6, 4 (1976), 319--340.

Digital Library

[53]

Preeti Ranjan Panda. 2001. SystemC - A modeling platform supporting multiple design abstractions. In Proceedings of the International Symposium on Systems Synthesis. 75--80.

Digital Library

[54]

Christian Pilato and Fabrizio Ferrandi. 2013. Bambu: A modular framework for the high level synthesis of memory-intensive applications. In Proceedings of the International Conference on Field Programmable Logic and Applications. 13--16.

[55]

Christian Pilato, Qirui Xu, Paolo Mantovani, Giuseppe Di Guglielmo, and Luca P. Carloni. 2016. On the design of scalable and reusable accelerators for big data applications. In Proceedings of the ACM International Conference on Computing Frontiers. 406--411.

Digital Library

[56]

Jing Pu, Steven Bell, Xuan Yang, Jeff Setter, Stephen Richardson, Jonathan Ragan-Kelley, and Mark Horowitz. 2016. Programming heterogeneous systems from an image processing DSL. ACM Transactions on Architecture and Code Optimization 14 (2016), 26:1--26:25.

Digital Library

[57]

Jonathan Ragan-Kelley, Andrew Adams, Sylvain Paris, Frédo Durand, Connelly Barnes, and Saman Amarasinghe. 2013. Halide: A language and compiler for optimizing parallelism, locality, and recomputation in image processing pipelines. In Proceedings of the Conference on Programming Language Design and Implementation. 519--530.

Digital Library

[58]

Alastair Reid. 2017. Trustworthy specifications of ARM® v8-A and v8-M system level architecture. In Proceedings of the Conference on Formal Methods in Computer-Aided Design. 161--168.

Digital Library

[59]

Alastair Reid, Rick Chen, Anastasios Deligiannis, David Gilday, David Hoyes, Will Keen, Ashan Pathirane, Owen Shepherd, Peter Vrabel, and Ali Zaidi. 2016. End-to-end verification of ARM® processors with ISA-formal. In Proceedings of the International Conference on Computer Aided Verification, Vol. 9780. 42--58.

[60]

Paul Rosenfeld, Elliott Cooper-Balis, and Bruce Jacob. 2011. DRAMSim2: A cycle accurate memory system simulator. IEEE Computer Architecture Letters 10, 1 (2011), 16--19.

Digital Library

[61]

Yakun Sophia Shao, Brandon Reagen, Gu-Yeon Wei, and David Brooks. 2015. The Aladdin approach to accelerator design and modeling. IEEE Micro 35, 3 (2015), 58--70.

Digital Library

[62]

Pramod Subramanyan, Bo-Yuan Huang, Yakir Vizel, Aarti Gupta, and Sharad Malik. 2017. Template-based parameterized synthesis of uniform instruction-level abstractions for SoC verification. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 99 (2017).

[63]

Pramod Subramanyan, Sharad Malik, Hareesh Khattri, Abhranil Maiti, and Jason Fung. 2016. Verifying information flow properties of firmware using symbolic execution. In Proceedings of the Conference on Design, Automation and Test in Europe. 1393--1398.

Digital Library

[64]

Pramod Subramanyan, Yakir Vizel, Sayak Ray, and Sharad Malik. 2017. Template-based synthesis of instruction-level abstractions for SoC verification. In Proceedings of the Conference on Formal Methods in Computer-Aided Design. 160--167.

Digital Library

[65]

Impulse Accelerated Technologies. 2003. Impulse CoDeveloper C-to-FPGA Tools. Retrieved November 17, 2017 from http://www.impulseaccelerated.com/products_universal.htm.

[66]

Caroline Trippel, Yatin A. Manerkar, Daniel Lustig, Michael Pellauer, and Margaret Martonosi. 2017. TriCheck: Memory model verification at the trisection of software, hardware, and ISA. In Proceedings of International Conference on Architectural Support for Programming Languages and Operating Systems. 119--133.

Digital Library

[67]

Muralidaran Vijayaraghavan, Adam Chlipala, Arvind, and Nirav Dave. 2015. Modular deductive verification of multiprocessor hardware designs. In Proceedings of the International Conference on Computer Aided Verification. 109--127.

[68]

Yakir Vizel, Orna Grumberg, and Sharon Shoham. 2012. Lazy abstraction and SAT-based reachability in hardware model checking. In Proceedings of the International Conference on Formal Methods in Computer-Aided Design. 173--181.

[69]

Andrew Waterman, Yunsup Lee, Rimas Avizienis, David A. Patterson, and Krste Asanović. 2017. The RISC-V Instruction Set Manual Volume II: Privileged Architecture Version 1.9.1. Retrieved November 17, 2017 from https://riscv.org/specifications/privileged-isa/.

[70]

Tjark Weber. 2004. Satisfiability modulo theories. In Handbook of Satisfiability. Vol. 185. 825--885.

Cited By

Huang BLyubomirsky SLi YHe MSmith GTambe TGaonkar ACanumalla VCheung AWei GGupta ATatlock ZMalik S(2024)Application-level Validation of Accelerator Designs Using a Formal Software/Hardware InterfaceACM Transactions on Design Automation of Electronic Systems10.1145/363905129:2(1-25)Online publication date: 14-Feb-2024
https://dl.acm.org/doi/10.1145/3639051
Jayasena AMishra P(2024)HIVE: Scalable Hardware-Firmware Co-Verification Using Scenario-Based Decomposition and Automated Hint ExtractionIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems10.1109/TCAD.2024.338396143:10(3278-3291)Online publication date: 1-Oct-2024
https://dl.acm.org/doi/10.1109/TCAD.2024.3383961
Yang JYang ZCasas JRay S(2024)Correct-by-Construction Design of Custom Accelerator MicroarchitecturesIEEE Transactions on Computers10.1109/TC.2023.332924373:1(278-291)Online publication date: 1-Jan-2024
https://dl.acm.org/doi/10.1109/TC.2023.3329243
Show More Cited By

Index Terms

Instruction-Level Abstraction (ILA): A Uniform Specification for System-on-Chip (SoC) Verification
1. Computer systems organization
  1. Architectures
2. Hardware

Recommendations

Formal security verification of concurrent firmware in SoCs using instruction-level abstraction for hardware
DAC '18: Proceedings of the 55th Annual Design Automation Conference

Formal security verification of firmware interacting with hardware in modern Systems-on-Chip (SoCs) is a critical research problem. This faces the following challenges: (1) design complexity and heterogeneity, (2) semantics gaps between software and ...
SoC Protocol Implementation Verification Using Instruction-Level Abstraction Specifications
In modern systems-on-chips, several hardware protocols are used for communication and interaction among different modules. These protocols are complex and need to be implemented correctly for correct operation of the system-on-chip. Therefore, protocol ...
An integrated environment for HDL verification
IVC '95: Proceedings of the 4th IEEE International Verilog HDL Conference

The functional verification of a digital design is an expensive step in the design process. As designs become more complex, simulation is challenged throughout the design and verification process, both at the low level (implementation verification), to ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Transactions on Design Automation of Electronic Systems

ACM Transactions on Design Automation of Electronic Systems Volume 24, Issue 1

January 2019

309 pages

ISSN:1084-4309

EISSN:1557-7309

DOI:10.1145/3293467

Editor:
Naehyuck Chang
Korea Advanced Institute of Science and Technology, Korea

Issue’s Table of Contents

Copyright © 2018 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Journal Family

ACM Journals for the Design of Smart and Connected Systems

Publication History

Published: 21 December 2018

Accepted: 01 September 2018

Revised: 01 June 2018

Received: 01 January 2018

Published in TODAES Volume 24, Issue 1

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Best Paper

Author Tags

Qualifiers

Research-article
Research
Refereed

Funding Sources

National Science Foundation

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

30
Total Citations
View Citations
2,539
Total Downloads

Downloads (Last 12 months)563
Downloads (Last 6 weeks)70

Reflects downloads up to 10 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Huang BLyubomirsky SLi YHe MSmith GTambe TGaonkar ACanumalla VCheung AWei GGupta ATatlock ZMalik S(2024)Application-level Validation of Accelerator Designs Using a Formal Software/Hardware InterfaceACM Transactions on Design Automation of Electronic Systems10.1145/363905129:2(1-25)Online publication date: 14-Feb-2024
https://dl.acm.org/doi/10.1145/3639051
Jayasena AMishra P(2024)HIVE: Scalable Hardware-Firmware Co-Verification Using Scenario-Based Decomposition and Automated Hint ExtractionIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems10.1109/TCAD.2024.338396143:10(3278-3291)Online publication date: 1-Oct-2024
https://dl.acm.org/doi/10.1109/TCAD.2024.3383961
Yang JYang ZCasas JRay S(2024)Correct-by-Construction Design of Custom Accelerator MicroarchitecturesIEEE Transactions on Computers10.1109/TC.2023.332924373:1(278-291)Online publication date: 1-Jan-2024
https://dl.acm.org/doi/10.1109/TC.2023.3329243
Li YCi YYang QKim T(2024)TIUP: Effective Processor Verification with Tautology-Induced Universal PropertiesProceedings of the 29th Asia and South Pacific Design Automation Conference10.1109/ASP-DAC58780.2024.10473912(269-274)Online publication date: 22-Jan-2024
https://dl.acm.org/doi/10.1109/ASP-DAC58780.2024.10473912
Hazott CStögmüller FGroße D(2024)Verifying Embedded Graphics Libraries leveraging Virtual Prototypes and Metamorphic Testing2024 29th Asia and South Pacific Design Automation Conference (ASP-DAC)10.1109/ASP-DAC58780.2024.10473799(275-281)Online publication date: 22-Jan-2024
https://doi.org/10.1109/ASP-DAC58780.2024.10473799
Hazott CStögmüller FGroße D(2024)Using virtual prototypes and metamorphic testing to verify the hardware/software-stack of embedded graphics librariesIntegration10.1016/j.vlsi.2024.102320(102320)Online publication date: Dec-2024
https://doi.org/10.1016/j.vlsi.2024.102320
Chen LChen YChu ZFang WHo THuang RHuang YKhan SLi MLi XLi YLiang YLiu JLiu YLin YLuo GPan HShi ZSun GTsaras DWang RWang ZWei XXie ZXu QXue CYan JYang JYu BYuan MYoung EZeng XZhang HZhang ZZhao YZhen HZheng ZZhu BZhu KZou S(2024)Large circuit models: opportunities and challengesScience China Information Sciences10.1007/s11432-024-4155-767:10Online publication date: 25-Sep-2024
https://doi.org/10.1007/s11432-024-4155-7
Orenes-Vera MYun HWistoff NHeiser GBenini LWentzlaff DMartonosi M(2023)AutoCC: Automatic Discovery of Covert Channels in Time-Shared HardwareProceedings of the 56th Annual IEEE/ACM International Symposium on Microarchitecture10.1145/3613424.3614254(871-885)Online publication date: 28-Oct-2023
https://dl.acm.org/doi/10.1145/3613424.3614254
Lu HXing YGupta AMalik S(2023)SoC Protocol Implementation Verification Using Instruction-Level Abstraction SpecificationsACM Transactions on Design Automation of Electronic Systems10.1145/361029228:6(1-24)Online publication date: 16-Oct-2023
https://dl.acm.org/doi/10.1145/3610292
Wang ZMohr Gvon Gleissenthall KReineke JGuarnieri MMeng WJensen CCremers CKirda E(2023)Specification and Verification of Side-channel Security for Open-source Processors via Leakage ContractsProceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security10.1145/3576915.3623192(2128-2142)Online publication date: 15-Nov-2023
https://dl.acm.org/doi/10.1145/3576915.3623192
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Media

Figures

Other

Tables

View Issue’s Table of Contents