Results 1 to 10 of about 2,705 (127)
A Faithful Semantics for Generalised Symbolic Trajectory Evaluation [PDF]
Logical Methods in Computer Science, 2009 Generalised Symbolic Trajectory Evaluation (GSTE) is a high-capacity formal verification technique for hardware. GSTE uses abstraction, meaning that details of the circuit behaviour are removed from the circuit model.
Koen Claessen, Jan-Willem Roorda
doaj +4 more sources
Formal hardware verification by symbolic ternary trajectory evaluation [PDF]
Proceedings of the 28th conference on ACM/IEEE design automation conference - DAC '91, 1991 Symbolic trajectory evaluation is a new approach to formal hardware verification combining the circuit modeling capabilities of symbolic logic simulation with some of the analytic methods found in temporal logic model checkers. We have created such an evaluator by extending the symbolic switch-level simulator COSMOS. This program gains added efficiency
Bryant, Randal E. +2 more
+11 more sources
Word-Level Symbolic Trajectory Evaluation [PDF]
, 2015 19 pages, 3 figures, 2 tables, full version of paper in International Conference on Computer-Aided Verification (CAV ...
Chakraborty, Supratik +6 more
+6 more sources
Formal verification of PowerPC arrays using symbolic trajectory evaluation [PDF]
Proceedings of the 33rd annual conference on Design automation conference - DAC '96, 1996 Verifying memory arrays such as on-chip caches and register files is a difficult part of designing a microprocessor. Current toolscannot verify the equivalence of the arrays to their behavioral or RTL models, nor their correct functioning at the transistor level.
Manesh Pandey +3 more
+4 more sources
Composing symbolic trajectory evaluation results [PDF]
, 1994 Symbolic trajectory evaluation shows much promise as a method for verifying large scale VLSI designs with a high degree of automation. However, to verify today's designs, a method for composing partial verification results is needed. Consequently, we have proven a number of inference rules for the composition of symbolic trajectory evaluation results ...
Scott Hazelhurst, Carl-Johan H. Seger
openaire +2 more sources
Automatic Abstraction in Symbolic Trajectory Evaluation [PDF]
Formal Methods in Computer Aided Design (FMCAD'07), 2007 Symbolic trajectory evaluation (STE) is a model checking technology based on symbolic simulation over a lattice of abstract state sets. The STE algorithm operates over families of these abstractions encoded by Boolean formulas, enabling verification with many different abstraction cases in a single modelchecking run.
Adams, S, Bjoerk, M, Melham, T, Seger, C
+6 more sources
A New SAT-Based Algorithm for Symbolic Trajectory Evaluation [PDF]
, 2005 We present a new SAT-based algorithm for Symbolic Trajectory Evaluation (STE), and compare it to more established SAT-based techniques for STE.
Jan-Willem Roorda, Koen Claessen
openaire +3 more sources
Automatic Refinement and Vacuity Detection for Symbolic Trajectory Evaluation [PDF]
, 2006 Symbolic Trajectory Evaluation (STE) is a powerful technique for model checking. It is based on 3-valued symbolic simulation, using 0,1 and X (”unknown”). The X value is used to abstract away parts of the circuit. The abstraction is derived from the user's specification.
Rachel Tzoref, Orna Grumberg
openaire +3 more sources
SAT-Based Assistance in Abstraction Refinement for Symbolic Trajectory Evaluation [PDF]
, 2006 We present a SAT-based algorithm for assisting users of Symbolic Trajectory Evaluation (STE) in manual abstraction refinement. As a case study, we demonstrate the usefulness of the algorithm by showing how to refine and verify an STE specification of a CAM.
Jan-Willem Roorda, Koen Claessen
openaire +2 more sources
Abstraction discovery and refinement for model checking by symbolic trajectory evaluation
, 2014 This dissertation documents two contributions to automating the formal verification of hardware – particularly memory-intensive circuits – by Symbolic Trajectory Evaluation (STE), a model checking technique based on symbolic simulation over abstract sets of states.
Sara Adams
+5 more sources