Paper: Categories, allegories and circuit design (at LICS 1994)

Authors: Carolyn Brown Graham Hutton

Abstract

Relational languages such as RUBY are used to derive hardware circuits from abstract specifications of their behaviour. Much reasoning is done informally in RUBY using pictorial representations of relational terms. We formalise this use of pictures in circuit design. We show that pictures naturally form a unitary pretabular allegory. Homomorphisms of pictures correspond to adding new wires or circuit comments. Two pictures are mutually homomorphic if and only if they represent equal allegorical terms. We prove soundness and completeness results which guarantee that deriving circuits using pictures does not lead to errors. We illustrate the use of pictures by deriving the ripple adder implementation from a high level, behavioural specification

BibTeX

  @InProceedings{BrownHutton-Categoriesallegorie,
    author = 	 {Carolyn Brown and Graham Hutton},
    title = 	 {Categories, allegories and circuit design},
    booktitle =  {Proceedings of the Ninth Annual IEEE Symposium on Logic in Computer Science (LICS 1994)},
    year =	 {1994},
    month =	 {July}, 
    pages =      {372--381},
    location =   {Paris, France}, 
    publisher =	 {IEEE Computer Society Press}
  }