Paige This research is on testing the feasibility of a transformational methodology, previously used only for software productivity improvement, within the context of hardware specification and synthesis. The research involves the designing and implementing a transformational environment for a hardware specification and synthesis language. This environment supports VHDL-like specifications, symbolic analysis of these specifications, and correctness preserving source-to-source transformations. Two applications are being carried out. The first emphasizes automatic hardware design in which the system is used to transform algorithmic level hardware specifications into register transfer level implementations. The second application deals with hardware verification by automatic linear time model checking using a subset of temporal logic.
