The first year was dominated by case studies in description and modeling as well as in verification and deductive design, building on and extending the partners' previous work, mainly concentrating on aspects in the small (see §2.3.2 for details).
Concerning NGHDL, we came up with a list of desirable language concepts and explored the possibilities of representing them within the generic theorem prover Isabelle; moreover, the selection of the language concepts was based on their suitability for the methodology of deductive design as employed in various case studies.
On the side of foundations, a central theme was the use of streams based on various formal definitions of that concept. Moreover, there were investigations on: modeling Synchronous Concurrent Algorithms (SCAs) using process algebra; effective algebras; models of time; tool-independent representation of algorithms and hardware; a framework for hardware-software codesign; and technology independent specifications.
These issues will be pursued in detail in smaller workshops during the second year (see again §2.3.2). These workshops are meant for extracting the common concepts and integrating them into a first version of the proposed language, concentrating on aspects in the small. At the same time, further case studies concerning aspects in the large will be conducted to prepare the next phase.