Research On The Formal Design Of Digital Hardware: Theories And Approaches

In the last several decades or so, the fast developing of microelectronic technology and growing requirement from the various kind of sophisticated applications make the modern integrated circuit (IC) more complicated in scale and functionality. These will inevitably lead to the higher demands for designing and manufacturing of IC systems.As far as the state of the art of manufacturing IC systems, the techniques of deep-submicron make it possible to implement functions of signal sampling, converting, storing, manipulating within a single chip which is called Systems-on-Chip (SoC). Hence the so-called "design productivity gap" which our ability to design complex integrated circuits was found to be lagging the technology's capability appears. The most obvious solution for closing this gap is to raise the level of abstraction in design.Do the design methodology and development tools we use today will meet the need of design abstraction after raising the design level? The answer is probably not.On the another hands, because of the increase in complexity of hardware, the subtle errors is much greater. How can we guarantee the correctness of design?One way of achieving these goals is by using formal methods, which are mathematically based languages, techniques, and tools for specifying and verifying such systems. These methods begin with the formal design specifications given by the designer and then derive the top design codes by using refinement calculus laws.This dissertation explores the possibility of formal methodology at the highest level of design of digital hardware or IC and covers several topics such as formal specifications, temporal logic, refinement calculus and formal semantics of HDL (Hardware Description Language). The thesis is organized as follows:(1) Looks back the progress achieved by the formal design of software or hardware, and covers the foundations for formal design, presents a new two-level formal design method.(2) Presents the formal semantics of VHDL in DC (Duration Calculus).(3) Discusses the formal specifications for hardware formal design and presents the formal model of FCMHD (Formal Computational Model for Hardware Design) and its formal semantics based on ITL (Interval Temporal Logic).(4) Presents a new kind of HDL ?CHDL (Core HDL) and gives its semantics in FCMHD.(5) Gives the refinement laws for FCMHD and transformation from CHDL to VHDL or Verilog HDL.(6) Ends up with a large example on the base of the theories and methods discussed in the former chapters.