4 ms·

Down karma, so might as well comment some more, so yes it seems weird that ARM wouldn't have a way to do this in-house. How do they prove to the fab houses tha

Down karma, so might as well comment some more, so yes it seems weird that ARM wouldn't have a way to do this in-house. How do they prove to the fab houses that the chip specs are good and don't have errors. With the high cost to make one, I think I'd like know that it's really going to work. Since the OP works for ARM, good that they are starting to do this. And since they are in the best position to see everything, it will be something that other vendors can rely on for their designs.

akiselev 10y ago
This article is about testing the implementations of various ARM processors (eight different product lines in various stages of design and production, according to the conclusion section) against the general ARM-v8m architecture specification that the manufacturers received as part of their licensing deal. Many of the processors already exist in the real world in smartphones and other hardware, this is just testing how many errors each manufacturer made when they took the IP and designed a physical chip, which are much bigger than just the ARM architecture. This is not verifying whether the specification and architectural decisions are bug free.
- adreid 10y ago
  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 10y ago
    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 ﬁnd and ISA-Formal is now a key part of ARM’s formal veriﬁcation 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?

akiselev 10y ago

This article is about testing the implementations of various ARM processors (eight different product lines in various stages of design and production, according to the conclusion section) against the general ARM-v8m architecture specification that the manufacturers received as part of their licensing deal. Many of the processors already exist in the real world in smartphones and other hardware, this is just testing how many errors each manufacturer made when they took the IP and designed a physical chip, which are much bigger than just the ARM architecture. This is not verifying whether the specification and architectural decisions are bug free.

adreid 10y ago
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 10y ago
  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 ﬁnd and ISA-Formal is now a key part of ARM’s formal veriﬁcation 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?