1. A method for designing high-assurance microcode, the method comprising the steps: receiving a plurality of requirements detailing intended behavior of a circuit; creating a model of microcode behavior; generating microcode based on the model; generating test cases based on the model; simulating the behavior of the microcode; translating the model into a synchronous program; translating the synchronous program into a verification tool-specific format; and formally verifying the model using a verification tool.