< retour aux publications

Efficient and Correct by Construction Assertion-Based Synthesis

Auteur(s) : K. Morin-Allory, N. Javaheri, D. Borrione

Journal : Transactions on Very Large Scale Integration (VLSI) Systems

Volume : 23

Issue : 12

Pages : 2890-290

Doi : 10.1109/TVLSI.2014.2386212

KWe 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.