1. An apparatus for automatically updating data broadcasting through a broadcasting terminal reproducing audiovisual (AV) broadcasting and data broadcasting, the apparatus comprising:
a storage unit that stores updated information for the data broadcast, which is predetermined by a user;
a radio frequency (RF) module that separates the data broadcasting predetermined by the user from the broadcasting signals;
a data broadcasting signal decoder that decodes the data broadcasting signal separated by the RF module; and
a controller that uses the update information for the data broadcasting stored in the storage unit to determine if the data broadcasting needs to be updated and that periodically updates the data broadcasting by controlling the data broadcasting signal decoder.
2. The apparatus of claim 1, further comprising an output unit, wherein the data broadcasting signal is downloaded in advance and stored in the storage unit, and thereafter the data broadcasting is output together with the audiovideo (AV) broadcasting through the output unit.
3. The apparatus of claim 2, wherein the output unit outputs an audiovideo (AV) broadcasting signal decoded by an AV broadcasting signal decoder and a data broadcasting signal decoded by the data broadcasting signal decoder.
4. The apparatus of claim 1, wherein the update information for the data broadcasting includes information on a sub channel, an ensemble channel, data content, and an update period.
5. The apparatus of claim 1, further comprising an audiovideo (AV) broadcasting signal decoder that decodes the AV broadcasting signal.
6. A method of automatically updating data broadcasting while audiovideo (AV) broadcasting is being watched through a broadcasting terminal, the method comprising:
comparing a predetermined update period of the data broadcasting with an elapsed time;
processing a predetermined data broadcasting signal if the elapsed time is greater than the update period; and
providing data broadcasting to a user by using the processed data broadcasting signal.
7. The method of claim 6, wherein the processing of the predetermined data broadcasting signal comprises:
filtering and separating only signals of mainsub channels that include a predetermined data broadcasting signal from broadcasting signals;
separating only the predetermined data broadcasting signal from the signals of mainsub channels; and
decoding the separated data broadcasting signal.
8. The method of claim 7, further comprising, if a mainsub channel of audiovideo (AV) broadcasting currently being watched by the user is different from a predetermined mainsub channel, changing the mainsub channel of the AV broadcasting into the predetermined mainsub channel.
9. The method of claim 6, further comprising:
informing the user that an update process for data broadcasting will be performed; and
canceling the update process for data broadcasting if the user indicates a desire not to perform the update process for data broadcasting.
10. The method of claim 6, further comprising:
informing the user that an update process for data broadcasting will be performed; and
delaying the update process for data broadcasting if the user indicates a desire to delay the update process for data broadcasting for a predetermined time.
11. The method of claim 6, further comprising the user predetermining update information for the data broadcasting.
12. The method of claim 6, wherein the data broadcasting signal includes one or more data content comprising traffic condition information, traffic accident information, destination information, weather information, financial information, and sports information.
13. The method of claim 6, wherein, in the providing of the data broadcasting to the user, only the data broadcasting is output.
14. The method of claim 6, wherein, in the providing of the data broadcasting to the user, the data broadcasting is output together with the audiovideo (AV) broadcasting currently being watched.
15. The method of claim 14, further comprising, if a mainsub channel of AV broadcasting currently being watched by a user is different from a predetermined mainsub channel, downloading and storing a broadcasting signal of the predetermined mainsub channel.
16. A method of automatically updating data broadcasting while audiovideo (AV) broadcasting is being watched through a broadcasting terminal, the method comprising:
comparing a predetermined update period of the data broadcasting with an elapsed time;
if the elapsed time is greater than the update period, and if a mainsub channel of AV broadcasting currently being watched by a user is different from a predetermined mainsub channel, changing the mainsub channel of AV broadcasting into the predetermined mainsub channel;
processing a predetermined data broadcasting signal of the predetermined mainsub channel; and
providing the data broadcasting to the user by using the processed data broadcasting signal.
17. A computer-readable medium having embodied thereon a computer program for executing a method of automatically updating data broadcasting while audiovideo (AV) broadcasting is being watched through a broadcasting terminal, the method comprising:
comparing a predetermined update period of the data broadcasting with an elapsed time;
processing a predetermined data broadcasting signal if the elapsed time is greater than the update period; and
providing the data broadcasting to a user by using the processed data broadcasting signal.
18. A method of providing broadcasting signals to the user from a plurality of mainsub channels, using digital multi-broadcasting (DMB), comprising:
displaying audiovideo (AV) broadcasting of a first mainsub channel; and
automatically providing on a periodic basis, data broadcasting of a second mainsub channel.
19. The method of claim 18, wherein the automatically providing of the data broadcasting comprises:
storing the data broadcasting in a storage unit;
matching the data broadcasting stored on the storage unit to a selection by a user, via a user interface; and
displaying on an output unit, the data broadcasting stored in the storage unit that matches the selection.
20. The method of claim 19, wherein the displaying of the data broadcasting comprises:
superimposing the matched data broadcasting on the audiovideo (AV) broadcasting currently being watched by the user.
21. The method of claim 19, further comprising:
replacing the display of the audiovideo (AV) broadcasting with the matched data broadcasting.
22. The method of claim 18, wherein the automatically providing of the data broadcasting comprises:
outputting audio content of the data broadcasting.
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 formally proving the functional equivalence of pipelined designs containing memories, comprising:
receiving a specification for a first pipelined design and a specification for a second pipelined design, wherein the first pipelined design includes a first memory system and the second pipelined design includes a second memory system;
generating, using one or more computers, representations of the first pipelined design and the second pipelined design in a combinational form, wherein the representations are generated based partly or solely on a correspondence between memory operations on the first memory system and corresponding memory operations on the second memory system, and wherein memory operations in the first memory system and the second memory system are converted into corresponding combinational operations based partly or solely on design inputs; and
comparing the combinational outputs of the first pipelined design and the combinational outputs of the second pipelined design to verify that the first pipelined design and the second pipelined design are functionally equivalent.
2. The method of claim 1, wherein the correspondence between operations on the first memory system and corresponding operations on the second memory system simplifies the verification of functional equivalence for the designs.
3. The method of claim 2, wherein in designs with different pipeline depths, write accesses to memories may occur in different cycles; and wherein determining the correspondence between the first memory system and the second memory system involves:
symbolically simulating both pipelined designs for several cycles to discover the relationship between the first memory system and the second memory system;
guessing in which pipeline cycles the contents of the first memory system and the contents of the second memory system match; and
proving by induction that the guess holds for all times.
4. The method of claim 3,
wherein the initial contents of the first memory system and the second memory system are assumed to be substantially the same; and
wherein comparing the outputs further comprises unrolling the pipelines to represent design outputs as combinational blocks comprised of the pipeline stages but without pipeline registers.
5. The method of claim 4,
wherein knowing the initial state of a memory system and unrolling the pipelines allows subsequent read and write accesses fromto the memory system to be represented combinationally; and
wherein determining that the memory systems correspond in certain pipeline cycles allows checking the equivalence of the design outputs using a combinational equivalence check instead of a sequential equivalence check.
6. The method of claim 5, wherein the data outputs from an initial set of pipeline cycles do not comprise meaningful values, and are ignored in the equivalence comparison.
7. The method of claim 1, wherein the method is used to generate a complete proof that verifies that a register-transfer-level description of a design is functionally equivalent to an original high-level description of the design.
8. The method of claim 1, wherein the representation of data in the first memory system is different from the representation of data in the second memory system.
9. The method of claim 1, wherein the first memory system andor the second memory system are comprised of multiple memories.
10. The method of claim 9, further comprising:
receiving a user-generated specification that specifies how the memory system of the first pipelined design and the memory system of the second pipelined design match; and
using the user-generated specification to assist in determining the correspondence between the first memory system and the second memory system.
11. A non-transitory computer-readable storage medium storing instructions that when executed by a computer cause the computer to perform a method for formally proving the functional equivalence of pipelined designs containing memories, the method comprising:
receiving a specification for a first pipelined design and a specification for a second pipelined design, wherein the first pipelined design includes a first memory system and the second pipelined design includes a second memory system;
generating representations of the first pipelined design and the second pipelined design in a combinational form, wherein the representations are generated based partly or solely on a correspondence between memory operations on the first memory system and corresponding memory operations on the second memory system, and wherein memory operations in the first memory system and the second memory system are converted into corresponding combinational operations based partly or solely on design inputs; and
comparing the combinational outputs of the first pipelined design and the combinational outputs of the second pipelined design to verify that the first pipelined design and the second pipelined design are functionally equivalent.
12. The non-transitory computer-readable storage medium of claim 11, wherein the correspondence between operations on the first memory system and corresponding operations on the second memory system simplifies the verification of functional equivalence for the designs.
13. The non-transitory computer-readable storage medium of claim 12, wherein in designs with different pipeline depths, write accesses to memories may occur in different cycles; and wherein determining the correspondence between the first memory system and the second memory system involves:
symbolically simulating both pipelined designs for several cycles to discover the relationship between the first memory system and the second memory system;
guessing in which pipeline cycles the contents of the first memory system and the contents of the second memory system match; and
proving by induction that the guess holds for all times.
14. The non-transitory computer-readable storage medium of claim 13,
wherein the initial contents of the first memory system and the second memory system are assumed to be substantially the same; and
wherein comparing the outputs further comprises unrolling the pipelines to represent design outputs as combinational blocks comprised of the pipeline stages but without pipeline registers.
15. The non-transitory computer-readable storage medium of claim 14,
wherein knowing the initial state of a memory system and unrolling the pipelines allows subsequent read and write accesses fromto the memory system to be represented combinationally; and
wherein determining that the memories correspond in certain pipeline cycles allows checking the equivalence of the design outputs using a combinational equivalence check instead of a sequential equivalence check.
16. The non-transitory computer-readable storage medium of claim 11, wherein the method is used to generate a complete proof that verifies that a register-transfer-level description of a design is functionally equivalent to an original high-level description of the design.
17. The non-transitory computer-readable storage medium of claim 11, wherein the representation of data in the first memory system is different from the representation of data in the second memory system.
18. The non-transitory computer-readable storage medium of claim 11, wherein the first memory system andor the second memory system are comprised of multiple memories.
19. The non-transitory computer-readable storage medium of claim 11, further comprising:
receiving a user-generated specification that specifies how the memory system of the first pipelined design and the memory system of the second pipelined design match; and
using the user-generated specification to assist in determining the correspondence between the first memory system and the second memory system.
20. An apparatus that formally proves the functional equivalence of pipelined designs containing memories, comprising:
a receiving mechanism configured to receive a specification for a first pipelined design and a specification for a second pipelined design, wherein the first pipelined design includes a first memory system and the second pipelined design includes a second memory system;
a generating mechanism configured to generate representations of the first pipelined design and the second pipelined design in a combinational form, wherein the representations are generated based partly or solely on a correspondence between memory operations on the first memory system and corresponding memory operations on the second memory system, and wherein memory operations in the first memory system and the second memory system are converted into corresponding combinational operations based partly or solely on design inputs; and
a comparison mechanism configured to compare the combinational outputs of the first pipelined design and the combinational outputs of the second pipelined design to verify that the designs are functionally equivalent.