Proof-Carrying Hardware Intellectual Property (PCHIP): Framework Automation and Enhancement

Proof carrying hardware intellectual property (PCHIP) introduces a framework in which a hardware intellectual property (IP) is accompanied by formal proofs of certain security-related properties, ensuring that the acquired IP is trustworthy. PCHIP framework adds extra burdensome tasks in the hardware IP development process, hindering its wide acceptance by the hardware design community. This work presents efforts toward automating parts of the PCHIP framework, in order to simplify the adoption of PCHIP by hardware designers, IP developers, and IP consumers and, thereby, increasing trust in hardware designs and hardware IP acquisition. It also demonstrates efforts in enhancing the PCHIP framework with more capabilities, including hierarchical proof development, hybrid module libraries which contain proved lemmas, in addition to the hardware module delivered as code in a hardware description language (HDL), and information flow tracking (IFT) in analog, digital and mixed-signal designs.