Entwicklung einer Methodik zur Formalen Synthese

点击翻译按钮获取中文摘要

In den ersten beiden Projektjahren wurde die Grundlage zur logisch fundierten Schaltungssynthese geschaffen. Durch diesen Ansatz ist es erstmals möglich, eine durchgängige, garantiert korrekte Synthese von der Systemebene bis zur Gatterebene durchzuführen. Neben der Korrektheit einer Implementierung spielt deren Qualität eine ebenso entscheidende Rolle für deren Verwertbarkeit. Daher soll die Qualität des Syntheseergebnisses nun in den Vordergrund gerückt werden. Zu diesem Zweck sollen die in konventionellen Algorithmen definierten Verfahren zur optimierenden Synthese in dem erarbeiteten formalen System eingesetzt werden. Ziel ist der Nachweis, daß mit Hilfe der Formalen Synthese qualitativ hochwertige Schaltungen synthetisiert werden können. Im Unterschied zur konventionellen Synthese wird bei der Formalen Synthese allerdings zusätzlich automatisch der Beweis erbracht, daß die synthetisierten Schaltungen bezüglich ihrer Spezifikationen korrekt sind.