TY - GEN
T1 - Supporting RTL flow compatibility in a microarchitecture-level design framework
AU - Schwartz-Narbonne, Daniel
AU - Chan, Carven
AU - Mahajan, Yogesh
AU - Malik, Sharad
PY - 2009
Y1 - 2009
N2 - Current RTL-based design methodologies face significant scaling challenges related to the difficulty of designing, modifying, and verifying RTL. RTL contains primarily low level structural information about the design. In contrast, the microarchitecture-level is much closer to the specification level, making it an effective entry point for hardware design. The explicit description of the high-level units of work is also beneficial for verification. Currently used models for high level design have very complex semantics. In this paper, we present a microarchitectural modeling language with simpler semantics. We demonstrate that it results in a significantly simpler synthesis to Verilog, providing for integration with existing RTL flows. Moreover, the simple semantics of the model enable the generation of PSL assertions for functionally verifying correctness of the synthesis. We demonstrate the efficacy of this approach through two case-studies - -a router switch and a processor design. We synthesized both designs, and formally verified the synthesis using the generated assertions.
AB - Current RTL-based design methodologies face significant scaling challenges related to the difficulty of designing, modifying, and verifying RTL. RTL contains primarily low level structural information about the design. In contrast, the microarchitecture-level is much closer to the specification level, making it an effective entry point for hardware design. The explicit description of the high-level units of work is also beneficial for verification. Currently used models for high level design have very complex semantics. In this paper, we present a microarchitectural modeling language with simpler semantics. We demonstrate that it results in a significantly simpler synthesis to Verilog, providing for integration with existing RTL flows. Moreover, the simple semantics of the model enable the generation of PSL assertions for functionally verifying correctness of the synthesis. We demonstrate the efficacy of this approach through two case-studies - -a router switch and a processor design. We synthesized both designs, and formally verified the synthesis using the generated assertions.
KW - Formal models
KW - Hardware resources
KW - Hierarchical design
KW - Microarchitecture level
KW - Transactions
UR - http://www.scopus.com/inward/record.url?scp=72149109505&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=72149109505&partnerID=8YFLogxK
U2 - 10.1145/1629435.1629482
DO - 10.1145/1629435.1629482
M3 - Conference contribution
AN - SCOPUS:72149109505
SN - 9781605586281
T3 - Embedded Systems Week 2009 - 7th IEEE/ACM International Conference on Hardware/Software-Co-Design and System Synthesis, CODES+ISSS 2009
SP - 343
EP - 352
BT - Embedded Systems Week 2009 - 7th IEEE/ACM International Conference on Hardware/Software-Co-Design and System Synthesis, CODES+ISSS 2009
T2 - Embedded Systems Week 2009, ESWEEK 2009 - 7th IEEE/ACM International Conference on Hardware/Software-Co-Design and System Synthesis, CODES+ISSS 2009
Y2 - 11 October 2009 through 16 October 2009
ER -