"On the Model-centric Design and Development of an FPGA-based Spaceborne Downlink Board"

Rob Jones, Roman Machan, Tahsin Lin, and Ed Leventhal
ASRC Aerospace Corporation


This article describes a novel, model-centric approach to the development of complex electronic systems in general, and an FPGA-based system in particular. Formal models were constructed using the Petri net (PN) language in a way that complements traditional VHDL model development, with the former driving the development of the latter. PNs can capture the diverse aspects of complex (computing and communications) systems, just as VHDL can, only formally and with analytical tractability that merely depends on the level of modeling power employed. For instance, a PN easily models state machines (finite automata with choice but no concurrency), dataflow graphs (concurrency but no choice), and queuing networks (dataflow with choice but no forks and joins), but it can also model much more complex algorithms and machines, including ones that are Turing equivalent.

As a formal model, the PN is mathematically based, well defined, and thus capable of unambiguous descriptions of design concepts and specifications. This can be done with arbitrary levels of abstraction and fidelity throughout the development life cycle, as this article shows. Formalisms like the PN allow computer-automated generation and analysis of the exact state space, all of the transitions the modeled system can take from one state to another, and the timing requirements of event sequences that cause these state transitions. An exact analysis of such behavior can prove design correctness in early development phases before committing to VHDL coding, FPGA synthesis, and hardware fabrication. PNs also enjoy a graphical form that is suitable for human consumption. This can aid requirements capture and traceability, notional design concept development, and design specifications.

This modeling approach was successfully applied to the design and development of an FPGA-based downlink board of high speed and complexity for space applications. As also discussed in this article, salient features include PCI and LVDS interfaces, (USES) lossless data compression, CCSDS packet formatting, and Reed-Solomon encoding. Through the use of PN models, system-level tradeoffs among design alternatives were studied and validated that optimized throughput, buffer sizes, dataflow control, and error containment strategies. These same models were then refined with increasing detail, driving the design to maturity, and verifying design correctness through rigorous analysis. Model-based testing was also performed, driven by simulated entropy rate data in realistic scenarios. All PN models were constructed and solved with the Stochastic Model-Checking Analyzer for Reliability and Timing (SMART), a toolset developed by researchers at the Univ. of California at Riverside and Iowa State Univ. at Ames, as well as this author, and funded in no small part by NASA.


2005 MAPLD International Conference Home Page