View in EDS

Template-Based Parameterized Synthesis of Uniform Instruction-Level Abstractions for SoC Verification.

Saved in:
Bibliographic Details
Title: Template-Based Parameterized Synthesis of Uniform Instruction-Level Abstractions for SoC Verification.
Authors: Subramanyan, Pramod, Huang, Bo-Yuan, Vizel, Yakir, Gupta, Aarti, Malik, Sharad
Source: IEEE Transactions on Computer-Aided Design of Integrated Circuits & Systems. Aug2018, Vol. 37 Issue 8, p1692-1705. 14p.
Subjects: Systems on a chip, Systems on a chip testing, Hardware, Cryptography, Python programming language
Abstract: Modern system-on-chip (SoC) designs comprise programmable cores, application-specific accelerators, and I/O devices. Accelerators are controlled by software/firmware and functionality is implemented by this combination of programmable cores, firmware, and accelerators. Verification of such SoCs is challenging, especially for system-level properties maintained by a combination of firmware and hardware. Attempting to formally verify the full SoC design with both firmware and hardware is not scalable, while separate verification can miss bugs. A general technique for scalable system-level verification is to construct an abstraction of SoC hardware and verify firmware/software using it. There are two challenges in applying this technique in practice. Constructing the abstraction to capture required details and interactions is error-prone and time-consuming. The second is ensuring abstraction correctness so that properties proven with it are valid. This paper introduces a methodology for SoC design and verification based on the synthesis of instruction-level abstractions (ILAs). The ILA is an abstraction of SoC hardware which models updates to firmware-visible state at the granularity of instructions. For hardware accelerators, the ILA is analogous to the instruction-set architecture definition for programmable processors and enables scalable verification of firmware interacting with hardware accelerators. To alleviate the disadvantages of manual construction of abstractions, we introduce two algorithms for synthesis of ILAs from partial description called templates. We then show how the ILA can be verified to be correct. We evaluate the methodology using a small SoC design consisting of the 8051 microcontroller and two cryptographic accelerators. The methodology uncovered 15 bugs. [ABSTRACT FROM AUTHOR]
Copyright of IEEE Transactions on Computer-Aided Design of Integrated Circuits & Systems is the property of IEEE and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.)
Database: Engineering Source
FullText Text:
  Availability: 0
Header DbId: egs
DbLabel: Engineering Source
An: 130828425
AccessLevel: 6
PubType: Academic Journal
PubTypeId: academicJournal
PreciseRelevancyScore: 0
IllustrationInfo
Items – Name: Title
  Label: Title
  Group: Ti
  Data: Template-Based Parameterized Synthesis of Uniform Instruction-Level Abstractions for SoC Verification.
– Name: Author
  Label: Authors
  Group: Au
  Data: <searchLink fieldCode="AR" term="%22Subramanyan%2C+Pramod%22">Subramanyan, Pramod</searchLink><br /><searchLink fieldCode="AR" term="%22Huang%2C+Bo-Yuan%22">Huang, Bo-Yuan</searchLink><br /><searchLink fieldCode="AR" term="%22Vizel%2C+Yakir%22">Vizel, Yakir</searchLink><br /><searchLink fieldCode="AR" term="%22Gupta%2C+Aarti%22">Gupta, Aarti</searchLink><br /><searchLink fieldCode="AR" term="%22Malik%2C+Sharad%22">Malik, Sharad</searchLink>
– Name: TitleSource
  Label: Source
  Group: Src
  Data: <searchLink fieldCode="JN" term="%22IEEE+Transactions+on+Computer-Aided+Design+of+Integrated+Circuits+%26+Systems%22">IEEE Transactions on Computer-Aided Design of Integrated Circuits & Systems</searchLink>. Aug2018, Vol. 37 Issue 8, p1692-1705. 14p.
– Name: Subject
  Label: Subjects
  Group: Su
  Data: <searchLink fieldCode="DE" term="%22Systems+on+a+chip%22">Systems on a chip</searchLink><br /><searchLink fieldCode="DE" term="%22Systems+on+a+chip+testing%22">Systems on a chip testing</searchLink><br /><searchLink fieldCode="DE" term="%22Hardware%22">Hardware</searchLink><br /><searchLink fieldCode="DE" term="%22Cryptography%22">Cryptography</searchLink><br /><searchLink fieldCode="DE" term="%22Python+programming+language%22">Python programming language</searchLink>
– Name: Abstract
  Label: Abstract
  Group: Ab
  Data: Modern system-on-chip (SoC) designs comprise programmable cores, application-specific accelerators, and I/O devices. Accelerators are controlled by software/firmware and functionality is implemented by this combination of programmable cores, firmware, and accelerators. Verification of such SoCs is challenging, especially for system-level properties maintained by a combination of firmware and hardware. Attempting to formally verify the full SoC design with both firmware and hardware is not scalable, while separate verification can miss bugs. A general technique for scalable system-level verification is to construct an abstraction of SoC hardware and verify firmware/software using it. There are two challenges in applying this technique in practice. Constructing the abstraction to capture required details and interactions is error-prone and time-consuming. The second is ensuring abstraction correctness so that properties proven with it are valid. This paper introduces a methodology for SoC design and verification based on the synthesis of instruction-level abstractions (ILAs). The ILA is an abstraction of SoC hardware which models updates to firmware-visible state at the granularity of instructions. For hardware accelerators, the ILA is analogous to the instruction-set architecture definition for programmable processors and enables scalable verification of firmware interacting with hardware accelerators. To alleviate the disadvantages of manual construction of abstractions, we introduce two algorithms for synthesis of ILAs from partial description called templates. We then show how the ILA can be verified to be correct. We evaluate the methodology using a small SoC design consisting of the 8051 microcontroller and two cryptographic accelerators. The methodology uncovered 15 bugs. [ABSTRACT FROM AUTHOR]
– Name: AbstractSuppliedCopyright
  Label:
  Group: Ab
  Data: <i>Copyright of IEEE Transactions on Computer-Aided Design of Integrated Circuits & Systems is the property of IEEE and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract.</i> (Copyright applies to all Abstracts.)
PLink https://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=egs&AN=130828425
RecordInfo BibRecord:
  BibEntity:
    Identifiers:
      – Type: doi
        Value: 10.1109/TCAD.2017.2764482
    Languages:
      – Code: eng
        Text: English
    PhysicalDescription:
      Pagination:
        PageCount: 14
        StartPage: 1692
    Subjects:
      – SubjectFull: Systems on a chip
        Type: general
      – SubjectFull: Systems on a chip testing
        Type: general
      – SubjectFull: Hardware
        Type: general
      – SubjectFull: Cryptography
        Type: general
      – SubjectFull: Python programming language
        Type: general
    Titles:
      – TitleFull: Template-Based Parameterized Synthesis of Uniform Instruction-Level Abstractions for SoC Verification.
        Type: main
  BibRelationships:
    HasContributorRelationships:
      – PersonEntity:
          Name:
            NameFull: Subramanyan, Pramod
      – PersonEntity:
          Name:
            NameFull: Huang, Bo-Yuan
      – PersonEntity:
          Name:
            NameFull: Vizel, Yakir
      – PersonEntity:
          Name:
            NameFull: Gupta, Aarti
      – PersonEntity:
          Name:
            NameFull: Malik, Sharad
    IsPartOfRelationships:
      – BibEntity:
          Dates:
            – D: 01
              M: 08
              Text: Aug2018
              Type: published
              Y: 2018
          Identifiers:
            – Type: issn-print
              Value: 02780070
          Numbering:
            – Type: volume
              Value: 37
            – Type: issue
              Value: 8
          Titles:
            – TitleFull: IEEE Transactions on Computer-Aided Design of Integrated Circuits & Systems
              Type: main
ResultId 1