View in EDS

Functional test generation based on word-level SAT

Saved in:
Bibliographic Details
Title: Functional test generation based on word-level SAT
Authors: Zeng, Zhihong1 zzeng@avery-design.com, Talupuru, Kesava R.1 kesava@logic-mill.com, Ciesielski, Maciej ciesiel@ecs.umass.edu
Source: Journal of Systems Architecture. Aug2005, Vol. 51 Issue 8, p488-511. 24p.
Subjects: Slosson Intelligence Test, Mathematics, RTL (Computer program language), Logic programming
Abstract: Abstract: Functional test generation coupled with symbolic simulation offers a good compromise between formal verification and numerical simulation for design validation. The generation of functional test vectors guided by miscellaneous coverage metrics can be posed as a satisfiability problem (SAT). While a number of efficient Boolean SAT engines have been developed for gate level designs, they are not directly applicable to behavioral and RTL designs containing significant arithmetic components. This paper presents two approaches that enhance the capability of functional test generation by preserving arithmetic operators in the design. They are based on word-level SAT techniques: (1) LPSAT, based on integer linear programming, and (2) CLP-SAT, based on constraint logic programming. The proposed SAT solvers allow to efficiently handle the designs with mixed word-level arithmetic operators and bit-level logic gates. The experimental results are quite encouraging compared to traditional CNF-based and BDD-based SAT solvers. The paper also suggests a method to build an integrated SAT solving framework where different SAT solvers work together to provide a more complete solution to functional test generation and other verification applications. [Copyright &y& Elsevier]
Copyright of Journal of Systems Architecture is the property of Elsevier B.V. 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: 18145381
AccessLevel: 6
PubType: Academic Journal
PubTypeId: academicJournal
PreciseRelevancyScore: 0
IllustrationInfo
Items – Name: Title
  Label: Title
  Group: Ti
  Data: Functional test generation based on word-level SAT
– Name: Author
  Label: Authors
  Group: Au
  Data: <searchLink fieldCode="AR" term="%22Zeng%2C+Zhihong%22">Zeng, Zhihong</searchLink><relatesTo>1</relatesTo><i> zzeng@avery-design.com</i><br /><searchLink fieldCode="AR" term="%22Talupuru%2C+Kesava+R%2E%22">Talupuru, Kesava R.</searchLink><relatesTo>1</relatesTo><i> kesava@logic-mill.com</i><br /><searchLink fieldCode="AR" term="%22Ciesielski%2C+Maciej%22">Ciesielski, Maciej</searchLink><i> ciesiel@ecs.umass.edu</i>
– Name: TitleSource
  Label: Source
  Group: Src
  Data: <searchLink fieldCode="JN" term="%22Journal+of+Systems+Architecture%22">Journal of Systems Architecture</searchLink>. Aug2005, Vol. 51 Issue 8, p488-511. 24p.
– Name: Subject
  Label: Subjects
  Group: Su
  Data: <searchLink fieldCode="DE" term="%22Slosson+Intelligence+Test%22">Slosson Intelligence Test</searchLink><br /><searchLink fieldCode="DE" term="%22Mathematics%22">Mathematics</searchLink><br /><searchLink fieldCode="DE" term="%22RTL+%28Computer+program+language%29%22">RTL (Computer program language)</searchLink><br /><searchLink fieldCode="DE" term="%22Logic+programming%22">Logic programming</searchLink>
– Name: Abstract
  Label: Abstract
  Group: Ab
  Data: Abstract: Functional test generation coupled with symbolic simulation offers a good compromise between formal verification and numerical simulation for design validation. The generation of functional test vectors guided by miscellaneous coverage metrics can be posed as a satisfiability problem (SAT). While a number of efficient Boolean SAT engines have been developed for gate level designs, they are not directly applicable to behavioral and RTL designs containing significant arithmetic components. This paper presents two approaches that enhance the capability of functional test generation by preserving arithmetic operators in the design. They are based on word-level SAT techniques: (1) LPSAT, based on integer linear programming, and (2) CLP-SAT, based on constraint logic programming. The proposed SAT solvers allow to efficiently handle the designs with mixed word-level arithmetic operators and bit-level logic gates. The experimental results are quite encouraging compared to traditional CNF-based and BDD-based SAT solvers. The paper also suggests a method to build an integrated SAT solving framework where different SAT solvers work together to provide a more complete solution to functional test generation and other verification applications. [Copyright &y& Elsevier]
– Name: AbstractSuppliedCopyright
  Label:
  Group: Ab
  Data: <i>Copyright of Journal of Systems Architecture is the property of Elsevier B.V. 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=18145381
RecordInfo BibRecord:
  BibEntity:
    Identifiers:
      – Type: doi
        Value: 10.1016/j.sysarc.2004.10.006
    Languages:
      – Code: eng
        Text: English
    PhysicalDescription:
      Pagination:
        PageCount: 24
        StartPage: 488
    Subjects:
      – SubjectFull: Slosson Intelligence Test
        Type: general
      – SubjectFull: Mathematics
        Type: general
      – SubjectFull: RTL (Computer program language)
        Type: general
      – SubjectFull: Logic programming
        Type: general
    Titles:
      – TitleFull: Functional test generation based on word-level SAT
        Type: main
  BibRelationships:
    HasContributorRelationships:
      – PersonEntity:
          Name:
            NameFull: Zeng, Zhihong
      – PersonEntity:
          Name:
            NameFull: Talupuru, Kesava R.
      – PersonEntity:
          Name:
            NameFull: Ciesielski, Maciej
    IsPartOfRelationships:
      – BibEntity:
          Dates:
            – D: 01
              M: 08
              Text: Aug2005
              Type: published
              Y: 2005
          Identifiers:
            – Type: issn-print
              Value: 13837621
          Numbering:
            – Type: volume
              Value: 51
            – Type: issue
              Value: 8
          Titles:
            – TitleFull: Journal of Systems Architecture
              Type: main
ResultId 1