Using Mathematica for Modeling, Simulation, and Property Checking of Hardware Systems

Ghiath Al Sammane

TIMA laboratory

Abstract

In the context of large hardware systems design, the functional specifications are written at an abstract level and executed on numeric test cases, as a first approach to debug the model from its most obvious errors. The simulation of the model behavior on numeric data is a well-understood technique that will not be replaced, but that cannot provide exhaustive checking. On the other hand, mathematical reasoning and theorem proving have been successfully applied to the validation of computer systems and to find subtle bugs, but their use requires significant expertise and a large formalization effort. Mathematica is used in our research team as a symbolic verification system that bridges the gap between numerical simulation and formal verification techniques. During this talk, we illustrate our work on a simplified 2-bit priority-based arbiter.