A method, apparatus and computer program product for automatic parity check identification. The method comprising: automatically identifying a parity signal in a circuit design, wherein the parity signal is defined as a parity function of a set of support signals, wherein the automatic identificatio
A method, apparatus and computer program product for automatic parity check identification. The method comprising: automatically identifying a parity signal in a circuit design, wherein the parity signal is defined as a parity function of a set of support signals, wherein the automatic identification comprises: obtaining a candidate parity signal and a corresponding set of candidate support signals; and verifying that a bit flip in exactly one of any of the corresponding candidate set of support signals induces a bit flip on a value of the candidate parity signal; wherein said method further comprises reporting the automatically identified parity signal.
대표청구항▼
1. A computer-implemented method performed by a computerized device comprising a processor, the method comprising: analyzing a circuit design to find a parity signal out of a plurality of signals defined by the circuit design, wherein a value of the parity signal is defined as a parity function base
1. A computer-implemented method performed by a computerized device comprising a processor, the method comprising: analyzing a circuit design to find a parity signal out of a plurality of signals defined by the circuit design, wherein a value of the parity signal is defined as a parity function based on values of a set of support signals, wherein finding the parity signal comprises: obtaining a candidate parity signal and a corresponding set of candidate support signals; andverifying that the circuit design is configured to induce a bit flip on a value of the candidate parity signal in response to a bit flip in any single signal that is comprised by a subset of the set of candidate support signals, whereby the candidate signal is verified to be a parity signal with respect to the subset of the set of support signals;wherein said method further comprises reporting that the candidate parity signal was found to have the functionality of the parity signal. 2. The method of claim 1, wherein said obtaining the candidate parity signal comprises: performing a simulation of the circuit design;for each signal in the circuit design, flipping a value of the signal; andidentifying an effected signal whose value is flipped in response to flipping the value of the signal, whereby the effected signal is the candidate signal and the signal whose value is flipped is comprised by the corresponding candidate set of support signals. 3. The method of claim 1, wherein said verifying comprises utilizing a Boolean Satisfiability problem (SAT) Solver. 4. The method of claim 3, wherein said verifying comprises: constructing a Conjunctive Normal Form formula (CNF), the CNF comprising: a logic circuit and a replicated logic circuit, wherein the logic circuit is a portion of the circuit design defining a value of the candidate parity signal based on the corresponding set of candidate support signals;the logic circuit having the corresponding candidate set of support signals as inputs to the logic circuit,the replicated logic circuit having, as inputs, values of the corresponding candidate set of support signals, each such value potentially flipped based on a value of an auxiliary signal,wherein the auxiliary signals are constrained using cardinality constraint logic to ensure that exactly one auxiliary signal is operable to flip exactly one of support signal,wherein values of the candidate parity signal in the logic circuit and in the replicated logic circuit are compared; andwherein the CNF is satisfiable if and only if the compared values are different. 5. The method of claim 4, wherein said verifying comprises: attempting to solve the CNF using the SAT solver, and in response to a determination that the CNF is unsatisfiable, indicating that the candidate parity signal is the parity signal and that the corresponding candidate set of support signals are the set of support signals. 6. The method of claim 5, wherein in response to a determination by the SAT solver that the CNF is satisfiable by a satisfying assignment: determining, based on the satisfying assignment, a candidate support signal of the candidate set of support signals for which a flipped value does not induce a flipped value of the candidate parity signal;removing the candidate support signal from the candidate set of support signals;reconstructing the CNF based on the updated candidate set of support signals; andattempting to solve the reconstructed CNF. 7. The method of claim 1, further comprising: identifying a parity-based error checker based on the parity signal;extracting checker information of the parity-based error checker, wherein the checker information comprises a protected state storage device which is protected by the parity-based error checker; andwherein said reporting comprises reporting to a user the existence of the parity-based error checker the checker information. 8. The method of claim 7, wherein the checker information further comprises checker gating conditions and type of parity protected. 9. The method of claim 1, further comprising: utilizing the reported identified parity signal for verification of the circuit design. 10. The method of claim 9, wherein the verification of the circuit design comprises at least one of the following: performing manual logic review of the circuit design;performing formal verification of the functionality of a parity-based error checker which is based on the parity signal; andautomatically verifying that the circuit design adheres to a requirement of a corresponding circuit specification. 11. A computerized apparatus having a processor, the processor being adapted to perform the steps of: analyzing a circuit design to find a parity signal out of a plurality of signals defined by the circuit design, wherein a value of the parity signal is defined as a parity function of based on values of a set of support signals, wherein finding the parity signal comprises: obtaining a candidate parity signal and a corresponding set of candidate support signals; andverifying that the circuit design is configured to induce a bit flip on a value of the candidate parity signal in response to a bit flip in any single signal that is comprised by a subset of the set of candidate support signals, whereby the candidate signal is verified to be a parity signal with respect to the subset of the set of support signals;wherein said processor further adapted to report that the candidate parity signal was found to have the functionality of the parity signal. 12. The computerized apparatus of claim 11, wherein obtaining the candidate parity signal comprises: performing a simulation of the circuit design;for each signal in the circuit design, flipping a value of the signal; andidentifying an effected signal whose value is flipped in response to flipping the value of the signal, whereby the effected signal is the candidate signal and the signal whose value is flipped is comprised by the corresponding candidate set of support signals. 13. The computerized apparatus of claim 11, wherein the verifying comprises utilizing a Boolean Satisfiability problem (SAT) Solver. 14. The computerized apparatus of claim 13, wherein verifying comprises: constructing a Conjunctive Normal Form formula (CNF), the CNF comprising: a logic circuit and a replicated logic circuit, wherein the logic circuit is a portion of the circuit design defining a value of the candidate parity signal based on the corresponding set of candidate support signals;the logic circuit having the corresponding candidate set of support signals as inputs to the logic circuit,the replicated logic circuit having, as inputs, values of the corresponding candidate set of support signals, each such value potentially flipped based on a value of an auxiliary signal,wherein the auxiliary signals are constrained using cardinality constraint logic to ensure that exactly one auxiliary signal is operable to flip exactly one of support signal,wherein values of the candidate parity signal in the logic circuit and in the replicated logic circuit are compared; andwherein the CNF is satisfiable if and only if the compared values are different. 15. The computerized apparatus of claim 14, wherein verifying comprises: attempting to solve the CNF using the SAT solver, and in response to a determination that the CNF is unsatisfiable, indicating that the candidate parity signal is the parity signal and that the corresponding candidate set of support signals are the set of support signals. 16. The computerized apparatus of claim 15, wherein in response to a determination by the SAT solver that the CNF is satisfiable by a satisfying assignment, the processor is adapted to perform: determining, based on the satisfying assignment, a candidate support signal of the candidate set of support signals for which a flipped value does not induce a flipped value of the candidate parity signal;removing the candidate support signal from the candidate set of support signals;reconstructing the CNF based on the updated candidate set of support signals; andattempting to solve the reconstructed CNF. 17. The computerized apparatus of claim 11, wherein said processor being further adapted to perform: identifying a parity-based error checker based on the parity signal;extracting checker information of the parity-based error checker, wherein the checker information comprises a protected state storage device which is protected by the parity-based error checker; andwherein said reporting comprises reporting to a user the existence of the parity-based error checker the checker information. 18. The computerized apparatus of claim 17, wherein the checker information further comprises checker gating conditions and type of parity protected. 19. The computerized apparatus of claim 11, wherein said processor being further adapted to perform: utilizing the reported identified parity signal for verification of the circuit design. 20. A computer program product comprising: a non-transitory computer readable medium retaining program instructions, which when read by a processor, cause the processor to performs the steps of:analyzing a circuit design to find a parity signal out of a plurality of signals defined by the circuit design, wherein a value of the parity signal is defined as a parity function based on values of a set of support signals, wherein finding the parity signal comprises: obtaining a candidate parity signal and a corresponding set of candidate support signals; andverifying that the circuit design is configured to induce a bit flip on a value of the candidate parity signal in response to a bit flip in any single signal that is comprised by a subset of the set of candidate support signals, whereby the candidate signal is verified to be a parity signal with respect to the subset of the set of support signals;wherein said program instruction, when read by the processor, further cause the processor to report that the candidate parity signal was found to have the functionality of the parity signal.
연구과제 타임라인
LOADING...
LOADING...
LOADING...
LOADING...
LOADING...
이 특허에 인용된 특허 (33)
Hashimoto Masashi,JPX, Apparatus and method for a party check logic circuit in a dynamic random access memory.
Jennings Andrew T. (West Chester PA) Schibinger Joseph S. (Phoenixville PA) Kalemba Ronald J. (Berwyn PA), Array for simulating computer functions for large computer systems.
Smith, Jane L.; Kirchenbauer, Douglas Paul; Muller, Robert A., Automated hardware parity and parity error generation technique for high availability integrated circuits.
Densham Rodney Hugh,GBX ; Kentish William,GBX ; Eastty Peter Charles,GBX ; Cooke Conrad Charles,GBX, Data processing system having capability to interpolate processing coefficients.
Agrawal Om P. ; Stanley Claudia A. ; He Xiaojie (Warren) ; Lee Chong M. ; Balzli ; Jr. Robert M. ; Metzger Larry R. ; Ilgenstein Kerry A., Enhanced macrocell module for high density CPLD architectures.
Ammann Lawrence M. (Vienna VA) Jackson Howard C. (Berthoud CO) Johnson Charles D. (Boulder CO) Lutter Edward P. (Boulder CO), Fast emulator using slow processor.
Read Andrew J. (Sunnyvale CA) Papamarcos Mark S. (San Jose CA) Heideman Wayne P. (San Jose CA) Mardjuki Robert K. (Peasanton CA) Couch Robert K. (Santa Cruz CA) Jaeger Peter R. (San Jose CA) Kappauf , Hardware modeling system and method of use.
Park,Min sang; Kwak,Jin seok; Jang,Seong jin, Integrated circuit devices having data inversion circuits therein with multi-bit prefetch structures and methods of operating same.
Bruce Kenneth E. (Nashua NH) Conway John W. (Waltham MA) Lombardo ; Jr. Ralph M. (Lowell MA) Tarbox Bruce H. (Billerica MA), Logic system for selectively reconfiguring an intersystem communication link.
Caprasse Friedhelm (Zorneding DEX), Method and apparatus for monitoring the consistency of successive binary code signal groups in data processing equipment.
Jibbe,Mahmoud K.; Khor,Chin, Method for controlling and emulating functional and logical behaviors of an array of storage devices for different protocols.
Roesner,Wolfgang; Shadowen,Robert J.; Williams,Derek E., Method, system and program product for providing a configuration specification language supporting error checking dials.
Donaldson Darrel D. (Lancaster MA) Gillett ; Jr. Richard B. (Westford MA), Node with coupling resistor for limiting current flow through driver during overlap condition.
Baker Ernest D. (Boca Raton FL) Dinwiddie ; Jr. John M. (West Palm Beach FL) Grice Lonnie E. (Boca Raton FL) Joyce James M. (Boca Raton FL) Loffredo John M. (Deerfield Beach FL) Sanderson Kenneth R. , Uncoupling a central processing unit from its associated hardware for interaction with data handling apparatus alien to.
※ AI-Helper는 부적절한 답변을 할 수 있습니다.