With the successful application of hardware agile design methodology, it has become a big challenge to optimize the design in novelly defined intermediate representations (IR), such as FIRRTL. However, there is little work focusing on this challenge, or the optimization tasks are left to logic synthesizers by translating IRs into designs in hardware description languages (HDL).

Dynamic verification method is still the most easily accessible and thus heavily used verification approach for System-on-Chip (SoC) designs. Assertions are widely used in dynamic verification for functional coverage analysis. At present, how to generate tests to effectively cover assertions defined over internal signals is still a challenge for dynamic verification. In this paper, we propose a novel test generation method to accelerate assertion coverage using surrogate logic model. A surrogate logic model is used to represent an approximate relationship between an internal signal and related input signals, which is derived from simulation results by using machine learning technology. With surrogate logic model, we transfer the test generation for assertion coverage problem to a random sampling problem and solve it by the state-of-the-art sampling techniques. Experimental results on diverse benchmarks demonstrate that the proposed method could accelerate assertions coverage in two aspects, one is covering an assertion as quick as possible and the other is covering an assertion more times in a given period.

Recently, hardware agile design methods have been developed to improve the design productivity. However, the mod-eling methods hinder further design productivity improvements. In this paper, we propose and implement a microprocessor agile design method using feature oriented programming technology to improve design productivity. In this method, designs could be uniquely partitioned and constructed incrementally to explore various functional design features flexibly and efficiently. The key techniques to improve design productivity are flexible modeling extension and on-the-fly feature composing mechanisms. The evaluations on RISC- V and OR1200 CPU pipelines show the effectiveness of the proposed method on duplicate codes reduction and flexible feature composing while avoiding design resource overheads.

With the ending of Moore's Law and Dennard scaling, modern System-on-a-Chip (SoC) trends to incorporate a large and growing number of specialized modules for specific applications. Verification is vital to the RTL design and faces new challenges due to the growing design complexities. In this paper, we proposed a symbolic simulation enhanced coverage- directed dynamic verification technique for RTL designs. We proposed novel Full Multiplexer Toggle Coverage (FMTC) to trace and provide feedback to the verification process. The proposed method is a hybrid between symbolic simulation and mutation based fuzz testing that offsets the disadvantages of both. The achievement of high coverage is obtained by interleaved symbolic simulation and fuzz testing passes. The symbolic simulation pass is used to generate tests that direct the testing to untouched corners. While the mutation based fuzz testing pass is used to leverage test generation tasks and to enable the method to deal with large scale designs. The empirical evaluation of the method shows promising results on archiving high coverage for practical designs.

This paper focused on the safety verification of the multithreaded programs for mobile crowdsourcing networks. A novel algorithm was proposed to find a way to apply IC3, which is typically the fastest algorithm for SAT‐based finite state model checking, in a very clever manner to solve the safety problem of multithreaded programs. By computing a series of overapproximation reachability, the safety properties can be verified by the SAT‐based model checking algorithms. The results show that the new algorithm outperforms all the recently published works, especially on memory consumption (an advantage that comes from IC3).

Scalability of cache coherence protocol is a key component in future shared-memory multi-core or multi-processor systems. The state space explosion is the first hurdle while applying model-checking to scalable protocols. In order to validate parameterized cache coherence protocols effectively, we present a new method of reducing the state space of parameterized systems, two-dimensional abstraction (TDA). Drawing inspiration from the design principle of parameterized systems, an abstract model of an unbounded system is constructed out of finite states. The mathematical principles underlying TDA is presented. Theoretical reasoning demonstrates that TDA is correct and sound. An example of parameterized cache coherence protocol based on MESI illustrates how to produce a much smaller abstract model by TDA. We also demonstrate the power of our method by applying it to various well-known classes of protocols. During the development of TH-1A supercomputer system, TDA was used to verify the coherence protocol in FT-1000 CPU and showed the potential advantages in reducing the verification complexity.

Functional verification is widely recognized as the bottleneck of the hardware design cycle. The coverage-driven verification approach makes coverage the core engine that drives the whole verification flow, which enables reaching high quality verification in a timely manner. In this paper, we present a coverage driven test generation methodology and a set of tools. We present a novel method for automatic generating simulation vectors from HDL descriptions based on path coverage and constraint solving. We present a novel approach to generate functional vectors based on assertions for RTL design verification. Our approach combines program-slicing based design extraction, word-level SAT and dynamic searching techniques. We also present a coverage analysis method based on VCD file, which only replaying the simulation of the control statements in the HDL description. Experimental results show the efficiency of our methodology.