[adreid]

A few clarifications:

The paper is about searching for bugs in ARM's designs - not designs by ARM's architecture licensees. (ARM has two types of partner: those who use ARM designed processors exactly as provided by ARM and those who create their own processors implementing ARM's architecture.)

The tests are performed on the Verilog. There are very good and thorough techniques such as Logical Equivalence Checking (LEC) for verifying that what gets taped out actually matches the Verilog.

We used the v8-A architecture spec that provides Virtual Memory and other features you need to support Linux, Android, etc. This is the architecture that applies to phones, tablets, servers, etc.

And we used the v8-M architecture spec that applies to micro-controllers.

Also, it is worth saying that this is only one of many verification techniques used. This one focuses on the processor pipeline rather than the memory system, instruction fetch, etc.

[akiselev]

I'm very confused and as the author I hope you can clarify this. The conclusion of the paper states:

》 This paper describes the steps needed to turn the basic idea into a scal- able, reusable technique: automation, dealing with a range of diferent micro- architectural design techniques, and initial bringup issues. We have applied this method to 8 diferent 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 methods to find and ISA-Formal is now a key part of ARM’s formal verification strategy. (emphasis mine)

Are you verifying that the Verilog code provided by ARM for the former type of partner matches what's on the processor after the whole synthesis and fabrication process or are you verifying that the Verilog matces a higher level spec?