Title: Tool assisted development and validation of architectural timing models
Advisors: Dan Grossman and Luis Ceze
Abstract: We present a tool-assisted approach for development and validation of architectural timing models. Our tool assists development by allowing models to be specified as abstract sketches of timing behavior. For example, a timing model sketch might state that a move instruction takes k1 cycles while a jump takes k2. We use the Z3 SMT solver to either synthesize a concrete model from this sketch by finding k1 and k2, or provide a counterexample that demonstrates to the user why no such k1 and k2 can exist. Additionally, our tool assists validation of timing models for specific processor architectures by observing real, physical hardware. We use our approach to build a timing model for the TI MSP430 fr5969 microcontroller. The resulting model exposes many inaccuracies in the official TI user manual and in existing emulators, and we show that it is cycle-accurate for code from a variety of applications when compared to the behavior of physical hardware devices.