Formal verification is fundamental in many phases of digital systems design. The most successful verification procedures employ Ordered Binary Decision Diagrams (OBDDs) as canonical representation for both Boolean cir...Formal verification is fundamental in many phases of digital systems design. The most successful verification procedures employ Ordered Binary Decision Diagrams (OBDDs) as canonical representation for both Boolean circuit specifications and logic designs, but these methods require a large amount of memory and time. Due to these limitations, several models of Decision Diagrams have been studied and other verification techniques have been proposed. In this paper, we have used probabilistic verification with Galois (or finite) field GF(2m) modifying the CUDD package for the computation of signatures in classical OBDDs, and for the construction of Mod2-OBDDs (also known as ?-OBDDs). Mod2-OBDDs have been constructed with a two-level layer of ?-nodes using a positive Davio expansion (pDE) for a given variable. The sizes of the Mod2-OBDDs obtained with our method are lower than the Mod2-OBDDs sizes obtained with other similar methods.展开更多
视图的秘密分享是图像信息安全领域独具吸引力的研究问题。寻求秘密视图完全的(Perfect)和理想的(Ideal)门限秘密分享方案(也称图像门限分享的完备方案),则是其中富有挑战性的未决课题。文中引入灰度值域GF(2m)上像素矩阵秘密分享的新...视图的秘密分享是图像信息安全领域独具吸引力的研究问题。寻求秘密视图完全的(Perfect)和理想的(Ideal)门限秘密分享方案(也称图像门限分享的完备方案),则是其中富有挑战性的未决课题。文中引入灰度值域GF(2m)上像素矩阵秘密分享的新观点和相应的代数几何编码方法,实现了数字图像(t,n)门限秘密分享的一种完备方案。该方案能够将一幅或多幅秘密图像编码为n幅各具随机视觉内容,同时又共具(t,n)门限结构的影子图像(或称份额图像)。证明了这种秘密分享方案的(t,n)门限结构不仅是完全的而且也是理想的,并给出了提高像素灰度值域GF(2m)上图像秘密分享算法效率的"m位像素值的分拆与并行"方法。分析表明,该图像秘密分享方法可以应用于高安全等级的秘密图像的网络多路径传输、保密图像信息的分散式存储控制、高维图形码(Bar-code in k dimension)和弹出码(Popcode)等新一代信息载体技术的识读控制等各方面。展开更多
文摘Formal verification is fundamental in many phases of digital systems design. The most successful verification procedures employ Ordered Binary Decision Diagrams (OBDDs) as canonical representation for both Boolean circuit specifications and logic designs, but these methods require a large amount of memory and time. Due to these limitations, several models of Decision Diagrams have been studied and other verification techniques have been proposed. In this paper, we have used probabilistic verification with Galois (or finite) field GF(2m) modifying the CUDD package for the computation of signatures in classical OBDDs, and for the construction of Mod2-OBDDs (also known as ?-OBDDs). Mod2-OBDDs have been constructed with a two-level layer of ?-nodes using a positive Davio expansion (pDE) for a given variable. The sizes of the Mod2-OBDDs obtained with our method are lower than the Mod2-OBDDs sizes obtained with other similar methods.
文摘视图的秘密分享是图像信息安全领域独具吸引力的研究问题。寻求秘密视图完全的(Perfect)和理想的(Ideal)门限秘密分享方案(也称图像门限分享的完备方案),则是其中富有挑战性的未决课题。文中引入灰度值域GF(2m)上像素矩阵秘密分享的新观点和相应的代数几何编码方法,实现了数字图像(t,n)门限秘密分享的一种完备方案。该方案能够将一幅或多幅秘密图像编码为n幅各具随机视觉内容,同时又共具(t,n)门限结构的影子图像(或称份额图像)。证明了这种秘密分享方案的(t,n)门限结构不仅是完全的而且也是理想的,并给出了提高像素灰度值域GF(2m)上图像秘密分享算法效率的"m位像素值的分拆与并行"方法。分析表明,该图像秘密分享方法可以应用于高安全等级的秘密图像的网络多路径传输、保密图像信息的分散式存储控制、高维图形码(Bar-code in k dimension)和弹出码(Popcode)等新一代信息载体技术的识读控制等各方面。
