|
|
|
|
|
|
|
|
Using Mathematica for Modeling, Simulation, and Property Checking of Hardware Systems
|
|
|
|
|
|
Organization: | TIMA Laboratory |
|
|
|
|
|
|
2004 Wolfram Technology Conference
|
|
|
|
|
|
Champaign IL
|
|
|
|
|
|
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.
|
|
|
|
|
|
|
|
|
|
|
|
http://www.wolfram.com/news/events/techconf2004
|
|
|
|
|
|
| ghiathalsammane.nb (365.8 KB) - Abstract of talk | | slides-tech.ppt (356 KB) - Powerpoint presentation |
|
|