We present a theory for automata in HOL, which is dedicated towards formal hardware synthesis. The theory contains definitions for formally representing and transforming automata. In this approach hardware is represented by automata descriptions and formM synthesis is performed by applying formally proven theorems. The approach presented is constructive -- i.e. starting from specifications at higher levels of abstractions, synthesis can be performed by repeated applications of these transformations. Specialized refinements and optimizations at the RT and gate levels are discussed.
CITATION STYLE
Eisenbiegler, D., & Kumar, R. (1995). An automata theory dedicated towards formal circuit synthesis. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 971, pp. 154–169). Springer Verlag. https://doi.org/10.1007/3-540-60275-5_63
Mendeley helps you to discover research relevant for your work.