A Constructive Approach towards Correctness of Synthesis - Application within Retiming
Dirk Eisenbiegler, Ramayya Kumar, Christian Blumenröhr · 1997
This paper is dedicated to correct synthesis. By correct synthesis we mean, that there is a mathematical proof telling us, that the output circuit description fulfills the input circuit description. There are several ways to achieve correct synthesis. In this paper, we present a novel approach which integrates conventional synthesis algorithms thus guaranteeing the same quality of designs. Our approach is fully automatic, although it is based on rule applications within a theorem prover. We compare our results in the area of retiming to other approaches.