liu.seSearch for publications in DiVA
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • oxford
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
A transformational approach to formal digital system design
Linköping University, Department of Computer and Information Science. Linköping University, The Institute of Technology.
1993 (English)Licentiate thesis, monograph (Other academic)
Abstract [en]

The continuing development in electronic technology has made it possible to fit more and more functionality on a single chip, thus allowing digital systems to become increasingly complex. This has led to a need for better synthesis and verification methods and tools to manage this complexity.

Formal digital system design is one such method. This is the integrated process of proof and design that starting from a formal specification of a digital system, generates a proof of correctness of its implementation as a by-product of the design process. Thus, by using this method, the designer can interactively transform the specification into a design that implements the specification, and at the same time generate a proof of its correctness.

In this thesis we present an approach to formal digital system design that we call transformational. By this we mean that we regard design as an iterative process that progresses stepwise by applying design decisions that transforms the design until a satisfactory design has been reached. To be able to support both synthesis and verification we use a two-level design representation where the first level is a design specification in logic that is used for formal reasoning, and the second level is a set of design annotations that are used to support design analysis and design checking.

We have implemented an experimental design tool based on the HOL (Higher Order Logic) proof system and the window inference package. We demonstrate the usability of our approach with a detailed account of two non trivial examples of digital design derivations made using the implemented tool.

Place, publisher, year, edition, pages
Linköping: Linköping University Electronic Press, 1993. , p. 122
Series
Linköping Studies in Science and Technology. Thesis, ISSN 0280-7971 ; 378
National Category
Human Computer Interaction
Identifiers
URN: urn:nbn:se:liu:diva-163147Local ID: LiU-TEK-LIC-1993:20ISBN: 9178711223 (print)OAI: oai:DiVA.org:liu-163147DiVA, id: diva2:1386087
Available from: 2020-01-16 Created: 2020-01-16 Last updated: 2020-01-24Bibliographically approved

Open Access in DiVA

No full text in DiVA

Authority records

Larsson, Mats

Search in DiVA

By author/editor
Larsson, Mats
By organisation
Department of Computer and Information ScienceThe Institute of Technology
Human Computer Interaction

Search outside of DiVA

GoogleGoogle Scholar

isbn
urn-nbn

Altmetric score

isbn
urn-nbn
Total: 180 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • oxford
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf