| layout | year | volume | title | slides | series | publisher | png | pages | number | month | location | journal | isbn | file | editor | doi | booktitle | authors | ar_shortname | ar_file | affiliation | acceptance | abstract | ENTRYTYPE | ID | bibtex |
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
paper |
2016 |
9780 |
End-to-End Verification of ARM Processors with ISA-Formal |
cav2016_isa_formal-slides.pdf |
Lecture Notes in Computer Science |
Springer Verlag |
cav2016_isa_formal.png |
42-58 |
9780 |
July |
Toronto, Canada |
CAV 2016, Part II, Lecture Notes in Computer Science |
978-3-319-41539-0 |
cav2016_isa_formal.pdf |
S. Chaudhuri, A. Farzan |
10.1007/978-3-319-41540-6_3 |
Proceedings of the 2016 International Conference on Computer Aided Verification (CAV'16) |
Alastair Reid and Rick Chen and Anastasios Deligiannis and David Gilday and David Hoyes and Will Keen and Ashan Pathirane and Erin Shepherd and Peter Vrabel and Ali Zaidi |
CAV 16 |
CAV_16 |
ARM Ltd |
28 |
Despite 20+ years of research on processor verification, it remains hard to use
formal verification techniques in commercial processor development. There are
two significant factors: scaling issues and return on investment. The
scaling issues include the size of modern processor specifications, the
size/complexity of processor designs, the size of design/verification teams and
the (non)availability of enough formal verification experts. The return on
investment issues include the need to start catching bugs early in development,
the need to continue catching bugs throughout development, and the need to be
able to reuse verification IP, tools and techniques across a wide range of
design styles.
<p>
This paper describes how ARM has overcome these issues in our Instruction Set
Architecture Formal Verification framework ``ISA-Formal.'' This is an
end-to-end framework to detect bugs in the datapath, pipeline control and
forwarding/stall logic of processors. A key part of making the approach scale
is use of a mechanical translation of ARM's Architecture Reference Manuals to
Verilog allowing the use of commercial model-checkers. ISA-Formal has proven
especially effective at finding micro-architecture specific bugs involving
complex sequences of instructions.
<p>
An essential feature of our work is that it is able to scale all the way from
simple 3-stage microcontrollers, through superscalar in-order processors up to
out-of-order processors. We have applied this method to 8 different ARM
processors spanning all stages of development up to release. In all
processors, this has found bugs that would have been hard for conventional
simulation-based verification to find and ISA-Formal is now a key part of ARM's
formal verification strategy.
<p>
To the best of our knowledge, this is the most broadly applicable formal
verification technique for verifying processor pipeline control in mainstream
commercial use.
|
inproceedings |
conf/cav/Reid16 |
@inproceedings{conf/cav/Reid16
, abstract = {
Despite 20+ years of research on processor verification, it remains hard to use
formal verification techniques in commercial processor development. There are
two significant factors: scaling issues and return on investment. The
scaling issues include the size of modern processor specifications, the
size/complexity of processor designs, the size of design/verification teams and
the (non)availability of enough formal verification experts. The return on
investment issues include the need to start catching bugs early in development,
the need to continue catching bugs throughout development, and the need to be
able to reuse verification IP, tools and techniques across a wide range of
design styles.
<p>
This paper describes how ARM has overcome these issues in our Instruction Set
Architecture Formal Verification framework ``ISA-Formal.'' This is an
end-to-end framework to detect bugs in the datapath, pipeline control and
forwarding/stall logic of processors. A key part of making the approach scale
is use of a mechanical translation of ARM's Architecture Reference Manuals to
Verilog allowing the use of commercial model-checkers. ISA-Formal has proven
especially effective at finding micro-architecture specific bugs involving
complex sequences of instructions.
<p>
An essential feature of our work is that it is able to scale all the way from
simple 3-stage microcontrollers, through superscalar in-order processors up to
out-of-order processors. We have applied this method to 8 different ARM
processors spanning all stages of development up to release. In all
processors, this has found bugs that would have been hard for conventional
simulation-based verification to find and ISA-Formal is now a key part of ARM's
formal verification strategy.
<p>
To the best of our knowledge, this is the most broadly applicable formal
verification technique for verifying processor pipeline control in mainstream
commercial use.
}
, acceptance = {28}
, affiliation = {ARM Ltd}
, ar_file = {CAV_16}
, ar_shortname = {CAV 16}
, authors = {Alastair Reid and Rick Chen and Anastasios Deligiannis and
David Gilday and David Hoyes and Will Keen and Ashan Pathirane and
Erin Shepherd and Peter Vrabel and Ali Zaidi}
, booktitle = {Proceedings of the 2016 International Conference on Computer Aided Verification (CAV'16)}
, doi = {10.1007/978-3-319-41540-6\_3}
, editor = {S. Chaudhuri and A. Farzan}
, file = {cav2016_isa_formal.pdf}
, isbn = {978-3-319-41539-0}
, journal = {CAV 2016, Part II, Lecture Notes in Computer Science}
, location = {Toronto, Canada}
, month = {July}
, number = {9780}
, pages = {42-58}
, png = {cav2016_isa_formal.png}
, publisher = {Springer Verlag}
, series = {Lecture Notes in Computer Science}
, slides = {cav2016_isa_formal-slides.pdf}
, title = {{E}nd-to-{E}nd {V}erification of {A}RM {P}rocessors with {I}SA-{F}ormal}
, volume = {9780}
, year = {2016}
}
|