Loading...
Please wait, while we are loading the content...
Similar Documents
Applicability of formal synthesis illustrated via scheduling
| Content Provider | Semantic Scholar |
|---|---|
| Author | Blumenröhr, Christian Eisenbiegler, Dirk Kumar, Ramayya |
| Copyright Year | 1996 |
| Abstract | This paper describes a novel technique for formal synthesis and exempli es the main ideas using the high level synthesis task scheduling The novelty of the approach is based on the fact that arbitrary scheduling algorithms can be embedded within a formal framework to automatically achieve guaranteed correct implementations Two realistic examples are used to emphasize its applicability and it can be seen that the additional costs for formal synthesis are almost negligible in practice We achieve the same quality for the implementations as conventional synthesis plus the proof of their correctness Introduction Although high level synthesis is based on a sequence of algorithms which conform to the correctness by construction paradigm its implementation may be error prone This is due to the complexity of the programs which implement these algorithms One approach towards proving the correctness of implementations is by post synthesis veri cation An excellent overview of veri cation techniques is given in Gupt Melh One of the important correctness criterions is to show that the implementation implies the speci cation Two of the most important reasons for the complexity of these proofs are the existence of the major gap between the abstraction levels of the speci cation and the implementation and the obliviousness of the information used in re ning a speci cation into an implemen tation Therefore full automation can only be achieved for comparatively small sized circuits at lower levels of abstraction For large sized circuits hardware veri cation specialists are mandatory They have to either provide appropriate structuring and abstraction of the proofs while using automatable logics or perform logical interactions with the underlying theorem prover while using complex logics Formal synthesis is a complementary approach to hardware veri cation since formal aver ment is an integral part of the synthesis process However it is a specialized technique which is only tailored towards the proof of synthesized implementations Veri cation is neverthe less needed for validating speci cations which can be achieved by checking properties such as safety and liveness We are developing a formal synthesis toolbox called HASH Higher order logic Applied to Synthesis of Hardware which is applicable to di erent abstraction levels It contains one universal transformation per synthesis step e g scheduling allocation retiming state minimization etc Each transformation is guided by the results of corresponding standard synthesis algorithms that abound in literature TLWN GDWL Hence no new synthesis This work has been partly nanced by the Deutsche Forschungsgemeinschaft Project SCHM The programs implementing the synthesis algorithms are mostly imperative in nature and the correctness of large imperative programs is nearly impossible to prove algorithms either formal or informal are proposed rather a general scheme for logically embedding various existing synthesis algorithms within a formal set up is presented EiKu b In contrast to conventional synthesis approaches only correct hardware implementations can be produced or no implementation is derived when the results of the synthesis algorithms are faulty The quality with respect to costs of the fully automatically generated implementations is dictated only by the conventional synthesis algorithms The implementations therefore have a higher quality than those of conventional synthesis from an overall perspective since they are proven to be correct This concept will be elaborated with respect to the scheduling task in the sections to follow There are also other approaches in the formal synthesis domain An overview is given in KBES But all other techniques do not exploit the results of the sophisticated algorithms which abound in synthesis FoMa HaLD JoBB ShRa Therefore the quality of their implementations is normally worse than that of conventional synthesis algorithms In contrast to HASH which supports fully automated synthesis all other approaches need interaction either at the schematic level or from a logician s point of view The major contributions of this paper are two fold formal synthesis within HASH is applicable to realistic circuits and the additional costs for formal synthesis are reasonable The above mentioned contributions are exempli ed via the scheduling task in high level syn thesis The outline of this paper is as follows in the next section we brie y introduce our approach and de ne the notations and scope of our work In section we will show the results with two realistic examples and section concludes the paper Our Formal Synthesis Approach towards Scheduling In this paper we concentrate on the transformation in HASH for performing the scheduling task within high level synthesis High level synthesis converts an algorithmic description of the circuit into a structure at the Register Transfer RT level The major steps in high level synthesis are scheduling allocation of storage functional and interconnection units binding the allocated hardware onto some library components and interface synthesis The scheduling task assigns a control step c step to each operation in the algorith mic speci cation There exist various heuristic algorithms for solving this task CaWo GDWL A large number of them start from data ow graphs that correspond to the ba sic blocks in the algorithmic description Although certain scheduling algorithms start from control data ow graphs we shall restrict ourselves to pure data ow graphs in this paper The underlying idea behind the scheduling transformation in HASH is illustrated in gure Given a data ow graph some scheduling heuristic is started This heuristic step has nothing to do with logic The heuristic returns a scheduling table which maps each opera tion in the data ow graph onto a c step This scheduling table is now used by the formal logical transformation in HASH to produce a scheduled data ow graph The split between design space exploration i e di erent schedule tables for di erent heuristics and the logical transformation is the core idea in HASH This core idea is applicable to most of the synthesis steps e g allocation no of resources available retiming split in the combinational logic etc schedule table scheduling heuristic (ASAP, ALAP, force-directed, ...) scheduled data flow graph and theorem transformation scheduling data flow graph Figure The concept of HASH as applied to scheduling All the logical transformations in HASH have been implemented within the HOL theorem prover GoMe Each transformation takes the current design state and the result of some synthesis heuristic and returns the new design state along with the correctness theorem stating that the old design state is equivalent to or implied by the new design state Returning to the scheduling task the formalization of the current design state i e the data ow graph is achieved by using expressions Davi The data ow graphs are represented as follows x xm let houtvars i op hinvars i in let houtvars i op hinvars i in let houtvarsli oplhinvarsli in y yn The above structure describes the input output function in terms of the basic operations in the data ow graph x x xm are the inputs y y yn the outputs and op op opl the operations of the data ow graph Each let term describes the connectivity of one operation For all i hinvarsii and houtvarsii denote the inputs and outputs of operation opi respectively The inputs and outputs of operations are tuples with each operation having the speci c arity of its input and output tuple This formal representation is however not unique since the ordering of the operations is ambiguous Nevertheless the data dependencies between the operations must be respected The scheduling transformation in HASH takes the formalized data ow graph g and the schedule table and produces g which is a composition of functions g g gk such that g gk g g and k is the number of c steps Each gi i k represents a slice in the original data ow graph g and corresponds to those operations that are executed in the i c step Additionally the transformation produces the correctness proof stating the equivalence between g and g If the heuristic produces a false result e g a schedule table where the data dependencies are violated or some operations are unscheduled then the transformation fails and returns some constructive feedback to the user which re ects the cause of the failure In gure a simple example is shown which illustrates the invocation of the schedul ing transformation in HASH In this example a well known heuristic called force directed scheduling has been applied PaKn For better readability the data ow graphs are shown in a schematic manner and not by their formal representation If in this example the heuristic schedules operation before operation an exception will be raised during the transforma tion giving the constructive feedback that g gure cannot be built with this schedule table It is also possible to combine several synthesis steps into one complex step Then the cor responding logical transformations have to be performed one after another The cost for this complex logical transformation is just the sum of the costs of the individual transformations see EiBK for more details about the transformations Experimental Results In this section we demonstrate that our formal synthesis scenario works with realistic ex amples We therefore consider two scalable data ow graphs and compare the runtimes for calculating the schedule using various algorithms with the runtimes for the transformations which produce a correct implementation We cannot compare our work with any other veri cation results since to our knowledge no one has formally veri ed the scheduling task The scheduling algorithms we applied are ASAP As Soon As Possible ALAP As Late As Possible list scheduling and two versions of force directed scheduling without with look ahead ASAP ALAP and the two versions of force directed schedul |
| File Format | PDF HTM / HTML |
| Alternate Webpage(s) | http://goethe.ira.uka.de/fsynth/publications/postscript/BlEK96.ps |
| Alternate Webpage(s) | https://publikationen.bibliothek.kit.edu/339596/772111 |
| Language | English |
| Access Restriction | Open |
| Content Type | Text |
| Resource Type | Article |
