Formally analyzed dynamic synthesis of hardware

Dynamic hardware reconfiguration based on run-time system specialization is viable with FPGAs. The research challenge for formal verification is to help ensure the correctness of dynamically generated hardware. In this paper, the approach is to verify a specialization synthesis algorithm used to reconfigure FPGA designs at run-time. The verification approach is based on a deep embedding of a language for netlist and the relational hardware modeling style