The instruction set architecture (ISA) specifies a contract between hardware and software; it covers all possible operations that have to be performed by a processor, regardless of the implemented architecture. Verifying the instruction execution against a golden execution model following the ISA is becoming a common practice to verify processors. Despite many potential applications, existing verification frameworks require an extensive test set to cover most of the processor states. In this paper, we suggest a verification scheme combining two different domains, simulation- and formal-verification, establishing a methodology for exclusive error detection. The first approach drives automatic program generation using genetic algorithms to maximize coverage of the test and the contrast against an instruction set simulator. The second is a formal verification approach, where an interface carries specific processor states according to the ISA specification. By combining these two, we present a reliable way to perform more accurate instruction verification by increasing processor state coverage and formal assertions to detect different kinds of errors. Compared to extensive torture test sets, this approach reaches a more significant number of internal states by taking advantage of the exercised abstractions. Among remarkable results to highlight, the proposed approach detected a RISC-V ISA specification gap revealing ambiguity from two different verification perspectives.

Simulation and Formal: The Best of Both Domains for Instruction Set Verification of RISC-V Based Processors / Duran, Ckristian; Morales, Hanssel; Rojas, Camilo; Ruospo, Annachiara; Ernesto, Sanchez; Roa, Elkim. - ELETTRONICO. - (2020). (Intervento presentato al convegno IEEE International Symposium on Circuits and Systems (ISCAS) tenutosi a Virtual Event nel from October 10 to October 21 2020) [10.1109/ISCAS45731.2020.9180589].

Simulation and Formal: The Best of Both Domains for Instruction Set Verification of RISC-V Based Processors

Annachiara Ruospo;Ernesto Sanchez;
2020

Abstract

The instruction set architecture (ISA) specifies a contract between hardware and software; it covers all possible operations that have to be performed by a processor, regardless of the implemented architecture. Verifying the instruction execution against a golden execution model following the ISA is becoming a common practice to verify processors. Despite many potential applications, existing verification frameworks require an extensive test set to cover most of the processor states. In this paper, we suggest a verification scheme combining two different domains, simulation- and formal-verification, establishing a methodology for exclusive error detection. The first approach drives automatic program generation using genetic algorithms to maximize coverage of the test and the contrast against an instruction set simulator. The second is a formal verification approach, where an interface carries specific processor states according to the ISA specification. By combining these two, we present a reliable way to perform more accurate instruction verification by increasing processor state coverage and formal assertions to detect different kinds of errors. Compared to extensive torture test sets, this approach reaches a more significant number of internal states by taking advantage of the exercised abstractions. Among remarkable results to highlight, the proposed approach detected a RISC-V ISA specification gap revealing ambiguity from two different verification perspectives.
File in questo prodotto:
File Dimensione Formato  
ISCAS_2020_Simulation_n_Formal_Camera.pdf

accesso aperto

Tipologia: 2. Post-print / Author's Accepted Manuscript
Licenza: PUBBLICO - Tutti i diritti riservati
Dimensione 449.1 kB
Formato Adobe PDF
449.1 kB Adobe PDF Visualizza/Apri
09180589.pdf

non disponibili

Tipologia: 2a Post-print versione editoriale / Version of Record
Licenza: Non Pubblico - Accesso privato/ristretto
Dimensione 360.22 kB
Formato Adobe PDF
360.22 kB Adobe PDF   Visualizza/Apri   Richiedi una copia
Pubblicazioni consigliate

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11583/2845745