The use of pipelines is an important technique in contemporary hardware design, particularly at the level of register-transfer logic (RTL). Earlier formal analysis using the ACL2 theorem prover showed correctness of pipelined floating-point RTL. This paper extends that work by considering a notion of a conditional pipeline, essentially the result of sharing hardware among several distinct pipelines. We have employed a pipeline tool, written in ACL2 but completely unverified, to find a pipeline-related bug in an industrial hardware design, which has since been corrected. We then enhanced this tool to generate lemmas that we have used to prove properties of the corrected design. This paper presents a theoretical basis for this tool and describes its design and operation at an abstract level, showing how it fits into the correctness proof. This work may be viewed, from a high-level perspective, as encouragement for formal verifiers to prove properties of the actual RTL-level models, rather than stopping with their various abstractions.