| Abstract |
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.
|
Collections
