On the functional verification of dynamic partial reconfiguration

Dynamic Partial Reconfiguration (DPR) on Field Programmable Gate Arrays (FPGAs) allows reconfiguration of some of the logic at runtime while the rest of the logic keeps operating. This feature allows the designers to build complex systems such as Software Defined Radio (SDR) in a reasonable area. However, utilizing DPR needs more verification efforts to ensure the correct operation of the reconfiguration logic and the design functionality. New scenarios should be covered due to the usage of DPR technique such as guaranteeing proper connections for the ports of the Reconfigurable Modules (RMs) which share the same Reconfigurable Region (RR) on the FPGA. This paper proposes a technique to verify the connections of the RMs using Assertion Based Verification (ABV). The proposal is to first model the connections of the RMs using System Verilog Assertions (SVAs), then instrument the design with the generated assertions, and then verify the instrumented design using formal verification methods to prove or disprove the correctness of the connections. The proposed technique is demonstrated on a real design that utilizes DPR technique.