Sciweavers

FMCAD
2009
Springer
13 years 11 months ago
Synthesizing robust systems
—Many specifications include assumptions on the environment. If the environment satisfies the assumptions then a correct system reacts as intended. However, when the environmen...
Roderick Bloem, Karin Greimel, Thomas A. Henzinger...
FMCAD
2009
Springer
13 years 11 months ago
Formal verification of analog designs using MetiTarski
William Denman, Behzad Akbarpour, Sofiène T...
FMCAD
2009
Springer
13 years 11 months ago
Scalable conditional equivalence checking: An automated invariant-generation based approach
—Sequential equivalence checking (SEC) technologies, capable of demonstrating the behavioral equivalence of two designs, have grown dramatically in capacity over the past decades...
Jason Baumgartner, Hari Mony, Michael L. Case, Jun...
FMCAD
2009
Springer
13 years 11 months ago
Interpolation-sequence based model checking
Yakir Vizel, Orna Grumberg
FMCAD
2009
Springer
13 years 11 months ago
Mixed abstractions for floating-point arithmetic
stractions for Floating-Point Arithmetic Angelo Brillout Computer Systems Institute, ETH Zurich Daniel Kroening and Thomas Wahl Oxford University Computing Laboratory Abstract—Fl...
Angelo Brillout, Daniel Kroening, Thomas Wahl
FMCAD
2009
Springer
13 years 11 months ago
Decision diagrams for linear arithmetic
—Boolean manipulation and existential quantification of numeric variables from linear arithmetic (LA) formulas is at the core of many program analysis and software model checkin...
Sagar Chaki, Arie Gurfinkel, Ofer Strichman
FMCAD
2009
Springer
13 years 11 months ago
Scaling VLSI design debugging with interpolation
—Given an erroneous design, functional verification returns an error trace exhibiting a mismatch between the specification and the implementation of a design. Automated design ...
Brian Keng, Andreas G. Veneris
FMCAD
2009
Springer
13 years 11 months ago
Assume-guarantee validation for STE properties within an SVA environment
Abstract—Symbolic Trajectory Evaluation is an industrialstrength verification method, based on symbolic simulation and abstraction, that has been highly successful in data path ...
Zurab Khasidashvili, Gavriel Gavrielov, Tom Melham
FMCAD
2009
Springer
13 years 11 months ago
Retiming and resynthesis with sweep are complete for sequential transformation
— There is a long history of investigations and debates on whether a sequence of retiming and resynthesis is complete for all sequential transformations (on steady states). It ha...
Hai Zhou
FMCAD
2009
Springer
13 years 11 months ago
Protocol verification using flows: An industrial experience
John W. O'Leary, Murali Talupur, Mark R. Tuttle