Skip to Content

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

Posted on

Authors:

  • Joosten, Sebastiaan J. C.
  • Schmaltz, Julien

Published in: Design, Automation & Test in Europe pp 1413–1418

Paper

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.

BibTeX entry:

@inproceedings{Joosten15,
 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.},
 author = {Joosten, Sebastiaan Jozef Christiaan and Schmaltz, Julien},
 booktitle = {Design, Automation \& Test in Europe},
 month = {Mar},
 organization = {EDA Consortium},
 pages = {1413--1418},
 title = {Automatic extraction of micro-architectural models of communication fabrics from register transfer level designs},
 year = {2015}
}