Automatic generation of hardware checkers from formal micro-architectural specifications

Alexander Fedotov, Julien Schmaltz

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

Abstract

To manage design complexity, high-level models are used to evaluate the functionality and performance of design solutions. There is a significant gap between these high-level models and the Register Transfer Level (RTL) implementations actually produced by designers. We address the challenge of bridging this gap, namely, relating abstract specifications to RTL implementations. An important feature of our proposed approach is to support non-deterministic specifications. From such a non-deterministic model, we automatically compute a representation of its observable behaviour. We then turn this representation into a System Verilog checker. The checker is connected to the input and output interfaces of the RTL implementation. The resulting combination is given to a commercial EDA tool to prove inclusion of the traces of the implementation into the traces of the specification. Our method is implemented for the formal micro-architectural description language (MaDL) - an extension of the xMAS formalism originally proposed by Intel - and exemplified on several examples.

Original languageEnglish
Title of host publicationProceedings of the 2018 Design, Automation and Test in Europe Conference and Exhibition, DATE 2018
PublisherInstitute of Electrical and Electronics Engineers
Pages1568-1573
Number of pages6
Volume2018-January
ISBN (Electronic)9783981926316
DOIs
Publication statusPublished - 19 Apr 2018
Event21st Design, Automation and Test in Europe Conference and Exhibition (DATE 2018) - Dresden, Germany
Duration: 19 Mar 201823 Mar 2018
Conference number: 21
https://www.date-conference.com/date18/

Conference

Conference21st Design, Automation and Test in Europe Conference and Exhibition (DATE 2018)
Abbreviated titleDATE 2018
CountryGermany
CityDresden
Period19/03/1823/03/18
Internet address

Fingerprint Dive into the research topics of 'Automatic generation of hardware checkers from formal micro-architectural specifications'. Together they form a unique fingerprint.

  • Cite this

    Fedotov, A., & Schmaltz, J. (2018). Automatic generation of hardware checkers from formal micro-architectural specifications. In Proceedings of the 2018 Design, Automation and Test in Europe Conference and Exhibition, DATE 2018 (Vol. 2018-January, pp. 1568-1573). Institute of Electrical and Electronics Engineers. https://doi.org/10.23919/DATE.2018.8342265