To fully utilize the advances in quantum computing, it is critical to develop verification techniques that can scale and ensure the design of reliable and error-free quantum circuits. In this work, we propose a formal verification approach for a popular subset of quantum walk circuits, which are those that traverse cycles. Quantum walks are the quantum mechanical analog of random walks and as such have many safety- critical and security-critical applications. The proposed approach incorporates abstractions for quantum gates used in quantum walk circuits and correctness properties. Experimental results demonstrated that the verification approach is very efficient and is able to scale up to quantum walk circuits with as many as 5,000 qubits.

Sleep Convention Logic (SCL) is an emerging ultra-low power Quasi-Delay Insensitive (QDI) asynchronous design paradigm with enormous potential for industrial applications. Design validation is a critical concern before commercialization. Unlike other QDI paradigms, such as NULL Convention Logic (NCL) and Pre-Charge Half Buffers (PCHB), there exists no formal verification methods for SCL. In this paper, we propose a unified formal verification scheme for combinational as well as sequential SCL circuits, based on equivalence checking, which verifies both safety and liveness. The method is demonstrated using several multipliers, MACs, and ISCAS benchmarks.

Precharge half buffer (PCHB) is one of the major quasi-delay insensitive (QDI) asynchronous design paradigms, which has been utilized in several commercial applications due to its low power and inherent robustness. In industry, QDI circuits are often synthesized from a synchronous specification using custom synthesis tools. Design validation of the implemented QDI circuits mostly relies on extensive simulation, which may fail to detect corner-case bugs, especially in complex designs. Hence, a formal verification scheme for PCHB circuits is much needed. In this article, we present a formal verification methodology for PCHB circuits synthesized from a Boolean/synchronous specification, which is based on equivalence checking and can guarantee both safety (full functional correctness) and liveness (absence of deadlock). The approach is fast, scalable, and applicable to combinational as well as sequential PCHB circuits. We demonstrate the method using several multipliers, multiply and accumulate circuits (MACs), and IEEE International Symposium on Circuits and Systems (ISCAS) benchmarks.

NULL Convention Logic (NCL) circuits are asynchronous circuits and find application in SoC design due to their delay-insensitive nature, which allows ease in resolution of timing issues in IP component reuse for SoC. NCL components are typically synthesized from synchronous circuits. For any design paradigm to be feasible, verification is an important factor. We present a formal verification methodology for checking equivalence of NCL circuits against their synchronous parent circuits. The methodology includes a procedure that computes the reachable states of NCL sequential circuits and a refinement mapping function that can be used to map NCL circuit states onto synchronous circuit states. The methodology is demonstrated by verifying the correctness of several NCL circuits.

Virtualization is a key aspect to achieve scalability and flexibility in a cloud. Many solutions have been proposed to monitor and deploy Virtual Machines (VM) in resource pool of cloud. However, most of the cloud management systems, such as Amazon EC2 are proprietary. In the said perspective, many open source VM-based platforms have tossed for general users to research. The existing work has mainly focused on the discussion of architecture, feature-set, and performance analysis. Other important aspects, such as formal analysis, modeling, and verification are usually ignored. In this paper, we provide formal analysis, modeling, and verification of three open source state-of-the-art VM-based cloud platforms: (a) Eucalyptus, (b) Open Nebula, and (c) Nimbus. We used High-Level Petri Nets (HLPN) to model and analyze the structural and behavioral properties of the systems. Moreover, to verify the models, we have used Satisfiability Modulo Theories Library (SMT-Lib) and Z3 Solver. We modeled about 100 VM to verify the correctness and feasibility of our models. The results reveal that the models are functioning correctly. Moreover, the increase in the number of VM does not affect the working of the models that indicates the practicability of the models in a highly scalable and flexible environment.

Modifications of arithmetic coding (AC) have been proposed to improve the security of traditional AC. Two main modifications to AC are randomized AC (RAC) and AC with key-based interval splitting (KSAC). Chosen-plaintext attacks have been proposed for these two methods when the same key is used to encrypt different messages. We first give a definition for security of encryption using AC that is based on the inability of the adversary to distinguish between the encryption of one plaintext from the encryption of another. Using this definition, we prove that RAC is insecure even if a new random key is used to compress every message. Our proof assumes that the adversary can only eavesdrop on the ciphertext and cannot request encryptions of chosen-plaintexts. We then prove that the method of first-compress-then-encrypt, where the encryption is performed by a bitwise xor of the compressed output with a pseudorandom bit sequence, is provably secure with respect to chosen-plaintext attacks. If the pseudorandom bit sequence is derived in advance using Advanced Encryption Standard (AES) in the counter mode, then the first-compress-then-encrypt method results in a performance penalty of only a few two input xor-gate delays.

We consider the problem of joint optimal placement of Phasor Measurement Units (PMU) and conventional measurements to ensure full observability in power systems. The problem is first formulated as a nonlinear integer programming problem and then recast in to an equivalent integer linear programming (ILP) problem by introducing auxiliary variables and constraints. The ensuing ILP problem is solved for the IEEE 14, 57 and 118 bus systems considering zero-injection buses. The results provide a far more economical solution to system observability compared to those obtained solely with PMU placement.

We show how to automatically verify pipelined machines with out-of-order execution using refinement. Our notion of refinement is based on Well-Founded Equivalence Bisimulations. Proving refinement guarantees that a pipelined machine will preserve all safety and liveness properties of its instruction set architecture. Checking liveness-used to ensure that deadlocks do not occur, i.e., there is always forward progress-is essential for out-of-order machines as the control logic is involved and prone to deadlock defects. In previous work on out-of-order verification, liveness checking was either ignored or not automated. We developed two automatic methods based on refinement that check both safety and liveness of out-of-order pipelined machines. We use extensive experimentation based on 14 out-of-order machine models to study and compare these methods. We find overall that the cost of proving both safety and liveness is about 81 percent more than the cost of proving safety alone.

In this paper we propose a new linear congruential generator (LCG) based pseudo random bit-sequence generator (PRBG) and its hardware implementation. Linear congruential generators (LCGs) of the form xi+1= axi+ b(mod m), have been used to generate pseudorandom numbers. However these generators have been known to be insecure. The proposed PRBG couples four such LCGs and is secure. A preliminary proof of security is outlined in this paper. The PRBG generates bit-sequences that pass all NIST pseudo randomness tests. Our PRBG has a very efficient hardware implementation because the modulo operation is with respect to 2nas opposed to p times q in the blum-blum-shub (BBS) generator, where p and q are large prime numbers. We also show that the hardware implementation can be easily pipelined, thereby increasing the throughput in spite of the hardware having large word-length inputs (n ges 128). A 4-stage pipelined hardware was implemented in VHDL for n = 128 and the synthesized hardware was simulated. Simulation results showed a 2.81 fold increase in throughput (number of pseudo-random bits output per unit time) compared to the non-pipelined version.

Desynchronization is a method used to synthesize circuits with a high degree of asynchronicity from synchronous parents. It is well known that asynchronous circuits are hard to design and verify. We propose a refinement-based formal method to check that desynchronized pipelines correctly implement their high-level non-pipelined specifications. The method is based on an algorithm to construct functions that relate desynchronized states with specification states. The method is used successfully to check partial safety of a desynchronized implementation of the DLX architecture.

We show how to automatically verify that complex pipelined machine models satisfy the same safety and liveness properties as their instruction-set architecture (ISA) models by using well-founded equivalence bisimulation (WEB) refinement. We show how to reduce WEB-refinement proof obligations to formulas expressible in the decidable logic of counter arithmetic with lambda expressions and uninterpreted functions (CLU). This allows us to automate the verification of the pipelined machine models by using the UCLID decision procedure to transform CLU formulas to Boolean satisfiability problems. To relate pipelined machine states to ISA states, we use the commitment and flushing refinement maps. We evaluate our work using 17 pipelined machine models that contain various features, including deep pipelines, precise exceptions, branch prediction, interrupts, and instruction queues. Our experimental results show that the overhead of proving liveness, obtained by comparing the cost of proving both safety and liveness with the cost of only proving safety, is about 17%, but depends on the refinement map used; for example, the liveness overhead is 23% when flushing is used and is negligible when commitment is used.

We present a refinement-based compositional framework for showing that pipelined machines satisfy the same safety and liveness properties as their non-pipelined specifications. Our framework consists of a set of convenient, easily applicable, and complete compositional proof rules. We show how to apply our compositional framework in the context of microprocessor verification to verify both abstract, term-level models and executable, bit-level models. Our framework enables us to verify machine models that are significantly more complex than the kinds of models that can be verified using current state-of-the-art automated decision procedures. For example, using our framework, we can verify a 32-bit, 10-stage, executable pipelined machine model. In addition, our compositional framework offers drastic improvements in the context of design debugging over monolithic approaches, in part because bugs are isolated to particular steps in the compositional proof and because the counter examples generated are much smaller.

We introduce collapsed flushing, a new flushing-based refinement map for automatically verifying safety and liveness properties of term-level pipelined machine models. We also present a new method for handling liveness that is both simpler to define and easier to verify than previous approaches. To empirically validate collapsed flushing, we ran extensive experiments which show more than an order-of-magnitude improvement in verification times over standard flushing. Furthermore, by combining collapsed flushing with commitment refinement maps, we can monolithically verify complex pipelined machine models with deep pipelines - a salient feature of state-of-the-art microprocessor designs - that previous approaches cannot handle

We present several techniques for automatically reducing memories in RTL designs. This includes a new memory abstraction algorithm that allows us to greatly reduce the size of memories and a technique based on-term rewriting that further improves the abstraction. In contrast to previously proposed methods for abstracting memories of RTL designs, our methods are general---e.g., they allow us to arbitrarily and directly compare memories---and they are sound and complete---e.g., there are no false positives or negatives. In addition, the combination of our techniques allows us to automatically verify RTL pipelined machine designs beyond the reach of current state-of-the-art methods, as our experimental results show.

While most of the effort in improving verification times for pipelined machine verification has focused on faster decision procedures, we show that the refinement maps used also have a drastic impact on verification times. We introduce a new class of refinement maps for pipelined machine verification, and using the state-of-the-art verification tools UCLID and Siege we show that one can attain several orders of magnitude improvements in verification times over the standard flushing-based refinement maps, even enabling the verification of machines that are too complex to otherwise automatically verify.

We show how to verify pipelined machine models with bit-level interfaces by using a combination of deductive reasoning and decision procedures. While decision procedures such as those implemented in UCLID can be used to verify pipelined machines, the models are at the term level: they abstract away the datapath, require the use of numerous abstractions, implement a small subset of the instruction set, and are far from executable. In contrast, we focus on verifying executable machines with bit-level interfaces. Such proofs have previously required substantial expert guidance and the use of deductive reasoning engines. We show that by integrating UCLID with the ACL2 theorem proving system, we can use ACL2 to reduce the proof that an executable, bit-level machine refines its instruction set architecture to a proof that a term level abstraction of the bit-level machine refines the instruction set architecture, which is then handled automatically by UCLID. In this way, we exploit the strengths of ACL2 and UCLID to prove theorems that are not possible to even state using UCLID and that would require prohibitively more effort using just ACL2.

We present a compositional reasoning framework based on refinement for verifying that pipelined machines satisfy the same safety and liveness properties as their instruction set architectures. Our framework consists of a set of convenient, easily-applicable, and complete compositional proof rules. We show that our framework greatly extends the applicability of decision procedures by verifying a complex, deeply pipelined machine that state-of-the-art tools cannot currently handle. We discuss how our framework can be added to the design cycle and highlight what arguably is the most important benefit of our approach over current methods, that the counterexamples generated are much simpler, as bugs are isolated to a particular step in the composition proof.

We introduce a new method of automating the verification of term-level pipelined machine models that is based on commitment refinement maps. Our method is much simpler to implement than current alternatives. More importantly, as our extensive experiments show, our method leads to more than a 30-fold improvement in verification times over the standard approaches to pipeline machine verification, which use refinement maps based on flushing and commitment. In addition, we can verify machines that are too complex to directly verify using flushing-based refinement maps

We show how to automatically verify that complex XScale-like pipelined machine models satisfy the same safety and liveness properties as their corresponding instruction set architecture models, by using the notion of well-founded equivalence bisimulation (WEB) refinement. Automation is achieved by reducing the WEB-refinement proof obligation to a formula in the logic of counter arithmetic with lambda expressions and uninterpreted functions (CLU). We use the tool UCLID to transform the resulting CLU formula into a Boolean formula, which is then checked with a SAT solver. The models we verify include features such as out of order completion, precise exceptions, branch prediction, and interrupts. We use two types of refinement maps. In one, flushing is used to map pipelined machine states to instruction set architecture states; in the other, we use the commitment approach, which is the dual of flushing, since partially completed instructions are invalidated. We present experimental results for all the machines modelled, including verification times. For our application, we found that the time spent proving liveness accounts for about 5% of the over-all verification time.

We present the formal verification of an Intel Xscale processor model. The Xscale is a superpipelined RISC processor with 7-stage integer, 8-stage memory, and variable-latency multiply-and-accumulate execution pipelines. The processor uses scoreboarding to track data dependencies, and implements both precise and imprecise exceptions. Such set of features had not been modeled and formally verified previously. The formal verification was done with an automatic tool flow that consists of the term-level symbolic simulator TLSim, the decision procedure EVC, and an efficient SAT-checker.