Automatic generation of hardware checkers from formal micro-architectural specifications

Alexander Fedotov, Julien Schmaltz

Onderzoeksoutput: Hoofdstuk in Boek/Rapport/CongresprocedureConferentiebijdrageAcademicpeer review

Samenvatting

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.

Originele taal-2Engels
TitelProceedings of the 2018 Design, Automation and Test in Europe Conference and Exhibition, DATE 2018
UitgeverijInstitute of Electrical and Electronics Engineers
Pagina's1568-1573
Aantal pagina's6
Volume2018-January
ISBN van elektronische versie9783981926316
DOI's
StatusGepubliceerd - 19 apr 2018
Evenement21st Design, Automation and Test in Europe Conference and Exhibition (DATE 2018) - Dresden, Duitsland
Duur: 19 mrt 201823 mrt 2018
Congresnummer: 21
https://www.date-conference.com/date18/

Congres

Congres21st Design, Automation and Test in Europe Conference and Exhibition (DATE 2018)
Verkorte titelDATE 2018
LandDuitsland
StadDresden
Periode19/03/1823/03/18
Internet adres

Vingerafdruk Duik in de onderzoeksthema's van 'Automatic generation of hardware checkers from formal micro-architectural specifications'. Samen vormen ze een unieke vingerafdruk.

  • Citeer dit

    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, blz. 1568-1573). Institute of Electrical and Electronics Engineers. https://doi.org/10.23919/DATE.2018.8342265