1. A method for establishing trust between a management processor and a management server comprising:
establishing trust between a scanning device and the management server by scanning a server code on the management server;
establishing trust between the scanning device and the management processor by scanning a processor code on the management;
creating a secure channel between the management server and the management processor through the scanning device; and
establishing trust between the management server and the management processor through the secure channel.
2. The method of claim 1, wherein establishing trust between the scanning device and the management server by scanning the server code includes the scanning device scanning the server code.
3. The method of claim 1, wherein establishing trust between the scanning device and the management processor by scanning the processor code includes the scanning device scanning the processor code.
4. The method of claim 1, wherein scanning the server code includes scanning a set of login data and a network address that correspond to the management server and the processor code includes a set of login data that corresponds to the management processor.
5. The method of claim 1, wherein establishing trust between the management server and the management processor through the secure channel includes the management server transmitting the processor code to the management processor and the management processor transmitting the server code to the management server.
6. A non-transitory computer-readable medium storing instructions for establishing trust between a management processor and a management server executable by a computer to cause the computer to:
receive a scanned server code that corresponds to the management server with a scanning device to establish trust between the scanning device and the management server;
receive a scanned processor code that corresponds to the management processor with the scanning device to obtain a set of processor login data of the management processor; and
send the set of processor login data to the management server to allow the management server to login to the management processor.
7. The medium of claim 6, wherein the server code includes a server universally unique identifier (UUID), a server security token, and a server network address that correspond to the server code.
8. The medium of claim 7, wherein establishing trust between the scanning device and the management server includes:
using the server UUID and the server network address to identify the management server and to establish a connection to the management server; and
using the server security token to establish trust with the management server.
9. A system for establishing trust between a management processor and a management server, comprising:
a server code that provides a set of server login data wherein the server code corresponds to the management server;
a processor code that provides a set of processor login data wherein the processor code corresponds to the management processor;
wherein the management processor receives the set of server login data and logs into the management server with the set of server login data; and
wherein the management server receives the set of processor login data and logs into the management processor with the set of processor login data.
10. The system of claim 9, wherein the management processor receives the set of server login data through a secured wireless connection and the management server receives the set of processor login data through the secured wireless connection.
11. The system of claim 9, wherein:
the server code is presented by the management server through a monitor that is connected to the management server upon a request by a scanning device; and
the processor code is provided on a processor housing that houses the management processor and is generated during a manufacturing process.
12. The system of claim 11, wherein the management server incorporates a server universally unique identifier (UUID), a server security token, and a server network address into the server code and display the server code on a monitor for the scanning device to scan.
13. The system of claim 11, wherein the processor code includes a unique processor UUID that identifies a management processor and a unique processor security token.
14. The system of claim 9, wherein the server code includes a server quick response (QR) code and the processor code includes a processor QR code.
15. The medium of claim 9, wherein the server code includes a server universal product code (UPC) and the processor code includes a processor UPC.
The claims below are in addition to those above.
All refrences to claim(s) which appear below refer to the numbering after this setence.
1. A method for verifying a design of a circuit, comprising:
selecting a first portion of a model of the design, wherein the first portion has a plurality of first inputs and outputs;
providing a property for the design, wherein the property defines a predetermined behavior of one or more of the first outputs;
determining whether a first stimulus exists that, when applied to the first inputs, can produce a behavior other than the predetermined behavior at the one or more first outputs;
when the stimulus exists, determining whether the model can produce the first stimulus at the first inputs; and
when the stimulus cannot be produced by the model at the inputs, preserving a first description of the first stimulus for analysis.
2. The method of claim 1, further comprising:
outputting the description.
3. The method of claim 1, further comprising:
generating a counterexample describing states of the first portion and a further portion of the model for one or more cycles.
4. The method of claim 3, further comprising:
outputting the counterexample.
5. The method of claim 1, further comprising:
selecting a second portion of the model, wherein the second portion has a plurality of second inputs and outputs, and wherein at least one of the second outputs is provided to at least one of the first inputs;
determining whether a second stimulus exists that, when applied to the inputs of, can produce a behavior other than the predetermined behavior at the one or more outputs of the first portion;
when the second stimulus exists, determining whether the model can produce the second stimulus at the second inputs; and
when the second stimulus cannot be produced by the model at the second inputs of the second portion, preserving a second description of the second stimulus for analysis.
6. The method of claim 5, further comprising:
outputting the second description.
7. The method of claim 5, further comprising:
generating a counterexample describing states of the first portion and the second portion for one or more cycles.
8. The method of claim 7, further comprising:
outputting the counterexample.
9. The method of claim 1, further comprising:
providing the model.
10. The method of claim 1, further comprising:
asserting that the first portion contains a fault when no stimulus exists that, when applied to the first inputs, can produce a behavior other than the predetermined behavior at the one or more outputs.
11. The method of claim 1, wherein:
the first portion is selected based on the property for the design.
12. A semiconductor verified by the method of claim 1.
13. A computer program stored on a tangible computer medium embodying instructions executable by a computer for verifying a design of a circuit, the computer program comprising:
selecting a first portion of a model of the design, wherein the first portion has a plurality of first inputs and outputs;
providing a property for the design, wherein the property defines a predetermined behavior of one or more of the first outputs;
determining whether a first stimulus exists that, when applied to the first inputs, can produce a behavior other than the predetermined behavior at the one or more first outputs;
when the first stimulus exists, determining whether the model can produce the first stimulus at the first inputs; and
when the stimulus cannot be produced by the model at the first inputs, preserving a first description of the first stimulus for analysis.
14. The computer program of claim 13, further comprising:
generating a counterexample describing states of the first portion and a second portion of the model for one or more cycles.
15. The computer program of claim 13, further comprising:
selecting a second portion of the model, wherein the second portion has a plurality of second inputs and outputs, and wherein at least one of the second outputs is provided to at least one of the first inputs;
determining whether a second stimulus exists that, when applied to the second inputs, can produce a behavior other than the predetermined behavior at the one or more first outputs;
when the second stimulus exists, determining whether the model can produce the second stimulus at the second inputs; and
when the second stimulus cannot be produced by the model at the second inputs, preserving a description of the second stimulus for analysis.
16. The computer program of claim 15, further comprising:
generating a counterexample describing states of the first portion and the second portion for one or more cycles.
17. The computer program of claim 13, further comprising:
providing the model.
18. The computer program of claim 13, further comprising:
asserting that the first portion contains a fault when no stimulus exists that, when applied to the first inputs, can produce a behavior other than the predetermined behavior at the one or more first outputs.
19. The computer program of claim 13, wherein:
the first portion is selected based on the property for the design.
20. A semiconductor verified by the computer program of claim 13.
21. A method for verifying a design of a circuit, comprising:
selecting a portion of a model of the design, wherein the portion has a plurality of inputs and outputs;
providing a property for the design, wherein the property defines a predetermined behavior of one or more of the outputs;
determining whether a stimulus exists that, when applied to the inputs, can produce a behavior other than the predetermined behavior at the one or more outputs;
determining whether the model can produce the stimulus at the inputs based on said stimulus existence determination; and
preserving a description of the stimulus for analysis when the stimulus cannot be produced by the model.