the proceedings contain 40 papers. the topics discussed include: verification challenges in configurable processor design with ASIP meister;towards the pervasive verification of automotive systems;finding and fixing f...
详细信息
ISBN:
(纸本)3540291059
the proceedings contain 40 papers. the topics discussed include: verification challenges in configurable processor design with ASIP meister;towards the pervasive verification of automotive systems;finding and fixing faults;verifying quantitative properties using bound functions;interleaved invariant checking with dynamic abstraction;automatic formal verification of liveness for pipelined processors with multicycle functional units;saturation-based symbolic reachability analysis using conjunctive and disjunctive partitioning;regular vacuity;automatic generation of hints for symbolic traversal;on the verification of memory management mechanims;formal verification of synchronizers;and resolving quartz overloading.
the proceedings contain 35 papers. the special focus in this conference is on correcthardwaredesign and verificationmethods. the topics include: hardware synthesis using SAFL and application to processor design;app...
ISBN:
(纸本)3540425411
the proceedings contain 35 papers. the special focus in this conference is on correcthardwaredesign and verificationmethods. the topics include: hardware synthesis using SAFL and application to processor design;applications of hierarchical verification in model checking;pruning techniques for the sat-based bounded model checking problem;heuristics for hierarchical partitioning with application to model checking;efficient reachability analysis and refinement checking of timed automata using BDDS;deriving real-time programs from duration calculus specifications;reproducing synchronization bugs with model checking;register transformations with multiple clock domains;coverability analysis using symbolic model checking;verification of basic block schedules using RTL transformations;parameterized verification of the flash cache coherence protocol by compositional model checking;towards provably-correcthardware compilation tools based on pass separation techniques;a higher-level language for hardware synthesis;hierarchical verification using an MDG-HOL hybrid tool;efficient debugging in a formal verification environment;using combinatorial optimization methods for quantification scheduling;formal verification of the vamp floating point unit;refinement-based formal verification of asynchronous wrappers for independently clocked domains in systems on chip;formal verification of conflict detection algorithms;induction-oriented formal verification in symmetric interconnection network s;a framework for microprocessor correctness statements;from operational semantics to denotational semantics for verilog and efficient verification of a class of linear hybrid automata using linear programming.
the paper presents high-level modelling and formal analysis and verification on an FPGA-based multigigabit network monitoring system called Scampi. UPPAAL was applied in this work to establish some correctness and thr...
详细信息
ISBN:
(纸本)3540291059
the paper presents high-level modelling and formal analysis and verification on an FPGA-based multigigabit network monitoring system called Scampi. UPPAAL was applied in this work to establish some correctness and throughput results on a model intentionally built using patterns reusable in other similar projects. Some initial experiments with parametric analysis using TREX were performed too.
It is easy to write and verify real-time specifications with existing languages and methods;one just represents time as an ordinary variable and expresses timing requirements with special timer variables. the resultin...
详细信息
ISBN:
(纸本)3540291059
It is easy to write and verify real-time specifications with existing languages and methods;one just represents time as an ordinary variable and expresses timing requirements with special timer variables. the resulting specifications can be verified with an ordinary model checker. this basic idea and some less obvious details are explained, and results are presented for two examples.
Quartz is a new declarative hardware description language with polymorphism, overloading, higher-order combinators and a relational approach to data flow, supporting formal reasoning for designverification in the sam...
详细信息
ISBN:
(纸本)3540291059
Quartz is a new declarative hardware description language with polymorphism, overloading, higher-order combinators and a relational approach to data flow, supporting formal reasoning for designverification in the same style as the Ruby language. the combination of parametric polymorphism and overloading within the language involves the implementation of a system of constrained types. this paper describes how Quartz overloading is resolved using satisfiability matrix predicates. Our algorithm is a new approach to overloading designed specifically for the requirements of describing hardware in Quartz.
the evolution of SAT technology over the last decade has motivated its application in model checking, initially through the utilization of SAT in bounded model checking (BMC) and, more recently, in unbounded model che...
详细信息
ISBN:
(纸本)3540291059
the evolution of SAT technology over the last decade has motivated its application in model checking, initially through the utilization of SAT in bounded model checking (BMC) and, more recently, in unbounded model checking (UMC). this paper addresses the utilization of interpolants in UMC and proposes two techniques for improving the original interpolant-based UMC algorithm. these techniques include improvements to the computation of interpolants, and redefining the organization of the unbounded model checking algorithm given the information extracted from interpolant computation.
作者：
Fujita, MUniv Tokyo
VLSI Design & Educ Ctr Bunkyo Ku Tokyo 1130032 Japan
A behavior-RTL equivalence checking method based on bottom-up reasoning is presented. Behavior and RTL descriptions are converted into dependence graphs from which virtual controllers/datapaths are generated. Actual e...
详细信息
ISBN:
(纸本)3540291059
A behavior-RTL equivalence checking method based on bottom-up reasoning is presented. Behavior and RTL descriptions are converted into dependence graphs from which virtual controllers/datapaths are generated. Actual equivalence checking is based on isomorphism analysis on dependence graphs and also virtual controllers/datapaths. First equivalence classes on partial computations are extracted by using Boolean reasoning on virtual controllers/datapaths. then these equivalence classes are used to prove the equivalence of the entire descriptions in a bottom-up way.
Formal property checking is used to check whether a circuit satisfies a temporal property or not. An important goal during the development of properties is the formulation of general proofs. Since assumptions of prope...
详细信息
ISBN:
(纸本)3540291059
Formal property checking is used to check whether a circuit satisfies a temporal property or not. An important goal during the development of properties is the formulation of general proofs. Since assumptions of properties define the situations under which the commitments are checked, in order to obtain general proofs assumptions should be made as general as possible. In practice this is accomplished iteratively by generalizing the assumptions step by step. thus, the verification engineer may start with strong assumptions and weakens them gradually. In this paper we propose a new approach to speed up SAT-based iterative property checking. this process can be exploited by reusing conflict clauses in the corresponding SAT instances of consecutive property checking problems. By this the search space is pruned, since recomputations of identical conflicts are avoided.
暂无评论