Verifying firmware binary images using a hardware design and formal assertions

A system configured to detect illegal instructions in a firmware binary image using a hardware design for an electronic device configured to execute the firmware binary image, detect illegal firmware instructions in the firmware binary image, and stop execution of the firmware binary image upon detection of an illegal firmware instruction, the system comprising:

• a memory configured to store:
• a hardware monitor comprising assertion evaluation logic configured to determine whether the firmware binary image comprises an illegal firmware instruction by evaluating one or more formal assertions that assert a formal property that states that if an instantiation of the hardware design has stopped execution of the firmware binary image, that the instantiation of the hardware design has or has not detected an illegal firmware instruction in the firmware binary image;
• and
• one or more processors configured to:
• formally verify, using a formal verification tool, that the one or more formal assertions are true for the hardware design loaded with the firmware binary image, and
• output one or more signals indicating whether or not each of the one or more formal assertions was successfully verified to identify whether the firmware binary image comprises an illegal firmware instruction.