The semantics of temporal logic is usually defined with respect to a word representing a computation path over a set of atomic propositions. A temporal logic formula does not contr...
el Sequential Memory Abstraction for Model Checking Per Bjesse Advanced Technology Group Synopsys Inc. Many designs intermingle large memories with wide data paths and nontrivial c...
Automatic techniques for software verification focus on obtaining witnesses of program failure. Such counterexamples often fail to localize the precise cause of an error and usuall...
Roopsha Samanta, Jyotirmoy V. Deshmukh, E. Allen E...
Post-silicon debug is the problem of determining what's wrong when the fabricated chip of a new design behaves incorrectly. This problem now consumes over half of the overall ...
Flavio M. de Paula, Marcel Gort, Alan J. Hu, Steve...
Abstract--This paper presents the verification of an asynchronous arbiter modeled at the circuit level with non-linear ordinary differential equations. We use Brockett's annul...
Abstract-- This work presents a technology-independent synthesis optimization that is effective in reducing the total number of state elements of a design. It works by identifying ...
Michael L. Case, Alan Mishchenko, Robert K. Brayto...
Synchronous Data flow (SDF) graphs have a simple and elegant semantics (essentially linear algebra) which makes SDF graphs eminently suitable as a vehicle for studying scheduling o...