Translating formal specifications into behavioural hardware descriptions

Drögehorn, Olaf

kassel university press, ISBN: 978-3-89958-100-3, 2004, 172 Pages

URN: urn:nbn:de:0002-1003

Zugl.: Kassel, Univ., Diss. 2004

| Price and available forms -->

Content: The technical development in digital circuits is going on quite fast and the complexity of modern systems is growing rapidly. Due to this growth of complexity the time of development is increasing, too. In the last years this was proportional to the amount of transistors used in the digital designs. By doubling the number of transistors the time of development was doubled, too. To ensure that the designed circuits will not have any bugs the manufactures carry out a lot of tests. But with the growth of complexity the test routines become very complicated and can not provide 100 percent coverage of the designed circuits. So the term “verification” is used almost always for a test cycle which covers the typical behaviour in an environment, the circuit was designed for.

To overcome this drawback a specification method for systems on a high level of abstraction is used in this thesis. This specification is independent from the desired implementation method but is powerful enough to specify all necessary constraints of the system. The methodology is based on a formal language and uses first order logic to prove that the specified system fulfils the required constraints. This thesis introduces a method with which this specification can be compiled into a hardware description language. It is done by adding several detailed information in order to implement the specification in the right way with the used hardware description language.

In order to keep correctness, it is shown, which steps are necessary to ensure that the implementation still fulfils the constraints of the specified system. Due to the refinements, made during the translation process, it is important to use special style conventions to ensure the correctness of the implementation. Furthermore it is obvious that a straight forward implementation of a formal specification can not be very efficient. The code needs to be optimized in several ways. But each optimization leads to differences between the specification and the produced realization. Therefore several optimizations have been described in this thesis, which have no drawbacks concerning the correctness of the system and still lead to an implementation compliant to the specification. In some cases additional proofs are necessary to ensure the correctness of the steps based on well known proving techniques, which are easy to use.

Last but not least a new design flow for complex systems is suggested. Starting on a very high level of abstraction, the system with its requirements can be specified formally. After several refinements and optimizations a behavioural hardware description will be derived. This description is well suited to be processed with tools used in the industry for simulations and analysis. Based on this analysis the right way for synthesis can be chosen and worked out. With common available synthesis tools the behavioural description can be used to produce a piece of silicon.

Publication is available in following forms:

Full text (pdf-file, not printable - 1.49 MB)
view PDF
Full text (pdf-file, printable, with costs - 1.49 MB) 10.00 Euro
(free of charge in kassel University network - you are in kassel University network if you are in the workplace, or you are using a pc in the ITS or in the library)
download PDF - Attention! with costs, because you are not in kassel University network!