Research Results | FPGA Finite State Machine (FSM) Modeling and Analysis


	Search:	Advanced Search

Domain-Specific Analysis < Verification & Validation < Results Home

Click here to complete a short survey. The results of this survey will be used to help us improve the research program and this website.

Click here to view research projects that had new research results added in the last 90 days.

FPGA Finite State Machine (FSM) Modeling and Analysis
Point of Contact	Jack Smith jack.smith@matricresearch.com
Dates	June 2006 - December 2006
Problem	Finite State Machines (FSMs) are used in many spaceflight software development efforts and play a significant role in FPGA design and development. Since an increasing number of spaceflight hardware components include FPGAs, and the mission-critical software interfaces to these systems (as well as embedded software), the FPGA FSMs should be rigorously exercised and analyzed. There are several research-capable tools (e.g. PROMELA/Spin) and industry tools that perform FSM modeling and analysis activities. We are interested in identifying the "best of breed" for usage in IV&V projects (where appropriate). This has applicability beyond the FPGA domain, into other IV&V project areas where FSMs are used. Large (many states) and complex (varying state transitions) FSMs can complicate any IV&V effort. Automated checking of FSM properties would alleviate much of this effort. However, many tools have varying input parameters (e.g. state transition tables versus diagrams) and algorithms for analysis. We propose to identify the "best of breed" for IV&V practitioner usage. Of important note, there has been a recent increase, and understandably so, of NASA projects (for example, James Webb Space Telescope, Kepler, NPP, MRO, etc) utilizing FPGAs (and their underlying FSMs).
Objective	Phase 1-To Compare/Contrast Tools for FSM Modeling and Analysis. Our solution is to gather a suite of tools for tandem compare/contrast utilizing a single, selected IV&V project. Phase 2-To Down-select Tools Based on Phase 1 Results. And, perform an in-depth compare/contrast study utilizing multi-project data sets.
Results	SAS 06 Executive Presentation.ppt SAS 06 Technical Presentation.ppt
Keywords
Categories	Code Analysis Domain-Specific Analysis Dynamic Analysis Formal Methods Static Analysis Test Analysis

Curator: Josh Stonestreet
NASA Official: Lisa Montgomery

NASA Privacy, Security, Notices