SEQUENTIAL CIRCUIT AND FORMING METHOD THEREOF, CONTROLLER AND FINITE-STATE MACHINE

摘要

PURPOSE: To simulate all possible states (i.e., all possible combinations of pointers, buffers, etc.) of a model in a short time. CONSTITUTION: Conversion from a high level to a low level is constituted in the form of formal top-down development procedure based upon successive improvement. Staring with the high level (abstract) such as the formal abstraction, etc., of a standard protocol, successive improvement is done to generate a detailed model. The said improvement is performed so as to guarantee the establishment of properties, confirmed at a certain level of the abstraction, at all subsequent abstraction levels. The successive improvement ends at a low-level 'model' forming the final implementation of the protocol. On the basis of formal verification, implementation by the finite state machine of a control-oriented system is automatically performed in a short time.