Skip to main content

ILAng: A Modeling and Verification Platform for SoCs Using Instruction-Level Abstractions

Author(s): Huang, Bo-Yuan; Zhang, Hongce; Gupta, Aarti; Malik, Sharad

Download
To refer to this page use: http://arks.princeton.edu/ark:/88435/pr14k0j
Full metadata record
DC FieldValueLanguage
dc.contributor.authorHuang, Bo-Yuan-
dc.contributor.authorZhang, Hongce-
dc.contributor.authorGupta, Aarti-
dc.contributor.authorMalik, Sharad-
dc.date.accessioned2021-10-08T19:46:39Z-
dc.date.available2021-10-08T19:46:39Z-
dc.date.issued2019en_US
dc.identifier.citationHuang, Bo-Yuan, Hongce Zhang, Aarti Gupta, and Sharad Malik. "ILAng: a modeling and verification platform for SoCs using instruction-level abstractions." In International Conference on Tools and Algorithms for the Construction and Analysis of Systems (2019): pp. 351-357. doi:10.1007/978-3-030-17462-0_21en_US
dc.identifier.issn0302-9743-
dc.identifier.urihttp://arks.princeton.edu/ark:/88435/pr14k0j-
dc.description.abstractWe present ILAng, a platform for modeling and verification of systems-on-chip (SoCs) using Instruction-Level Abstractions (ILA). The ILA formal model targeting the hardware-software interface enables a clean separation of concerns between software and hardware through a unified model for heterogeneous processors and accelerators. Top-down it provides a specification for functional verification of hardware, and bottom-up it provides an abstraction for software/hardware co-verification. ILAng provides a programming interface for (i) constructing ILA models (ii) synthesizing ILA models from templates using program synthesis techniques (iii) verifying properties on ILA models (iv) behavioral equivalence checking between different ILA models, and between an ILA specification and an implementation. It also provides for translating models and properties into various languages (e.g., Verilog and SMT LIB2) for different verification settings and use of third-party verification tools. This paper demonstrates selected capabilities of the platform through case studies. Data or code related to this paper is available at: [9].en_US
dc.format.extent351 - 357en_US
dc.language.isoen_USen_US
dc.relation.ispartofInternational Conference on Tools and Algorithms for the Construction and Analysis of Systemsen_US
dc.rightsFinal published version. This is an open access article.en_US
dc.titleILAng: A Modeling and Verification Platform for SoCs Using Instruction-Level Abstractionsen_US
dc.typeConference Articleen_US
dc.identifier.doi10.1007/978-3-030-17462-0_21-
dc.identifier.eissn1611-3349-
pu.type.symplectichttp://www.symplectic.co.uk/publications/atom-terms/1.0/conference-proceedingen_US

Files in This Item:
File Description SizeFormat 
IlangModelingVerifSocsAbstractions.pdf379.82 kBAdobe PDFView/Download


Items in OAR@Princeton are protected by copyright, with all rights reserved, unless otherwise indicated.