Ozbaltan, MeteBerthier, Nicolas2026-03-262026-03-2620212300-26111230-238410.24425/acs.2021.1374262-s2.0-85112581942https://doi.org/10.24425/acs.2021.137426https://hdl.handle.net/20.500.14901/1625Özbaltan, Mete/0000-0002-3215-6363We devise a tool-supported framework for achieving power-efficiency of data-flow hardware circuits. Our approach relies on formal control techniques, where the goal is to compute a strategy that can be used to drive a given model so that it satisfies a set of control objectives. More specifically, we give an algorithm that derives abstract behavioral models directly in a symbolic form from original designs described at Register-transfer Level using a Hardware Description Language, and for formulating suitable scheduling constraints and power-efficiency objectives. We show how a resulting strategy can be translated into a piece of synchronous circuit that, when paired with the original design, ensures the aforementioned objectives. We illustrate and validate our approach experimentally using various hardware designs and objectives.eninfo:eu-repo/semantics/openAccessSymbolic Discrete Controller SynthesisDigital Synchronous CircuitsPower-EfficiencyArticle