This directory contains files related to studies involving the use of 
formal reasoning systems to verify the  s i n g l e  p u l s e r  circuit.

@README

  Created August 19, 1994.  This file.
  Revised October 21, 1994.  This file.
  Revised September 14, 1995.  This file, subdirectories.
  Revised September 18, 1995.  This file, added Fisler95.ps and
         JohnsonBarwiseAllwein93.ps


TPCD94.ps.Z		(175847)
TPCD94.ps.Z.uu		(243986)

  Created October 19, 1994.
  Revised October 21, 1994.
  Final version of the paper "Studies of the Single Pulser in Various Reasoning
  Systems," by Steven D Johnson, Paul S Miner, and Albert Camilleri,
  to appear in the proceedings of the IFIP WQ 10.2 Conference on Theorem
  Provers in Circuit Design (TPCD 94), at Bad Herranalb (Blackforest),
  Germany, 26-28 September 1994, published by Springer.


TPCD94.apx.ddd.ps.Z     (48078)
TPCD94.apx.ddd.ps.Z.uu  (66278) 

  Created August 19, 1994.
  Appendix to the "Studies of the Single Pulser
  in Various Reasoning Systems," by Steven D Johnson, Paul S Miner,
  and Albert Camilleri, detailing the DDD study.

Fisler95.ps *** (c) Kathryn Fisler assigned to Oxford Press
  Copied here on September 18, 1995

  Kathi Fisler's chapter on diagramatic reasoning, cited in the article
  TPCD94.  This chapter is to appear in a forthcoming book, on Diagrams in
  Logic, edited by G. Allwein and K.J. Barwise, to be published by Oxford
  Press.  Until this book appears, individuals my retrieve copies of
  the article for personal use, but should not distribute copies any further.
   
JohnsonBarwiseAllwein93.ps
  Copied here on September 18, 1995

  "Towards the Rigorous Use of Diagrams in Reasoning about Hardware," in
  G. Allwein and K.J. Barwise (eds.), Working Papers on Diagrams in Logic,
  Indiana University Logic Group Preprint IULG-93-23. Revised collection
  to be published in 1995 by Oxford Press.  This article uses the single
  pulser as its core example.
  
DDD/*

  Data files and listings for the DDD derivation exercise in the
  TPCD94 article, as described in the appendix TPCD.apx.ddd.ps.


HOL/mail

  Collection of communciations to the HOL newsgroup concerning the Singel
  Pulser example.  This data was retrieved from the HOL archive at

       http://lal.cs.byu.edu/cgi-bin/info-hol_search

  with the search string "pulser"


OCT/*

  Data files and listings for the Octtools synthesis exercise in the
  TPCD94 article.


PVS/*

  Data files and listings for the PVS specification and proof done by
  Paul Miner.


SMV

  mail     - correspondence, mostly taken from the HOL newsgroup (see above)
  sp-6.smv - SMV source file verification in TPCD94.


ST/mail

  Subdirectory containing communciations with Technical University of Denmark
  on a study of the Single Pulser using Synchrnized Transitions (ST)