A synthesis framework based on trace and automata theory
Jerome Fron, Chih-Yuan Yang, M. Damiani, Givanni De Micheli · 1994
In this paper we present a method for modeling don't cares at high-level in a form that can be used by sequential logic synthesis. Behavior is specified by a set of concurrent, interacting processes. Each process is described formally by its set of execution traces and represented by an /spl omega/-automaton. This type of specification is formally precise and allows the inclusion of don't cares by allowing multiple execution traces for a given input. Moreover, it allows us to cast the synthesis problem into a language containment problem, and to provide a formal description of these don't cares. We have developed a prototype synthesis system based on this framework, targeting the synthesis of the control portion of a circuit. Starting from a hardware description language Hardware, a specification is expressed in terms of a set of interconnected /spl omega/-automata. We demonstrate the feasibility of the approach by showing the possibility of traversing the state space of the specification automata.>