The demonstrator consists of a video stream processing pipeline in reconfigurable hardware, which is based on a single, Linux-based reconfigurable system-on-chip. Video frames are grabbed from an attached USB webcam, sent from the Linux in the processing system (PS) to the programmable logic (PL) and then passed through an image processing pipeline which, at the end, displays the final frames on an attached HDMI display. Within the pipeline is a pixelstream monitoring and enforcement unit, which is capable of checking pre-defined properties of individual pixels or a group of them, and then enforcing their conformance to said property. In the demonstrator, the enforcement unit works by setting conflicting pixels to a safe state (i.e., to black), and the monitor itself can be synthesized on-the-fly from a user-defined formula given in the Property Specification Language (PSL). For the combination of this monitoring and enforcement unit, a proof by induction will also be generated on-the-fly, proving that the final bitstream actually contains an implementation that indeed is true to the PSL specification and generates a pixelstream which is guaranteed to never contain any illegal pixels. Since we cannot interpret the bitstreams of current FPGAs, since their vendors do not disclose the format, we employ a virtual FPGA overlay with an open bitstream format, so that we can easily obtain the netlist from a bitstream.
To this end, we have generated two interwoven flows, one for the Consumer and one for the Producer, which in combination show the feasibility and flexibility of this powerful PCH certified runtime-monitoring technique. Within the OTF context, PCH can be applied at several places, to ease the following descriptions we will use the interaction between a OTF provider, who combines single services into a larger service to fulfill a user request, and an OTF service provider, who provides one of the single services, as example.