Automatic pipeline synthesis and formal verification from transactional datapath specifications

Pipelining a datapath by hand is tedious and error prone, as it requires a designer to reason about overlapped concurrent execution of sequentially dependent operations in different pipeline stages. Nevertheless, doing so is often necessary to meet performance targets and improve efficiency. Automation techniques have been proposed to reduce the manual effort in designing, implementing, and verifying pipelines. Nevertheless, they are limited in the extent and form of automation that they can do, and the type and size of designs that they can handle.;This thesis presents the transactional datapath specification (T-spec) and the technology (T-piper) to automatically synthesize and formally verify in-order pipeline implementations from it. T-spec elevates design abstraction by allowing a designer to reason about a sequential system at the transactional level, where state transformations happen in a single step, thereby relieving designer's burden to resolve subtle corner cases from concurrent execution due to pipelining. Unlike previous works, the proposed approach can automatically identity and place forwarding paths, support general value speculation (i.e., on any state, with custom predictors), and automatically perform scalable verification using compositional model checking. Further, it improves upon existing processor-specific works since it can handle any sequential designs. Finally, it is extendable to do multi-treaded pipeline synthesis, a novel capability not achievable by any previous work. The technology has been made available online at www.t-piper.net, and its effectiveness has been demonstrated by various design case studies.