Logic synthesis of concurrent control specifications

The number of transistors per chip increases by 58% per year. At the same time, the designer productivity increases by 21% per year. Thus, an increasing number of design and verification engineers is required to tape-out a chip in the same amount of time. In order to close the design productivity gap the abstraction layer should be raised to boost the design productivity more than the above percentage. For instance, the productivity was increased by 10x in 80s when the state of the art design practice changed from stick diagrams to gate level design. Later on, during the 90s, the productivity increased further by 10x by moving to the RTL level design. Behavioral modeling, lately extended the productivity further by 5x. In behavioral modeling, the control is decoupled from the datapath. It is separately described by HDL structures which correspond to monolithic FSMs, increasing thus the abstraction layer from RTL to FSMs. The underlying EDA tools extract, synthesize and verify monolithic FSMs with algorithms performing at this higher level of abstraction. For instance, state minimization which was originally handled by the engineers themselves, is automatically performed by the EDA tools increasing the quality of results, the design time and the verifiability. Although a monolithic FSM is an adequately powerful formalism to describe sequential circuits, it fails to model concurrency without state explosion. Interacting FSM models have so far lacked the formal rigor for expressing the synchronizing interactions between different FSMs. The event based, PTnet model is able to model both concurrency and choice within the same model, however lacks a polynomial time flow to implementation, as current methods of exposing the event state space require a potentially exponential number of states. In this work, a novel formalism for interacting FSMs is introduced i.e Multiple, Synchronized FSMs (MSFSMs), a compact Interacting FSMs model, potentially implementable using any existing monolithic FSM implementation method. MSFSMs efficiently describe concurrent control systems whilst also acting as an intermediate representation for synthesizing existing specifications described as PTNets with FSMbased flows or for verifying concurrency related properties for systems described as a FSMs with PTNet-based algorithms. PTNet to MSFSMs and MSFSMs to interacting FSMs transformation algorithms are proved in this work to be tractable. Thus, efficient PTNet synthesis and interacting FSMs verification flows are introduced which exploit MSFSMs and which do not exhibit state explosion. Furthermore, novel efficient algorithms introduced at the MSFSM level optimize the control specifications by exploiting the inter-FSM communication. Experimental results indicate that PTNets can indeed be transformed to synthesizable FSMs through transformation to MSFSMs without exhibiting state explosion. A large set of concurrent specifications was transformed to MSFSMs in less than one second each, whereas tools generating the full state space needed days of execution time just to generate specification’s state graph. The logic synthesis framework developed in this work, Expose, approaches the quality of results of logic synthesis tools which generate the exponentially large state space of the specifications, whilst approaching the execution time of the direct-mapping methodologies. Concurrent specifications which could only be implemented through direct mapping, as the execution time for full state space exploration is prohibitive, can now be synthesized using Expose. Our results also show that the MSFSM-based heuristic optimization algorithms drastically and predictably improve the implementation metrics of area and performance as they benefit from the confluence between MSFSMs and state space. By assembling a synthesis flow out of heuristic optimizations, an overall area and performance gain of 80% and 35% respectively was obtained.