Automatic extraction of micro-architectural models of communication fabrics from register transfer level designs

S.J.C. Joosten, J. Schmaltz

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

7 Citations (Scopus)
5 Downloads (Pure)

Abstract

Multi-core processors and Systems-on-Chips are composed of a large number of processing and memory elements interconnected by complex communication fabrics. These fabrics are large systems made of many queues and distributed control logic. Recent studies have demonstrated that high levels models of these networks are either tractable for verification or can provide key invariants to improve hardware model checkers. Formally verifying Register Transfer Level (RTL) designs of these networks is an important challenge, yet still open. This paper bridges the gap between high level models and RTL designs. We propose an algorithm that from a Verilog description automatically produces its corresponding micro-architectural model. We prove that the extracted model is transfer equivalent to the original RTL circuit. We illustrate our approach on a typical example of communication fabrics: a scoreboard with credit-flow control.
Original languageEnglish
Title of host publication2015 Design, Automation & Test in Europe Conference & Exhibition (DATE, Grenoble, France, March 9-13, 2015)
Place of PublicationPiscataway NJ
PublisherInstitute of Electrical and Electronics Engineers
Pages1413-1418
ISBN (Print)978-3-9815-3704-8
Publication statusPublished - 2015

Fingerprint

Dive into the research topics of 'Automatic extraction of micro-architectural models of communication fabrics from register transfer level designs'. Together they form a unique fingerprint.

Cite this