Publication:
Linking simulation with formal verification at a higher level

dc.contributor.coauthorYu, Yuan
dc.contributor.coauthorBatson, Brannon
dc.contributor.departmentDepartment of Computer Engineering
dc.contributor.kuauthorTaşıran, Serdar
dc.contributor.schoolcollegeinstituteCollege of Engineering
dc.date.accessioned2024-11-09T23:10:00Z
dc.date.issued2004
dc.description.abstractWe use simulation to bridge the gap between specification and formal verification of high-level models and simulation of RTL models. The authors apply their practical, two-phase procedure for defining the refinement map to the Alpha 21364 multiprocessing hardware. The methodology and tools they present can improve simulation coverage. Our technique verifies that a hardware design described at the RTL is a correct implementation of an algorithm-level, executable formal specification. We use a high-level formal specification as the basis for monitoring functional correctness, measuring simulation coverage, and generating test cases.
dc.description.indexedbyScopus
dc.description.issue6
dc.description.openaccessYES
dc.description.publisherscopeInternational
dc.description.sponsoredbyTubitakEuN/A
dc.description.volume21
dc.identifier.doi10.1109/MDT.2004.94
dc.identifier.issn0740-7475
dc.identifier.quartileQ1
dc.identifier.scopus2-s2.0-11244327859
dc.identifier.urihttps://doi.org/10.1109/MDT.2004.94
dc.identifier.urihttps://hdl.handle.net/20.500.14288/9385
dc.keywordsCache memory
dc.keywordsComputer hardware description languages
dc.keywordsComputer simulation
dc.keywordsFormal languages
dc.keywordsHigh level languages
dc.keywordsIntegrated circuit layout
dc.keywordsMicroprocessor chips
dc.keywordsCache coherence protocol
dc.keywordsExecutable formal specification
dc.keywordsFormal verification
dc.keywordsComputer circuits
dc.language.isoeng
dc.publisherIEEE
dc.relation.ispartofIEEE Design and Test of Computers
dc.subjectComputer Engineering
dc.titleLinking simulation with formal verification at a higher level
dc.typeJournal Article
dspace.entity.typePublication
local.contributor.kuauthorTaşıran, Serdar
local.publication.orgunit1College of Engineering
local.publication.orgunit2Department of Computer Engineering
relation.isOrgUnitOfPublication89352e43-bf09-4ef4-82f6-6f9d0174ebae
relation.isOrgUnitOfPublication.latestForDiscovery89352e43-bf09-4ef4-82f6-6f9d0174ebae
relation.isParentOrgUnitOfPublication8e756b23-2d4a-4ce8-b1b3-62c794a8c164
relation.isParentOrgUnitOfPublication.latestForDiscovery8e756b23-2d4a-4ce8-b1b3-62c794a8c164

Files