Driven to Abstraction

Someday, in the not too distant future, I will be able to fall asleep, play computer games or write a bestselling novel at the wheel (well 2/3 isn’t bad). Until such time however, I have just the one option – concentrate deeply and blast the speakers with my classic rock and punk collection.

In the past few years I’ve clocked up a lot of miles slogging up and down the motorway between my hometown in Lancashire and the South East and it can get boring. On a recent drive, somewhere in the middle of Thin Lizzy’s Live & Dangerous, I started to wonder: I know how to get home from here, but I don’t know where I am. How can that be?

I know the 200 miles journey like the back of my hand, but all I actually remember are the important exits. When I reach junction 19 of the M1 I join the M6, if I’m feeling like losing a few quid I can take the toll road past Birmingham and I know where to exit for home, but I don’t know where I am in between. It’s all just filler in between those important exits where I need to take action. So long as I get to those exits eventually I’ll make it to my home.

It occurred to me that my brain had, subconsciously, performed an abstraction on the journey to make it more efficient to remember. When people who aren’t used to Formal hear about abstraction they often think it sounds like a strange concept, but it’s actually so natural and we don’t even think about it.

Let’s look at one example of how this concept could be applied to Formal. Imagine we need to verify a design containing a 12 bit counter and we aren’t getting conclusive results. This counter has 4096 different values that it can take… but are they all important? Counters usually are used to make decisions at particular values, out of 4096 there may only be 3 states that are actually important.

We could remove this counter from the design and create an abstract model for the counter that just contains 3 possible values: The three important states and one “unimportant state” to represent all others. By doing this we ask the Formal tool to only look at the important states. It is like get me home and don’t waste time worrying about if you’re near Northampton or Stoke. This can significantly reduce the verification time, and you can even get the Formal tool to automatically create an abstract counter model for you. You may of course later want to ensure that the counter moves correctly (sanity checks like I will reach the M6, and add performance check that I won’t go via Southampton).

Abstraction in Formal verification can get you faster results and it is nothing stranger than what you subconsciously do all the time.