Formal verification of random priority-based arbiters using property strengthening and underapproximations
US8370553B2 · kind B2 · utility
Assignee
Inventors
Key dates
| Filing date | Oct 18, 2010 |
| Grant date | Feb 5, 2013 |
| Priority date | — |
| Expiry date | Jul 30, 2031 |
Classification
- Technology area (CPC G)Physics
- CPC primaryG06F13/364
- WIPO fieldComputer technology
- WIPO sectorElectrical engineering
Abstract
A mechanism is provide for formally verifying random priority-based arbiters. A determination is made as to whether a random priority-based arbiter is blocking one of a set of output ports or a set of input ports. Responsive to the first predetermined time period expiring before the processor determines whether the random priority-based arbiter is blocking, a determination is made as to whether the random priority-based arbiter is blocking one of the set of output ports or the set of input ports within a second predetermined time period using the random seed and at least one of property strengthening or underapproximation. Responsive to the processor determining that the random priority-based arbiter satisfies a non-blocking specification such that not one of the set of output ports or the set of input ports is blocked within the second predetermined time period, the random priority-based arbiter is validated as satisfying the non-blocking specification.
Source: USPTO / EPO open patent data. Objective bibliographic and citation counts.