In this paper we study the structure of k-transitive closures of directed paths and formulate several properties. Concept of k-transitive orientation generalizes the traditional concept of transitive orientation of a ...In this paper we study the structure of k-transitive closures of directed paths and formulate several properties. Concept of k-transitive orientation generalizes the traditional concept of transitive orientation of a graph.展开更多
An algorithm for the verification of strong open bisimulation in π-calculus with mismatch was presented, which is based on the symbolic transition graph (STG). Given two processes, we can convert them into two STGs b...An algorithm for the verification of strong open bisimulation in π-calculus with mismatch was presented, which is based on the symbolic transition graph (STG). Given two processes, we can convert them into two STGs by a set of rules at first. Next, the algorithm computes a predicate equation system (PES) from the STGs. This is the key step of the whole algorithm. Finally, the PES is solved and the greatest symbolic solution is got. Correctness of the algorithm is proved and time complexity discussed. It is shown that the worst-case time complexity is exponential.展开更多
A method for automatic verification of cache coherence protocols is presented, in which cache coherence protocols are modeled as concurrent value-passing processes, and control and data consistency requirement are des...A method for automatic verification of cache coherence protocols is presented, in which cache coherence protocols are modeled as concurrent value-passing processes, and control and data consistency requirement are described as formulas in first-order p-calculus. A model checker is employed to check if the protocol under investigation satisfies the required properties. Using this method a data consistency error has been revealed in a well-known cache coherence protocol. The error has been corrected, and the revised protocol has been shown free from data consistency error for any data domain size, by appealing to data independence technique.展开更多
At-speed testing using external tester requires an expensive equipment, thus built-in self-test (BIST) is an alternative technique due to its ability to perform on-chip at-speed self-testing. The main issue in BIST f...At-speed testing using external tester requires an expensive equipment, thus built-in self-test (BIST) is an alternative technique due to its ability to perform on-chip at-speed self-testing. The main issue in BIST for at-speed testing is to obtain high delay fault coverage with a low hardware overhead. This paper presents an improved loop-based BIST scheme, in which a configurable MISR (multiple-input signature register) is used to generate test-pair sequences. The structure and operation modes of the BIST scheme are described. The topological properties of the state-transit ion- graph of t he proposed B IS T scheme are analyzed. B ased on it, an approach to design and efficiently implement the proposed BIST scheme is developed. Experimental results on academic benchmark circuits are presented to demonstrate the effectiveness of the proposed BIST scheme as well as the design approach.展开更多
文摘In this paper we study the structure of k-transitive closures of directed paths and formulate several properties. Concept of k-transitive orientation generalizes the traditional concept of transitive orientation of a graph.
基金National Natural Science Foundation of China ( No. 6 98730 32 ) 86 3Hi-Τ ech Project ( 86 3-30 6 -ZT-0 6 -0 2 -2 )
文摘An algorithm for the verification of strong open bisimulation in π-calculus with mismatch was presented, which is based on the symbolic transition graph (STG). Given two processes, we can convert them into two STGs by a set of rules at first. Next, the algorithm computes a predicate equation system (PES) from the STGs. This is the key step of the whole algorithm. Finally, the PES is solved and the greatest symbolic solution is got. Correctness of the algorithm is proved and time complexity discussed. It is shown that the worst-case time complexity is exponential.
基金Supported by the Intel Strategic CAD Labs, the National Natural Science Foundation of China （Grant No. 60421001）, and the Chinese Academy of Sciences.
文摘A method for automatic verification of cache coherence protocols is presented, in which cache coherence protocols are modeled as concurrent value-passing processes, and control and data consistency requirement are described as formulas in first-order p-calculus. A model checker is employed to check if the protocol under investigation satisfies the required properties. Using this method a data consistency error has been revealed in a well-known cache coherence protocol. The error has been corrected, and the revised protocol has been shown free from data consistency error for any data domain size, by appealing to data independence technique.
基金the National Natural Science Foundation of China under grant Nos.69976002and 69733010.
文摘At-speed testing using external tester requires an expensive equipment, thus built-in self-test (BIST) is an alternative technique due to its ability to perform on-chip at-speed self-testing. The main issue in BIST for at-speed testing is to obtain high delay fault coverage with a low hardware overhead. This paper presents an improved loop-based BIST scheme, in which a configurable MISR (multiple-input signature register) is used to generate test-pair sequences. The structure and operation modes of the BIST scheme are described. The topological properties of the state-transit ion- graph of t he proposed B IS T scheme are analyzed. B ased on it, an approach to design and efficiently implement the proposed BIST scheme is developed. Experimental results on academic benchmark circuits are presented to demonstrate the effectiveness of the proposed BIST scheme as well as the design approach.
