Automatic generation of hardware checkers from formal micro-architectural specifications

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.

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
StatePublished - 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

Specifications
Hardware
Computer hardware description languages
Inclusion
Functionality
Language
Formalism

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. DOI: 10.23919/DATE.2018.8342265
Fedotov, Alexander ; Schmaltz, Julien. / Automatic generation of hardware checkers from formal micro-architectural specifications. Proceedings of the 2018 Design, Automation and Test in Europe Conference and Exhibition, DATE 2018. Vol. 2018-January Institute of Electrical and Electronics Engineers, 2018. pp. 1568-1573
@inproceedings{52fbcae559e5474f8cc69e296c7b2c19,
title = "Automatic generation of hardware checkers from formal micro-architectural specifications",
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.",
author = "Alexander Fedotov and Julien Schmaltz",
year = "2018",
month = "4",
day = "19",
doi = "10.23919/DATE.2018.8342265",
language = "English",
volume = "2018-January",
pages = "1568--1573",
booktitle = "Proceedings of the 2018 Design, Automation and Test in Europe Conference and Exhibition, DATE 2018",
publisher = "Institute of Electrical and Electronics Engineers",
address = "United States",

}

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, Institute of Electrical and Electronics Engineers, pp. 1568-1573, 21st Design, Automation and Test in Europe Conference and Exhibition (DATE 2018), Dresden, Germany, 19/03/18. DOI: 10.23919/DATE.2018.8342265

Automatic generation of hardware checkers from formal micro-architectural specifications. / Fedotov, Alexander; Schmaltz, Julien.

Proceedings of the 2018 Design, Automation and Test in Europe Conference and Exhibition, DATE 2018. Vol. 2018-January Institute of Electrical and Electronics Engineers, 2018. p. 1568-1573.

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

TY - GEN

T1 - Automatic generation of hardware checkers from formal micro-architectural specifications

AU - Fedotov,Alexander

AU - Schmaltz,Julien

PY - 2018/4/19

Y1 - 2018/4/19

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=85048789673&partnerID=8YFLogxK

U2 - 10.23919/DATE.2018.8342265

DO - 10.23919/DATE.2018.8342265

M3 - Conference contribution

VL - 2018-January

SP - 1568

EP - 1573

BT - Proceedings of the 2018 Design, Automation and Test in Europe Conference and Exhibition, DATE 2018

PB - Institute of Electrical and Electronics Engineers

ER -

Fedotov A, Schmaltz J. 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. Institute of Electrical and Electronics Engineers. 2018. p. 1568-1573. Available from, DOI: 10.23919/DATE.2018.8342265