Method and apparatus for formally comparing stream-based designs
US7509604B1 · kind B1 · utility
Assignee
Inventors
Key dates
| Filing date | Jun 10, 2005 |
| Grant date | Mar 24, 2009 |
| Priority date | — |
| Expiry date | Apr 6, 2027 |
Classification
- Technology area (CPC G)Physics
- CPC primaryG06F30/3323
- WIPO fieldComputer technology
- WIPO sectorElectrical engineering
Abstract
An equivalency testing system, for formally comparing an RTLM and HLM, is presented. RTLM and HLM are first converted into DFGs RTLMDFG and HLMDFG. RTLMDFG and HLMDFG are then put into timestep form and are called RTLMts and HLMts. A test bench CSts is selected that couples RTLMts and HLMts. The combination of RTLMts[t], HLMts[t] and CSts[t] can have parts designated as datapath. Parts designated as datapath can be subject to a form of equivalence checking that seeks to prove equivalence by a form of inductive theorem proving. The theorem proving starts from initial conditions for HLMts[t] determined by partial execution of the HLM. A CSts for proving stream-based equivalence is presented. The CSts operates by allowing one DFG to process data as soon as it can, while not guaranteeing the same for a second DFG. The stream-based combining structure can be used in with any formal analysis tool.
Source: USPTO / EPO open patent data. Objective bibliographic and citation counts.