Refinement-based verification of elastic pipelined systems

A formal verification procedure to check the correctness of synchronous elastic pipelined systems against their synchronous specification systems was developed. The procedure can deal with elastic systems that incorporate early evaluation. Note that the goal of the verification procedure is not to establish the correctness of the algorithm for synthesising elastic circuits, but instead, to find bugs and formally prove the correctness of elasticised designs. Dataflow through elastic architectures is complicated by the insertion of any number of elastic buffers in any place in the design. The authors introduce elastic token-flow diagrams, which are used to track the flow of data in elastic architectures. The authors provide a method to construct such diagrams. The authors also develop a highly automated and systematic procedure based on elastic token-flow diagrams that computes functions that map states of elastic systems to states of the synchronous parent systems. Such functions, known as refinement maps are used to compare behaviours of elastic and synchronous systems and hence prove their equivalence. The effectiveness of our methods is demonstrated by verifying 14 elastic pipelined processor models, eight of which incorporate early evaluation.