Analytical development and verification of control-intensive systems
First Claim
1. In a computer, a method for creating a sequential circuit comprising the steps of:
- receiving a specification and tasks for said sequential circuit;
testing whether said tasks are performable in said sequential circuit when said circuit conforms to said specification;
forming a refined specification by adding detailed information about said specification and defining new tasks to be performed;
formally verifying that said refined specification preserves behavior of said given specification, in that the response of said circuit to input signals when it conforms to said refined specification is consonant with the response of said circuit to the same input signals when it conforms to said given specification;
replacing said tasks with said new tasks and said specification with said refined specification, and returning to said step of testing; and
developing and delivering structure information based on said specification, for effectuating said sequential circuit.
8 Assignments
0 Petitions
Accused Products
Abstract
Designs are created through a high-level to low-level transformation in the form of a formal top-down development procedure based upon successive refinement. Starting with a high-level (abstract) model, such as a formal abstraction of a protocol standard, successively more detailed models are created through successive refinement, in a fashion which guarantees that properties verified at one level of abstraction hold in all successive levels of abstraction. The successive refinements end with a low-level "model" which forms the ultimate implementation of the protocol. In one embodiment of this invention, the analysis/development apparatus creates a unique C language code representation of the specified system that is guaranteed to carry out the tasks specified when executed in a stored program controlled machine. In another embodiment, the code is used to create a "net list" for manufacturing the specified system.
-
Citations
29 Claims
-
1. In a computer, a method for creating a sequential circuit comprising the steps of:
-
receiving a specification and tasks for said sequential circuit; testing whether said tasks are performable in said sequential circuit when said circuit conforms to said specification; forming a refined specification by adding detailed information about said specification and defining new tasks to be performed; formally verifying that said refined specification preserves behavior of said given specification, in that the response of said circuit to input signals when it conforms to said refined specification is consonant with the response of said circuit to the same input signals when it conforms to said given specification; replacing said tasks with said new tasks and said specification with said refined specification, and returning to said step of testing; and developing and delivering structure information based on said specification, for effectuating said sequential circuit. - View Dependent Claims (2)
-
-
3. In a computer a method for creating a sequential circuit that performs given tasks, comprising the steps of:
-
entering into an analyzer a specification of said sequential circuit; forming a refined specification by adding to said analyzer detailed information absent in said specification; formally verifying that said refined specification preserves behavior of said specification, in that the response of said circuit to input signals when it conforms to said refined specification is consonant with the response of said circuit to the same input signals when it conforms to said specification; replacing said specification with said refined specification, and returning to said step of forming; and developing and delivering out of said analyzer structure information based on said specification, for effectuating said sequential circuit. - View Dependent Claims (4, 5, 6, 7, 8)
-
-
9. In a computer, a method for creating a sequential circuit that performs given tasks in accordance with a given specification, comprising the steps of:
-
defining a reduction of said given specification for each of said given tasks to form a reduced specification for each task; testing that each reduced specification subsumes said given specification with respect to said task and leaves its corresponding task invariant; testing each task to determine that it is performable in a circuit that conforms to the reduced specification corresponding to the tested task; developing circuit structure information, based on said given specification, for effectuating said sequential circuit; and
incorporating said structure information in a pattern of connections of an integrated circuit. - View Dependent Claims (10, 11, 12, 13)
-
-
14. In a computer, a method for creating a sequential circuit comprising the steps of:
-
entering into an analyzer a circuit specification and tasks; testing whether said tasks are performable in said sequential circuit when said sequential circuit conforms to said specification; forming a refined specification by adding to said analyzer detailed information about said specification and entering a new tasks to be performed; formally verifying that said refined specification preserves behavior of said specification, in that the response of said circuit to input signals when it conforms to said refined specification is consonant with the response of said circuit to the same input signals when it conforms to said specification; replacing said tasks with said new tasks and said specification with said refined specification, and returning to said step of testing; defining a reduction of said specification for each of said tasks to form a reduced specification for each task; testing the reduced specification to determine that each reduced specification subsumes said specification and leaves its corresponding task invariant; testing each task to determine that it is performable in a circuit that conforms to the reduced specification corresponding to the tested task; and developing and delivering out of said analyzer structure information based on said specification, for effectuating said sequential circuit.
-
-
15. In a computer, a method for creating a sequential machine that conforms to a given specification, which machine performs tasks, comprising the steps of:
-
developing a refinement specification of said sequential circuit to form a refined candidate specification and defining tasks to be performed by said sequential machine; testing the assertion that the refined candidate specification is subsumed by said given specification and that the tasks are performable by said sequential machine when said machine conforms to said refined candidate specification; correcting said refined candidate specification and said tasks when said testing indicates rejection of said assertion; replacing said given specification with said refined candidate specification and returning to said step of developing a refinement when said testing indicates acceptance of said assertion. - View Dependent Claims (16, 17, 18, 19, 20, 21, 22)
-
-
23. A sequential circuit for carrying our given tasks, having a stored program processor and a memory, with a signal set stored in said memory having a portion that is essential for performing said given tasks, and said portion consisting of a plurality of modules, with each module forming a switch construct having references to no modules other than modules that control input and output functions of said stored program processor.
-
24. A controller comprising:
- a processor to form a finite state machine with an input port and an output port and which develops prechosen responses at said output port in consequence of input signals at said input port and the state of said finite state machine, having
an execution program for effecting said prechosen responses, and a memory for storing said execution program, wherein said execution program, in a portion thereof that is essential to effect said chosen responses, includes switch constructs, with branches of all of said switch constructs including commands selected strictly from a set that excludes calls to functions other than functions that interact with said input port and said output port.
- a processor to form a finite state machine with an input port and an output port and which develops prechosen responses at said output port in consequence of input signals at said input port and the state of said finite state machine, having
-
25. Apparatus comprising:
- a finite state machine with an input port and an output port and which develops prechosen responses at said output port in consequence of input signals at said input port and the state of said finite state machine, having
an execution program for effecting said prechosen responses, a memory for storing said execution program, and a processor connected to said memory and to said input port and output port, wherein said execution program, in a portion thereof that is essential to effect said chosen responses, includes switch constructs, with branches of all of said switch constructs including commands selected strictly from a set that excludes calls to functions other than functions that interact with said input port and said output port. - View Dependent Claims (26)
- a finite state machine with an input port and an output port and which develops prechosen responses at said output port in consequence of input signals at said input port and the state of said finite state machine, having
-
27. A sequential machine, formed form a plurality of interacting finite state machines and having an input port and an output port, comprising:
-
an execution program to effect chosen responses of said machine at said output port to input signals at said input port, a memory for storing said execution program, and a processor connected to said memory and to said input port and output port, wherein said execution program includes a switch construct for each of said interacting finite state machines, with branches of all of said switch constructs that are essential to effect said chosen responses including commands selected strictly from a set that excludes calls to functions other than functions that interact with said input ports and said output ports. - View Dependent Claims (28)
-
-
29. A sequential circuit for carrying our given tasks, comprising:
- cooperating modules, where the structure of each of the modules forms a switch construct that is structured in accordance with an iteratively applied method comprising the steps of
developing a circuit specification to form a given specification; testing whether said given tasks are performable in said sequential circuit when said circuit conforms to said given specification, and whether to continue to a step of forming a refined specification; forming a refined specification by adding detailed information about said specification and defining new tasks to be performed; verifying that said refined specification carries out said given tasks with the same responsiveness as those tasks are carried out by said given specification, in that the response of said circuit to input signals, when it conforms to said refined specification, is consonant with the response of said circuit to the same input signals when it conforms to said given specification; replacing said given tasks with said new tasks and said given specification with said refined specification, and returning to said step of testing; and developing said set of modules from said given specification.
- cooperating modules, where the structure of each of the modules forms a switch construct that is structured in accordance with an iteratively applied method comprising the steps of
Specification