This thesis presents a formal verification procedure to check correctness of the synchronous elastic pipelined system that incorporates early evaluation against its synchronous parent system. Note that the goal of the ...