In dieser Arbeit wird ein Verfahren der formal korrekten Synthese vorgestellt, mit Hilfe dessen ein automatisierter Entwurf von Prozessoren mit Pipelining möglich ist. Das Verfahren basiert auf einer kleinen Menge korrektheitserhaltender Transformationen, deren Anwendung effizient durch eine unabhängige Post-Synthese-Verifikation überprüft wird. Zur Spezifikation dient eine im Rahmen dieser Arbeit entwickelte, experimentelle Hardwarebeschreibungssprache LLS (Language of Labelled Segments). Der transformale Ansatz kann neben der Synthese auch zur Verifikation genutzt werden. Ein automatisches Verfahren wird vorgestellt, daß die Äquivalenz eines Entwurfs vor und nach dem Einplanungsschritt der High-Level-Synthese nachweist. Durch Anwenden von Transformationen kann die Äquivalenz zweier Beschreibungen gezeigt werden. Die Äquivalenz ist gegeben, wenn eine Folge korrektheitserhaltender Transformationen existiert, die die eine in die andere Beschreibung umwandelt. Insbesondere Ergebnisse moderner Einplanungsverfahren wie z.B. AFAP und DLS können mit dem vorgestellten Verfahren, das sowohl auf zyklischen Kontrollflußgraphen als auch für Pipeline-Systeme arbeitet, verifiziert werden.