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 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.
Routing wires are dominant performance stoppers in deep sub-micron technologies, and there is an urgent need to take them into account already at higher levels of abstraction. However, the normal design flow gives the...
详细信息
ISBN:
(纸本)3540291059
Routing wires are dominant performance stoppers in deep sub-micron technologies, and there is an urgent need to take them into account already at higher levels of abstraction. However, the normal design flow gives the designer only limited control over the details of the lower levels, risking the quality of the final result. We propose a language, called Wired, which lets the designer express circuit function together with layout, in order to get more precise control over the result. the complexity of larger designs is managed by using parameterised connection patterns. the resulting circuit descriptions are compact, and yet capture detailed layout, including the size and positions of wires. We are able to analyse non-functional properties of these descriptions, by "running" them using non-standard versions of the wire and gate primitives. the language is relational, which means that we can build forwards, backwards and bi-directional analyses. Here, we show the description and analysis of various parallel prefix circuits, including a novel structure with small depth and low fanout.
design derivation, a correct-by-construction system design method, specifies behavior with abstract datatypes. Refining these abstract datatypes is necessary for architectural decomposition. A new transformation primi...
详细信息
暂无评论