Efficient and Correct by Construction Assertion-Based Synthesis

We propose a unifying formalization of the concepts of monitor and reactant, and derive a modular synthesis method to achieve automatic generation of compliant modules from declarative temporal specifications. The founding dependence relation and its hardware interpretation provide an algorithm to automatically decide which signals are observed and which are generated. The method is efficient, and it synthesizes control circuits in a few seconds. The results obtained on classical benchmarks show that our technique compiles properties more efficiently than previous prototype tools.