The Infona portal uses cookies, i.e. strings of text saved by a browser on the user's device. The portal can access those files and use them to remember the user's data, such as their chosen settings (screen view, interface language, etc.), or their login data. By using the Infona portal the user accepts automatic saving and using this information for portal operation purposes. More information on the subject can be found in the Privacy Policy and Terms of Service. By closing this window the user confirms that they have read the information on cookie usage, and they accept the privacy policy and the way cookies are used by the portal. You can change the cookie settings in your browser.
We present a method for exploiting symmetry-breaking constraints in modular schemes for constructing equivalent Boolean encodings of cardinality constraints. These techniques result in speedup in automated debugging of complex VLIW processors in formal verification by Correspondence Checking and efficient translation to Boolean Satisfiability (SAT).
We study the efficient formal verification of polymorphic heterogeneous multi-core architectures, such as Bahurupi, and also present insights on how to design such architectures at a high level of abstraction in order to facilitates their formal verification. To the best of our knowledge, this is the first work on formal verification of such architectures.
We present parallel algorithms for Binary Decision Diagram (BDD) manipulation optimized for efficient execution on Graphics Processing Units (GPUs). Compared to a sequential CPU-based BDD package with the same capabilities, our GPU implementation achieves at least 5 orders of magnitude speedup. To the best of our knowledge, this is the first work on using GPUs to accelerate a BDD package.
We propose a novel method for error diagnosis of pipelined microprocessors that allows us to exploit Positive Equality in Correspondence Checking. We also present static CNF variable ordering heuristics that dramatically reduce the solution space during the debugging. Experimental results indicate speedup of up to 2 orders of magnitude relative to previous approaches when applying the method to automated...
We present highly automatic techniques for formal verification of pipelined microprocessors with hardware support for multithreading. The processors are modeled at a high level of abstraction, using a subset of Verilog, in a way that allows us to exploit the property of Positive Equality that results in significant simplifications of the solution space, and orders of magnitude speedup relative to...
We present a method for automatic formal verification of Digital Signal Processors (DSPs) that have VLIW architecture and reconfigurable functional units optimized for accelerating Software Defined Radio (SDR) applications to be used for future space communications by NASA. The formal verification was done with the highly automatic method of Correspondence Checking by exploiting the property of Positive...
Presented is a method for debugging of pipelined processors in their formal verification with the highly automatic and scalable approach of Correspondence Checking, where a pipelined/superscalar/VLIW implementation is compared against a non-pipelined specification via an inductive correctness criterion based on symbolic simulation in a way that guarantees the correctness of the implementation for...
With the number of processor cores in modern CPUs growing exponentially, it is expected that CPUs will have on the order of a hundred cores in the next 5 - 7 years. Thus, the need to implement parallel SMT decision procedures to utilize the increasing number of cores. We study a method to design independent strategies for a portfolio of parallel independent strategies in an SMT decision procedure...
Set the date range to filter the displayed results. You can set a starting date, ending date or both. You can enter the dates manually or choose them from the calendar.