Efficient execution of alternating automaton representing a safety assertion for a circuit
US10831956B2 · kind B2 · utility
Assignee
Inventors
Key dates
| Filing date | Nov 30, 2017 |
| Grant date | Nov 10, 2020 |
| Priority date | — |
| Expiry date | Mar 1, 2039 |
Classification
- Technology area (CPC G)Physics
- CPC primaryG06F2119/18
- WIPO fieldComputer technology
- WIPO sectorElectrical engineering
Abstract
A system receive as input a circuit design and a description of the behavior of the circuit design specified as assertions. The system generates a model used for verifying that the circuit design satisfies the specified behavior. The system generates an alternating automaton representing the assertions. The alternating automaton may be non-deterministic. The system translates the alternating automaton to a finite state machine (FSM) that may be represented using a representation such as a register transfer level (RTL) representation. The system models existential transitions in the state machine using variables. As a result, the system generates fewer states in the state machine, thereby requiring significantly less memory resources for processing the assertion. The system validates the circuit design using the state machine for further design and manufacture of the circuit.
Source: USPTO / EPO open patent data. Objective bibliographic and citation counts.