Formal verification is playing a significant role in IC design.However,the common models for verification either have their complexity problems or have applicable limitations.In order to overcome the deficiencies,a no...Formal verification is playing a significant role in IC design.However,the common models for verification either have their complexity problems or have applicable limitations.In order to overcome the deficiencies,a novel model-WGL(Weighted Generalized List)is proposed,which is based on the general-list decomposition of polynomials,with three different weights and manipulation rules introduced to effect node sharing and the canonicity.Timing parameters and operations on them are also considered.Examples show the word-level WGL is the only model to linearly represent the common word-level functions and the bit-level WGL is especially suitable for arithmetic intensive circuits.The model is proved to be a uniform and efficient model for both bit-level and word-level functions.Then based on the WGL model,a backward-construction verification approach is proposed,which reduces time and space complexity for multipliers to polynomial complexity(time complexity is less than O(n3.6)and space complexity is less than O(n1.5))without hierarchical partitioning.Both the model and the verification method show their theoretical and applicable significance in IC design.展开更多
To evaluate the operation comfortability in the master-slave robotic minimally invasive surgery(MIS), an optimal function was built with two operation comfortability decided indices, i.e., the center distance and volu...To evaluate the operation comfortability in the master-slave robotic minimally invasive surgery(MIS), an optimal function was built with two operation comfortability decided indices, i.e., the center distance and volume contact ratio. Two verifying experiments on Phantom Desktop and Micro Hand S were conducted. Experimental results show that the operation effect at the optimal relative location is better than that at the random location, which means that the optimal function constructed in this paper is effective in optimizing the operation comfortability.展开更多
The bar code is one of the identification technologies used more successfully in the world. This technology was first developed as the second half of the twentieth century and quickly achieved acceptance in both indus...The bar code is one of the identification technologies used more successfully in the world. This technology was first developed as the second half of the twentieth century and quickly achieved acceptance in both industry and commerce. In this paper studies are discussed on the design, development and printing of one-dimensional barcodes of the symbologies Code 39 and Interleaved 2 of 5. There are also discussed techniques for recovering the information encoded in the bar code, which can be extended to other symbologies. The purpose of the paper is the development of an open solution with the objective to make the decoding of barcodes using computer vision techniques possible, which will be divided into four basic stages： acquisition, pre-processing, processing and presentation of results. Practical tests conducted with samples show satisfactory results, validating the operating principles of the elements involved. The proposed objective was achieved and practical tests validated the operating principles of the elements addressed by providing contribution to that segment decoding barcodes.展开更多
基金Sponsored by the National Natural Science Foundation of China(Grant No.69973014and60273081)the Natural Science Foundation of Heilongjiang Province(Grant No.F0209)HEU Foundation(Grant No.HEUF04088).
文摘Formal verification is playing a significant role in IC design.However,the common models for verification either have their complexity problems or have applicable limitations.In order to overcome the deficiencies,a novel model-WGL(Weighted Generalized List)is proposed,which is based on the general-list decomposition of polynomials,with three different weights and manipulation rules introduced to effect node sharing and the canonicity.Timing parameters and operations on them are also considered.Examples show the word-level WGL is the only model to linearly represent the common word-level functions and the bit-level WGL is especially suitable for arithmetic intensive circuits.The model is proved to be a uniform and efficient model for both bit-level and word-level functions.Then based on the WGL model,a backward-construction verification approach is proposed,which reduces time and space complexity for multipliers to polynomial complexity(time complexity is less than O(n3.6)and space complexity is less than O(n1.5))without hierarchical partitioning.Both the model and the verification method show their theoretical and applicable significance in IC design.
基金Supported by the National High Technology Research and Development Program of China("863" Program,No.2012AA02A606)the Research Project of State Key Laboratory of Mechanical System and Vibration(MSV201412)
文摘To evaluate the operation comfortability in the master-slave robotic minimally invasive surgery(MIS), an optimal function was built with two operation comfortability decided indices, i.e., the center distance and volume contact ratio. Two verifying experiments on Phantom Desktop and Micro Hand S were conducted. Experimental results show that the operation effect at the optimal relative location is better than that at the random location, which means that the optimal function constructed in this paper is effective in optimizing the operation comfortability.
文摘The bar code is one of the identification technologies used more successfully in the world. This technology was first developed as the second half of the twentieth century and quickly achieved acceptance in both industry and commerce. In this paper studies are discussed on the design, development and printing of one-dimensional barcodes of the symbologies Code 39 and Interleaved 2 of 5. There are also discussed techniques for recovering the information encoded in the bar code, which can be extended to other symbologies. The purpose of the paper is the development of an open solution with the objective to make the decoding of barcodes using computer vision techniques possible, which will be divided into four basic stages： acquisition, pre-processing, processing and presentation of results. Practical tests conducted with samples show satisfactory results, validating the operating principles of the elements involved. The proposed objective was achieved and practical tests validated the operating principles of the elements addressed by providing contribution to that segment decoding barcodes.
