Titlebook: Correct Hardware Design and Verification Methods; 11th IFIP WG 10.5 Ad Tiziana Margaria,Tom Melham Conference proceedings 2001 Springer-Ver

方舟

Applications of Hierarchical Verification in Model Checkingms to successfully verify a wide spectrum of large and complex circuits. This paper describes a variety of the decomposition techniques that we have used as part of a large industrial formal verification effort on the Intel Pentium® 4 (Willamette) processor.

dialect

微不足道

Infect

Efficient Reachability Analysis and Refinement Checking of Timed Automata Using BDDs timed automata [.]. Matrix-based algorithms for the reachability analysis of timed automata are implemented in tools like Kronos, Uppaal, HyTech and Rabbit. A new BDD-based version of Rabbit, which supports also refinement checking, is now available.

BRUNT

Deriving Real-Time Programs from Duration Calculus SpecificationsThe main idea of our approach is to model discretization at state level by introducing the discrete states approximating the continuous ones, and then derive a specification of the control program over discrete states. Then the control program is derived from its specification using an extension of

懦夫

轿车

Formally-Based Design Evaluation Logic in Lotos - the ISO Language Of Temporal Ordering Specification). Relations for (strong) conformance are defined to verify a design specification against a high-level specification. Tools have been developed for automated testing and verification of conformance between an implementation and it

Detain

带来的感觉

Register Transformations with Multiple Clock Domainsance and power requirements. In this paper, we identify a special case of multiple clocking that encompasses typical design styles, and we present a theory enabling a wide range of register transformations relating to the multiple clock domains. For example, we can perform pipelining, phase abstract

有毛就脱毛

Temporal Properties of Self-Timed Ringst self-timed networks, a ring, and note that for timing applications, self-timed rings should maintain uniform spacing of events. In practice, all previous designs of which we are aware cluster events into bursts. In this paper, we describe a dynamical systems approach to verify the temporal propert