Innovation in Verification March 2020

This blog is the next in a series in which Paul Cunningham (GM of the Verification Group at Cadence), Jim Hogan and I pick a paper on a novel idea we appreciated and suggest opportunities to further build on that idea.

We welcome comments on our blogs and suggestions for new topics if they’re based on published work.

The Innovation

Our next pick is End-to-End Concolic Testing for Hardware/Software Co-Validation. The paper was presented June 2019 at the ICESS conference. The authors are from Intel Hillsboro and Portland State University.

“Concolic” is a combination of concrete and symbolic, a method to increase coverage in very complex systems through an intermingling of direct code execution/simulation (at the instruction level) and symbolic analysis. Symbolic can do a more general analysis than direct (like formal), while direct execution helps bound these to be near realistic execution paths and can be used to handle libraries/IP inaccessible to symbolic analysis.

The authors earlier build on their own concolic platform, Crete, which they have described in an earlier paper, there applied only to analysis of software utilities. Crete first traces conventional execution through instruction sequences and states, in this instance tracing the system and each IP (here modeled as a virtual model), then flattening that hierarchy into a combined trace.

In the current paper, the trace is instrumented with assertions and symbolic values at hardware/software interfaces. The instrumented trace is then submitted to a concolic analysis. Interesting new traces discovered in this flow, where they violate an assertion for example, can be fed back to directed simulation for further analysis.

Concolic methods are already used in software testing, for example Microsoft reported use of these methods in testing Windows 7. Development and advances we have seen are so far academic or in-house.

Paul

This is an intriguing paper and mature in the scale and type of system they use to analyze their method (a complete mini system with OS, Driver, virtual E1000 Ethernet adapter and virtual 8051 CPU). I like that they consider realistic challenges and limitations. For example, they have thought about how to handle address translation from virtual to physical. Generally, they have pretty robust and scalable ways to instrument verification through callbacks inserted into the instruction stream.

I see a conceptual similarity with constrained random simulation. Constrained-random is a semi-random generation of traces in which each trace is discrete, where a single testbench can generate many traces. Conversely, concolic takes a single discrete trace and abstracts/symbolizes parts of that trace.

I have a couple of thoughts. First, to enable concolic simulation initial analysis must capture virtual model states along the trace. How will this work if you’re using commercial virtual platforms? Should it be an ecosystem play? Virtual component providers may need to offer a mechanism for save/restore in support of concolic methods.

The other point (which the authors fully acknowledge), is that to become really valuable, this testing needs to be able to work with multiple threads/interleaving traces (multiple IPs running concurrently). That will be a harder problem and got me thinking again about portable stimulus, about how you might randomize or explore that space of different concurrent traces. Could we extend PSS / Perspec into concolic? That would be an intriguing direction. Again, I would be interested in helping anyone in academia who wants to explore this idea further.

Finally, they found a couple of real bugs in QEMU, impressive in a well-tested model. I’d like to know more about these, also their take on what made concolic uniquely suited to finding these bugs, versus other approaches such as randomized testing.

Jim

First, I like the idea of system level testing coming together in a unified verification suite.

This area is probably too early stage to be talking about investment potential. When it does reach more maturity, it looks like a technology rather than an independent tool. I get the impression that there will be a million of these good ideas. We’ve already discussed a couple in earlier blogs. Great for verification but the verification team isn’t going to want to see more and more tools.

Maybe we should look at these as widgets that sit inside the primary verification platform. Maybe follow Paul’s idea that PSS is the cockpit where you pull down different apps depending on what kind of verification coverage you’re looking for.

Me

A very simple software example to illustrate a plus for concolic testing over randomized testing is:

int foo(…) { …

if (img.magic != 0xEEEE) return -1;

if (img.h > 1024) return -1;

return img.sz / img.h;

}

This can trigger an error on the division if img.h is 0. Randomized testing has to survive two branches and have the correct value of img.h to trigger that error. Concolic can justify a method to get past both branches, and through symbolic simulation can consider all cases for img.h. Randomization is much simpler in many cases, but concolic can be more effective in threading a path through these complex cases. I see definite value in improving branch coverage in this way for security, maybe also safety and more generally functional reliability.

To see the next paper, click HERE.

To see the previous paper click HERE.