The Pelican Has Landed: Formal on an Unannounced ARM Processor

At the Jasper Users’ Group, Alex Netterville of ARM presented about how ARM are using formal on an unannounced processor code-named Pelican. Don’t read the presentation trying to find out information about Pelican itself, there isn’t any. That wasn’t the topic. Alex has been using formal approaches for 10 years and worked on the ARM Cortices R4, A9, A5, and M0+.

The approach he discussed was using formal approaches for all interfaces, precisely stating the way that the interface between two subsystems should behave, and without peeking inside the subsystems. These definitions have to exist or nobody can design the subsystems, but word of mouth is a terrible way to do it, a Word document is better since at least it is written down and changes can be tracked, but a writing formal properties is the best since it is executable and it is possible to check whether the subsystems do indeed implement the specified behavior (subject to some caveats, of course).

At the start of the project the interface specs are owned by the microarchitects. Unit level designers share ownership throughout the project, keeping them up to date along with the RTL. But before RTL is written, they allow a formal bench to be created and block I/O behavior to be examined with Jasper Visualize.

Properties need to be written in a way that adapts to the environment. If only one block is present they are checking either the outputs or the inputs (depending on which block it is) and assuming that the other block (which isn’t present) is correct. If both blocks are present they are eavesdropping on the traffic and checking it conforms.

Specifications are simple and non-verbose, using a pseudo language that was created with an optimal set of keywords. From that they can generate OVL, SVA, Jasper TCL etc. The typical size of one of these “.i” files is from tens of lines to thousands of lines. But the generated files are typically 4-6X bigger.

The interface specifications are used at several levels. At the unit-level, when a block is isolated from its environment, it is used to constrain inputs and check outputs. At the top level (or higher levels) it is used to check the interaction of sub-blocks.

One challenge with formal at ARM (see my earlier blog) is lowering the barriers to adoption so that designers use it. The test environment makes it easy to specify the test hierarchy, methodology and the configuration. Underlying Jasper-specific TCL then automatically builds and configures the appropriate design.

When all the blocks are put together there are often problems where tests either pass at the unit level but fail at the top level or vice versa. If it fails at the top but passes at sub-level then the assumptions at the input of a block might be too strong. The other way around, where they pass at the top but fail at the sub-level is because the assumptions at the input of the sub-block are too weak.

So what are the issues with this interface-centric methodology.

• Isolated unit level formal benches may not model the environmental context of that unit in the final product correctly in projects that don’t adopt this methodology
• Clocks and resets may not be attached to the correct interface specification
• System level modelling at top can sometimes be a compromise that doesn’t catch all use cases.
• A signal might be missing from an interface specification

There is more in the presentation. If you are a Jasper user (not necessarily one who attended JUG) then you can download the presentations, including this one, here.

More articles by Paul McLellan…