Empowering the Experts : High-Assurance , High-Performance , High-Level Design with Cryptol

You are a highly skilled cryptographer charged with designing a custom, state-of-the-art encryption solution for protecting mission-critical information. There are explicit and competing requirements for the implementation— throughput, size, power utilization, operation temperature, etc.—that may affect the implementation. You produce a design and want to see how it matches up with the implementation requirements. How would you proceed? Typically, you find an expert hardware designer who translates your algorithm into VHDL (a hardware description language), and then runs proprietary tools to characterize the implementation. If it uses too much power, or has insufficient throughput, or..., the hardware designer iteratively tweaks the design until it is “good enough.” But how do you know if it still works the way you intended? Typically, the design is fabricated (if it is an ASIC—application-specific integrated circuit) or loaded into an FPGA (field-programmable gate array), placed into a test harness, and blasted with test vectors. If it works, great. Otherwise, the search begins to find the error.