Personal tools
You are here: Home Events Lab Lunch by Brian Campbell

Lab Lunch by Brian Campbell

— filed under:

  • Lab Lunch
When May 12, 2015
from 01:00 PM to 02:00 PM
Add event to calendar vCal

Automated fuzz testing of formal processor models


A few weeks ago Ian described the REMS project at lab lunch.  Across the project we have several substantial formal models of processor instruction sets.  Validating these models against actual implementations isn't easy - even a simple processor's pipeline is handling several instructions at once and we want to know that they don't interfere with one another.

I'll describe our automatic test case generation for these models which runs sequences of randomly chosen instructions, using constraints gathered from the model and an automated theorem prover to choose a processor state where they won't crash.  I'll also mention what's so interesting about the models and processors we've been testing.

Document Actions