Quantum computing, once just a theoretical field, is quickly advancing as physical quantum technology increases in size, capability, and reliability. In order to fully harness the power of a general quantum computer or an application-specific device, compilers and tools must be developed that optimize specifications and map them to a realization on a specific architecture. In this talk, a technique and prototype tool for synthesizing algorithms into a quantum computer is described. A unique aspect of this tool is its incorporation of internal formal equivalence checking that ensures the initially specified algorithm is functionally equivalent to the optimized, technologically-mapped output.