Supporting RTL flow compatibility in a microarchitecture-level design framework

ABSTRACT

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.

REFERENCES

• 1: Verilog Register Transfer Level Synthesis. IEC 62142-2005 2005-06 IEEE Std 1364.1, pages 1--116.
• 2: IEEE Std 1666 - 2005 IEEE Standard SystemC Language Reference Manual. IEEE Std 1666-2005, pages 1--423, 2006.
• 3: Standard for SystemVerilog-Unified Hardware Design, Specification, and Verification Language. IEC 62530:2007 (E), pages 1--668, 2007.
• 4: D. August, S. Malik, L.-S. Peh, and V. Pai. Achieving structural and composable modeling of complex systems. Paral lel and Distributed Processing Symposium, 2004. Proceedings. 18th International, April 2004.
• 5: N. Blanc, D. Kroening, and N. Sharygina. Scoot: A tool for the analysis of SystemC models. In Proceedings of TACAS 2008, volume 4963 of LNCS, pages 467--470. Springer, 2008.
• 6: Cadence Design Systems. Incisive formal verifier. Online, http://www.cadence.com/, May 2009.
• 7: X. Chen, S. M. German, and G. Gopalakrishnan. Transaction based modeling and verification of hardware protocols. In FMCAD '07: Proc. of the Formal Methods in Computer Aided Design, pages 53--61. IEEE Computer Society, 2007.
• 8: W. Dally and B. Towles. Principles and Practices of Interconnection Networks. Morgan Kaufmann Publishers Inc., San Francisco, CA, USA, 2003.
• 9: D. Harel and E. Gery. Executable ob ject modeling with statecharts. Computer, 30(7):31--42, Jul 1997.
• 10: J. Hennessy and D. Patterson. Computer Architecture: A Quantitative Approach. Morgan Kaufmann, 2006.
• 11: J. Hoe and Arvind. Operation-centric hardware description and synthesis. Computer-Aided Design of Integrated Circuits and Systems, IEEE Transactions on, 23(9):1277--1288, Sept. 2004.
• 12: P. M. Kogge. The microprogramming of pipelined processors. In ISCA '77: Proceedings of the 4th annual symposium on Computer architecture, pages 63--69, New York, NY, USA, 1977. ACM.
• 13: Y. Maha jan, C. Chan, A. Bayazit, S. Malik, and W. Qin. Verification-driven formal architecture and microarchitecture modeling. Formal Methods and Models for Codesign, 2007. MEMOCODE 2007. 5th IEEE/ACM International Conference on, pages 123--132, 2007.
• 14: Y. Maha jan and S. Malik. Automating hazard checking in transaction-level microarchitecture models. Formal Methods in Computer Aided Design, pages 62--65, Nov. 2007.
• 15: J. Nestor. Teaching computer organization with HDLs: an incremental approach. Microelectronic Systems Education, 2005. Proceedings. 2005 IEEE International Conference on, pages 77--78, June 2005.
• 16: L.-S. Peh. Flow control and micro-architectural mechanisms for extending the performance of interconnection networks. PhD thesis, 2001. Adv. William J. Dally.
• 17: W. Qin and S. Malik. Flexible and formal modeling of microprocessors with application to retargetable simulation. Design, Automation and Test in Europe Conference and Exhibition, 2003, pages 556--561, 2003.
• 18: O. Schliebusch, A. Hoýmann, A. Nohl, G. Braun, and H. Meyr. Architecture implementation using the machine description language LISA. In ASP-DAC '02: Proceedings of the 2002 conference on Asia South Pacific design automation/VLSI Design, Washington, DC, USA, 2002. IEEE Computer Society.
• 19: C. Schulz-Key, M. Winterholer, T. Schweizer, T. Kuhn, and W. Rosenstiel. Ob ject-oriented modeling and synthesis of SystemC specifications. In ASP-DAC '04: Proceedings of the 2004 conference on Asia South Pacific design automation, pages 238--243, Piscataway, NJ, USA, 2004. IEEE Press.
• 20: S. Swan. SystemC transaction level models and RTL verification. Design Automation Conference, 2006 43rd ACM/IEEE, pages 90--92, 2006.
• 21: Synopsys Inc. Design compiler. Online, http://www.synopsys.com, May 2009.
• 22: S. Williams. Icarus Verilog. Online, http://icarus.com/eda/verilog, Nov. 2008.

INDEX TERMS

Primary Classification:
  B. Hardware
  B.5 REGISTER-TRANSFER-LEVEL IMPLEMENTATION
      B.5.2 Design Aids
          Subjects: Automatic synthesis

Additional Classification:
  B. Hardware
  B.5 REGISTER-TRANSFER-LEVEL IMPLEMENTATION
      B.5.2 Design Aids
          Subjects: Verification; Hardware description languages

General Terms:
Design, Languages, Verification

Keywords:
formal models, hardware resources, hierarchical design, microarchitecture level, transactions