Success of simulation-based functional verification depends on the quality and diversity of the verification tests that are simulated. The objective of test generation methods is to generate tests that exercise as much different functionality of the hardware designs as possible. In this paper, we propose a novel methodology that generates a model of the verification tests in a given test set using unsupervised support vector analysis. One potential application is to use this model to select tests that are likely to exercise functionality that has not been tested so far. Since this selection can be done before simulation, it can be used to filter redundant tests and reduce required simulation cycles. Our methodology can be combined with a test generation method like constrained-random test generation to increase its effectiveness without making fundamental changes to the verification flow. Experimental results based on application of the proposed methodology to the OpenSparc T1 processor are reported to demonstrate the practicality of our approach.

Extensive software-based simulation continues to be the mainstream methodology for functional verification of designs. To optimize the use of limited simulation resources, coverage metrics are essential to guide the development of effective test suites. Traditional coverage metrics are defined based on either a functional model or a structural model of the design. If our goal is to select a subset of tests from a set of tests, using these coverage metrics require simulation of the entire set before the effectiveness of tests can be compared. In this paper, we propose a novel methodology that estimates the input space covered by a set of tests. We use unsupervised support vector analysis to learn such a space, resulting in a subset of tests that represent the original set of tests. A direct application of this methodology is to select tests before simulation in order to reduce simulation cycles. Consequently, simulation effectiveness can be improved. Experimental results based on application of the proposed methodology to the OpenSparc T1 processor are reported to demonstrate the practicality of our approach.

Assertion based verification encourages the insertion of many assertions into a design. Typically, not all assertions can be proven (or falsified). The indeterminate assertions require manual analysis in order to determine design correctness -- a time-consuming and error-prone process. This paper shows how automatic assume guarantee reasoning can be used to reduce the amount of manual analysis. We present algorithms to automatically compute the assume guarantee relations between assertions. We extend circular assume guarantee reasoning to compute more proofs. And, we show how automatic assume guarantee reasoning can be used in practice to reduce the number of indeterminate assertions requiring manual analysis. We present the results of applying our algorithms to large industrial designs.

A decision procedure for a theory of arrays is of interest for applications in formal verification, program analysis and automated theorem proving. This paper presents a decision procedure for an extensional theory of arrays and proves it correct.

Bit-v ector theories with concatenation and extraction have been shown to be useful and important for hardware verification. We have implemented an extended theory which includes arithmetic. Although deciding equality in suc h a theory is NP-hard, our implementation is efficient for many practical examples. We believ e this to be the first such implementation which is efficient, automatic, and complete.

We introduce a general, automatic verification technique for pipelined designs. The technique is based on a scalable, formal methodology for analysing pipelines. The key advantages to our technique are: it specifically targets pipeline control, making it more efficient; it requires no explicit specification, since it compares hardware against itself; it can be used within the broader framework of hierarchical verification; and, it can be easily extended to handle certain "complex" pipelined structures.

Article Free Access Share on A scalable formal verification methodology for pipelined microprocessors Authors: Jeremy Levitt Computer Systems Laboratory, Stanford University, CA Computer Systems Laboratory, Stanford University, CAView Profile , Kunle Olukotun Computer Systems Laboratory, Stanford University, CA Computer Systems Laboratory, Stanford University, CAView Profile Authors Info & Claims DAC '96: Proceedings of the 33rd annual Design Automation ConferenceJune 1996 Pages 558–563https://doi.org/10.1145/240518.240624Published:01 June 1996Publication History 15citation273DownloadsMetricsTotal Citations15Total Downloads273Last 12 Months24Last 6 weeks13 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF

Abstract—We present a new approach to event-driven simu-lation that does not use a centralized run-time event queue, yet is capable of handling arbitrary models, including those with unclocked feedback and nonunit delay. The elimination of the event queue significantly reduces run-time overhead, resulting in faster simulation. We have implemented our algorithm in a pro-totype Verilog simulator called VeriSUIF. Using this simulator we demonstrate improved performance vs. a commercial simulator on a small set of programs. I.