—We introduce a novel hardware intellectual property acquisition protocol, show how it can support the transfer of provably trustworthy modules between hardware IP producers and consumers, and discuss what it might mean for a device to be considered “secure.” Specifically, we demonstrate the applicability of previous work in the software field of ProofCarrying Code (PCC) to the problem of hardware trust and use it to combat the threat of hardware IP-level Trojans. We outline a semantic model representing the constructs permissible in a Verilog hardware description language (HDL) and show how this model can be used to reason about the trustworthiness of circuits represented at the register-transfer level (RTL). A discussion of “security-related properties” reveals how rules for trustworthy operation might be established for a particular design without necessarily specifying exact functionality. We then examine a hypothetical scenario involving a consumer with certain securit...