The promise of formal methods to eliminate design errors in safety critical systems is realizable, however, much of the technology remains academic or removed from current engineering practice. At Derivation Systems, Inc. we believe that in over for formal methods to reach their full potential, a formal design tool must support the generative and deductive aspects of design. We also believe that for a formal design tool to be practical, it must integrate with existing logic synthesis tools to generate hardware realizations. We propose the development of DRS (Derivational Reasoning System), a design tool which reflects a formal approach to digital design founded in derivational reasoning. The significance of the innovation is the development of a design tool which integrates derivation with existing verification and logic synthesis tools in a unified framework. This will allow designers to construct correct hardware from high level abstract specifications.In terms of NASA's objectives, we believe our methodology would be naturally applied to key components of fault tolerant architectures. We see our methods as being applied to such architectures as the RCP(Reliable Computing Platform) and FTPP components. We see the greatest commercial potential for DRS in the low-volume ASIC design market. Our system will increase reliability and shorten the design cycle for these high cost devices. These devices range from simple controllers to key components of fault-tolerant architectures.Derivation, Verification, Hardware Synthesis, FM9001
