PCH Demonstrator

Overview

The Proof-Carrying Hardware (PCH) Demonstrator is a collection of software tools, scripts and hardware modules that demonstrate the PCH tool flow and show the proof-carrying hardware service exchange between a provider and an OTF service provider.

Features

The demonstrator features two separate flows, one for each involved party.

Provider (PCH consumer)

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:

Related tools

  • VTR (from Verilog-to-Routing) tool flow (ABC, ODIN II, VPR) is used to synthesize the design
  • ZUMA scripts are used to transform the synthesized design into an overlay configuration bitstream
  • ABC is used to form the miter function
  • picoSAT is used to solve the unSAT problem
  • tracecheck is used to validate a previously computed unSAT proof
  • ReconOS is used to run the hardware / software co-design

Contact

If you have any questions regarding the PCH demonstrator, please contact the research staff from Subproject B4.