Hardware and Software: Verification and Testing: 6th International Haifa Verification Conference, HVC 2010, Haifa, Israel, October 4-7, 2010. Revised Selected PapersSharon Barner, Ian Harris, Daniel Kroening, Orna Raz This book constitutes the thoroughly refereed post-conference proceedings of the 6th International Haifa Verification Conference, HVC 2010, held in Haifa, Israel in October 2010. The 10 revised full papers presented together with 7 invited papers were carefully reviewed and selected from 30 submissions. The papers address all current issues, challenges and future directions of verification for hardware, software, and hybrid systems and have a research focus on hybrid methods and the migration of methods and ideas between hardware and software, static and dynamic analysis, pre- and post-silicon. |
Contents
| 1 | |
| 3 | |
| 4 | |
| 5 | |
An Introduction to Test Specification in FQL | 9 |
What to Do When Things Go Wrong | 23 |
Special Session on Debugging | 24 |
Debugging Unrealizable Specifications with ModelBased Diagnosis | 29 |
Variants of LTL Query Checking | 76 |
SATSolving Based on Boundary Point Elimination | 93 |
An Industrial Evaluation | 112 |
A Strategy Language for SimulationBased Verification of Hardware | 129 |
Advances in Simultaneous Multithreading Testcase Generation Methods | 146 |
Revisiting Synthesis of GR1 Specifications | 161 |
An Efficient and Flexible Approach to Resolution Proof Reduction | 182 |
| 197 | |
Parallelizing a Symbolic Compositional ModelChecking Algorithm | 46 |
Reaching Coverage Closure in Postsilicon Validation | 60 |
Other editions - View all
Common terms and phrases
achieved algorithm approach assignment automatic basic block BDD nodes Boolean boundary points BPE procedure BPE-SAT bring-up Büchi automaton bugs CDCL SAT-solvers clauses of F CNF formula code coverage complexity computation conflict coverage closure debugging defined denoted describe diagnosis edges eliminated environment example execution existential quantification falsified fixpoint full-X-tree function functional verification hardware Heidelberg IEEE implementation input instruction irritator threads labeled LNCS Los Alamitos method minimal model checking Picosat placeholder point of F post-silicon validation POWER7 pre-silicon problem processor query random reachability realizable regression suite regular expressions resolution proof resolvent safe-X-tree satisfies scenarios Section silicon simulation Simultaneous Multithreading solution solver Springer strategy subformulas symbolic simulation syntactic reduction synthesis SystemVerilog tape-out techniques temporal logic test templates testcase Thread Irritation tion transition relation unrealizable core variables verification Verilog vlogsl