NASA Office of Logic Design

NASA Office of Logic Design

A scientific study of the problems of digital engineering for space flight systems,
with a view to their practical solution.


2005 MAPLD International Conference

Ronald Reagan Building and International Trade Center
Washington, D.C.

September 7-9, 2005

Session W: Verification of Large Designs and Related Design Methodologies

Wes Powell, NASA Goddard Space Flight CenterJohn Lach, University of Virginia
Session Chairs:
Wes Powell, NASA Goddard Space Flight Center
John Lach, University of Virginia
 


Session W will be in an informal workshop format and will be open to all MAPLD attendees. This is the first year for this session and is being created based on interest from a number of MAPLD participants.

Session W will held in the Continental B room and consist of two segments:

 

"We aren't dealing with ordinary machines here. These are highly complicated pieces of equipment almost as complicated as living organisms. In some cases, they've been designed by other computers.   We don't know exactly how they work."

-- Scientist in Michael Crichton's 1973 movie, Westworld

Description

This session will address the issues in verification strategies for large FPGA designs for space applications developed using high-level design tools.

Designers on upcoming missions are being faced with the dilemma of how to develop large, high performance FPGA applications while still being able to verify them with an acceptable degree of rigor. The size of today's FPGAs and the complexity of the applications are driving designers to use high-level tools where the design is specified at higher level of abstraction that conventional hardware description languages. However, with these tools the designer can be very removed from the actual logic that is being produced. A similar situation exists with the use of third party IP cores, which are used as "black boxes" in designs and where the degree and rigor of their testing may be unknown.

Hence, a very real challenge is how to verify designs developed with these tools to ensure that they are sufficiently robust for space applications. Spaceflight FPGA designs, especially those for mission and safety-critical applications, are often analyzed at the gate level. It will be very difficult (if not impossible) to perform this level of verification with the output of high-level tools and third party IP cores. Tools that automatically insert redundancy into synthesized netlists will complicate this even further.

Topics for discussion:

  1. Verification methods and strategies for large FPGA applications developed with high-level design tools and third party IP cores.
  2. Assessments of appropriate spaceflight uses for these applications.

 

Wednesday, 4:05 to 5:35 pm

4:05 pm   Submission 185
"A Verified Implementation of a Control System"
Alistair A. McEwan1 and J. C. P. Woodcock2
1
University of Surrey
2University of York
Abstract: mcewan_a.html
Paper: 185_mcewan_p.pdf
Presentation: bof_mcewan_bof-w.pdf
4:20 pm   Submission 226
"Using Software Rules to Enhance FPGA Reliability"
Chandru Mirchandani
Lockheed Martin Transportation and Security Solutions
Abstract: mirchandani_a.html
Presentation: mirchandani_p.ppt,   mirchandani-bof-w.ppt
Paper: mirchandani_paper.doc
4:35 pm   Submission 116
"Reliable SW/HW Co-Design for Wireless Communication System Integrating the Spin Model Checker and Celoxica's DK Suite"
Stefanos Skoulaxinos
Heriot-Watt University
Abstract: skoulaxinos_a.pdf
Presentation: skoulaxinos_p.pptskoulaxinos_poster.ppt,   skoulaxinos_bof_w.ppt
4:50 pm   Submission 177
"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
Abstract: jones_a.html
Presentation: jones_p.pptjones_bof-w.ppt
5:05 pm   Submission 247
"Design, Development and Validation Testing of a Versatile PLD Implementable Single-Chip Heterogeneous, Hybrid and Reconfigurable Multiprocessor Architecture"
J. Robert Heath, Sridhar Hegde, Kanchan Bhide, Paul Maxwell, Xiaohui Zhao, and Venugopal Duvvuri
University of Kentucky
Abstract: heath_a.html
5:20 pm   Submission 241
"Accessible Formal Verification for Safety-Critical FPGA Design"
John Lach1, Scott Bingham1, Carl Elks1, Travis Lenhart1, Thuy Nguyen2, Patrick Salaun2
1
University of Virginia
2Electricité de France
Abstract: lach_a.html
Presentation: lach_p.ppt,   lach_bof-w.ppt

 


Thursday, 4:30 to 6:00 pm

4:30 pm   Submission 237
"Verification of Intellectual Property for FPGA Designs"
Ian Land
Actel Corporation
Abstract: land_2_a.html
Presentation: land_p.pptland_bof-w.ppt
4:45 pm   Submission 170
"Verification of Moderate Complexity IP: Case Study, MIL-STD-1553B Interface"
Rod Barto
NASA Office of Logic Design
Abstract: barto_2_a.html
Presentation: barto_p.ppt,   barto_bof-w.ppt
5:00 pm   Submission 1014"FT-UNSHADES: A New System for SEU Injection, Analysis and Diagnostics over Post Synthesis Netlist"
M. Aguirre1, J.N. Tombs1, F. Muñoz1, V. Baena1, A. Torralba1, A. Fernández-León2, F. Tortosa-López2
1
Escuela Superior de Ingenieros Universidad de Sevilla Camino de los Descubrimientos
2Data Systems Division. ESTEC/TOS-ED European Space Agency
Abstract: aguirre_a.html
Presentation: aguirre_p.ppt
5:15 pm   Submission 157
"Multi-level Simulation of a Real Time Vibration Monitoring System Component"
Bryan Robertson and DeLisa Wilkerson
NASA/Marshall Space Flight Center
Abstract: robertson_a.html
Presentation: robertson_p.ppt,   robertson_bof-w.ppt
5:30 pm   Submission 193
"Extending FPGA Verification Through The PLI"
Charlie Howard
Southwest Research Institute
Abstract: howard_a.html
Presentation: howard_p.ppt,   howard_bof-w.ppt
Paper: howard_paper.doc
5:45 pm   Submission 145
"Methods to Differentiate Mil/Aero Solutions Using FPGA"
Dan Gardner
Mentor Graphics Corporation
Abstract: gardner_2_a.html
Presentation: gardner_p.ppt,   gardner_bof-w.ppt

2005 MAPLD International Conference Home Page


Home - NASA Office of Logic Design
Last Revised: February 03, 2010
Digital Engineering Institute
Web Grunt: Richard Katz
NACA Seal