WE WILL DESIGN AND FORMALLY VERIFY A VLIW PROCESSOR THAT IS RADIATION-HARDENED, AND WHERE THE VLIW INSTRUCT…

Public award description

WE WILL DESIGN AND FORMALLY VERIFY A VLIW PROCESSOR THAT IS RADIATION-HARDENED, AND WHERE THE VLIW INSTRUCTIONS CONSIST OF PREDICATED RISC INSTRUCTIONS FROM THE POWERPC 750 INSTRUCTION SET ARCHITECTURE (ISA). THE POWERPC 750 ISA IS USED IN THE RADIATION-HARDENED RAD750 FLIGHT-CONTROL COMPUTER THAT IS UTILIZED IN MANY NASA SPACE MISSIONS, INCLUDING DEEP IMPACT, THE MARS RECONNAISSANCE ORBITER, THE MARS ROVERS, AND IS PLANNED TO BE USED IN THE CREW EXPLORATION VEHICLE (CEV). THE VLIW PROCESSOR WILL HAVE RECONFIGURABLE FUNCTIONAL UNITS AND SPECIALIZED INSTRUCTIONS THAT WILL BE OPTIMIZED FOR SOFTWARE DEFINED RADIO APPLICATIONS. THE RADIATION-HARDENING WILL BE DONE AT THE MICROARCHITECTURAL LEVEL WITH A MECHANISM THAT WILL ALLOW THE DETECTION AND CORRECTION OF ALL TIMING ERRORS---CAUSED NOT ONLY BY RADIATION, BUT ALSO BY VARIATIONS IN THE VOLTAGE, FREQUENCY, MANUFACTURING PROCESS, AND AGING OF THE CHIP. THE BINARY-CODE COMPATIBILITY OF THE RESULTING VLIW PROCESSORS WITH THE POWERPC 750 ISA WILL ALLOW THEM TO SEAMLESSLY EXECUTE LEGACY BINARY CODE FROM PREVIOUS SPACE MISSIONS. WE HAVE MADE CRITICAL CONTRIBUTIONS TO THE FIELDS OF FORMAL VERIFICATION OF COMPLEX PIPELINED MICROPROCESSORS, AND BOOLEAN SATISFIABILITY (SAT), AND HAVE DEVELOPED HIGHLY EFFICIENT ELECTRONIC DESIGN AUTOMATION (EDA) TOOLS THAT WE WILL USE.