The consumer employs a filtering application (see screenshot), which filters each image in a stream and displays them alongside. The filtering is performed in hardware on an FPGA using exchangeable filter modules implemented in an FPGA overlay.

The consumer can request a new filter module from the OTF service provider at runtime, by sending an exact specification of the filter. This is implemented by sending a Verilog behavioral hardware description file to the OTF service provider, which processes the design using the provider tool flow and sends back a proof-carrying FPGA overlay configuration (bitstream) that implements the new module and proves functional equivalence of the implementation to the original Verilog specification. The consumer checks the proof and then uses the new filter module, if it is trustworthy.

The consumer’s flow thus encompasses:

• Sending Verilog description of new filter module to OTF service provider
• Receiving implemented bitstream and equivalence proof
• Checking if proof premise matches equivalence problem (fail if not)
• Checking if proof indeed proves functional equivalence (fail if not)
• Reconfiguring the filter with the new module

OTF service provider (PCH producer)

The producer receives the Verilog source file from the consumer, along with the task to implement a functionally equivalent FPGA overlay module. The producer employs the well-known VTR (from Verilog-To-Routing) tool flow, together with a specialized tool flow for the overlay, to synthesize the description into an implemented module, i.e., an overlay bitstream. The provider then re-extracts the logic function of that bitstream into a format suitable for logic reasoning, and constructs a proof premise for functional equivalence by forming what is called a miter function of the specification and implementation, yielding an unSAT problem, which can be proved afterwards. The producer sends the resulting proof and the overlay bitstream back to the consumer.

Thus the producer's flow consists of:

• Receiving a Verilog description of a hardware module
• Synthesizing that description into an overlay configuration bitstream
• Formulating the equivalence proof for description and implementation
• Conducting the proof
• Sending proof and bitstream back to the provider

Overall tool flow: