Publication: Linking simulation with formal verification at a higher level
dc.contributor.coauthor | Yu, Yuan | |
dc.contributor.coauthor | Batson, Brannon | |
dc.contributor.department | Department of Computer Engineering | |
dc.contributor.kuauthor | Taşıran, Serdar | |
dc.contributor.schoolcollegeinstitute | College of Engineering | |
dc.date.accessioned | 2024-11-09T23:10:00Z | |
dc.date.issued | 2004 | |
dc.description.abstract | We 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.indexedby | Scopus | |
dc.description.issue | 6 | |
dc.description.openaccess | YES | |
dc.description.publisherscope | International | |
dc.description.sponsoredbyTubitakEu | N/A | |
dc.description.volume | 21 | |
dc.identifier.doi | 10.1109/MDT.2004.94 | |
dc.identifier.issn | 0740-7475 | |
dc.identifier.quartile | Q1 | |
dc.identifier.scopus | 2-s2.0-11244327859 | |
dc.identifier.uri | https://doi.org/10.1109/MDT.2004.94 | |
dc.identifier.uri | https://hdl.handle.net/20.500.14288/9385 | |
dc.keywords | Cache memory | |
dc.keywords | Computer hardware description languages | |
dc.keywords | Computer simulation | |
dc.keywords | Formal languages | |
dc.keywords | High level languages | |
dc.keywords | Integrated circuit layout | |
dc.keywords | Microprocessor chips | |
dc.keywords | Cache coherence protocol | |
dc.keywords | Executable formal specification | |
dc.keywords | Formal verification | |
dc.keywords | Computer circuits | |
dc.language.iso | eng | |
dc.publisher | IEEE | |
dc.relation.ispartof | IEEE Design and Test of Computers | |
dc.subject | Computer Engineering | |
dc.title | Linking simulation with formal verification at a higher level | |
dc.type | Journal Article | |
dspace.entity.type | Publication | |
local.contributor.kuauthor | Taşıran, Serdar | |
local.publication.orgunit1 | College of Engineering | |
local.publication.orgunit2 | Department of Computer Engineering | |
relation.isOrgUnitOfPublication | 89352e43-bf09-4ef4-82f6-6f9d0174ebae | |
relation.isOrgUnitOfPublication.latestForDiscovery | 89352e43-bf09-4ef4-82f6-6f9d0174ebae | |
relation.isParentOrgUnitOfPublication | 8e756b23-2d4a-4ce8-b1b3-62c794a8c164 | |
relation.isParentOrgUnitOfPublication.latestForDiscovery | 8e756b23-2d4a-4ce8-b1b3-62c794a8c164 |