Recently, there has been a growing interest in leveraging Large Language Models for Verilog code generation. However, the current quality of the generated Verilog code remains suboptimal. This is largely due to the absence of well-defined, well-organized datasets with high-quality samples, as well as a lack of innovative fine-tuning methods and models specifically trained on Verilog. In this paper, we introduce a novel open-source dataset and a corresponding fine-tuning technique, which utilizes a multi-layered structure that we refer to as PyraNet. Our experiments demonstrate that employing the proposed dataset and fine-tuning approach leads to a more accurate fine-tuned model, producing syntactically and functionally correct Verilog code. The evaluation results show improvements by up-to 32.6% in comparison to the CodeLlama-7B baseline model and upto 16.7% in comparison to the state-of-the-art models using VerilogEval evaluation platform.

Modeling system-level behaviors of intricate System-on-Chip (SoC) designs is crucial for design analysis, testing, and validation. This paper presents an approach, AutoModel, to automatically inferring concise and abstract models from SoC communication traces, capturing the system-level protocols that govern co-ordinations among design blocks for various system functions. In this approach, a causality graph with annotations obtained from the SoC traces is constructed first. The annotated causality graph represents all potential causality relations among messages under consideration. Next, a constraint satisfaction problem is formulated from the causality graph, which is then solved by a satisfiability modulo theories (SMT) solver to find satisfying solutions. Finally, finite state models are extracted from the generated solutions, which can be used to explain and understand the input traces. The proposed approach is validated through experiments using synthetic traces obtained from simulating a transaction-level model of a multicore SoC design and traces collected from running real programs on a realistic multicore SoC modeled in gem5.

This article proposes a specification mining framework,FlowMiner, that automatically mines patterns from highly concurrent communication traces for system-on-chip (SoC) designs. It addresses the problem of the lack of comprehensive, accurate, and up-to-date specifications necessary to perform rigorous and thorough validation of complex SoC designs. The extracted patterns characterize how components of an SoC design communicate and coordinate with each other to realize various system functions. InFlowMiner, a set of inference rules and optimization techniques are presented to reduce mining complexity. Evaluation of this framework in several experiments shows promising results.

Concise and abstract models of system-level behaviors are invaluable in design analysis, testing, and validation. In this paper, we consider the problem of inferring models from communication traces of system-on-chip (SoC) designs. The traces capture communications among different blocks of a system design in terms of messages exchanged. The extracted models characterize the system-level communication protocols governing how blocks exchange messages, and coordinate with each other to realize various system functions. In this paper, the above problem is formulated as a constraint satisfaction problem, which is then fed to a satisfiability modulo theories (SMT) solver. The solutions returned by the SMT solver are used to extract the models that accept the input traces. In the experiments, we demonstrate the proposed approach with traces collected from a transaction-level simulation model of a multicore SoC design and a trace of a more detailed multicore SoC modeled in GEM5.

Stochastic model checking is a technique for analyzing systems that possess probabilistic characteristics. However, its scalability is limited as probabilistic models of real-world applications typically have very large or infinite state space. This paper presents a new infinite state CTMC model checker, STAMINA, with improved scalability. It uses a novel state space approximation method to reduce large and possibly infinite state CTMC models to finite state representations that are amenable to existing stochastic model checkers. It is integrated with a new property-guided state expansion approach that improves the analysis accuracy. Demonstration of the tool on several benchmark examples shows promising results in terms of analysis efficiency and accuracy compared with a state-of-the-art CTMC model checker that deploys a similar approximation method.

Security protocol verification using commonly-used model-checkers or symbolic protocol verifiers has several intrinsic limitations. Spin suffers the state explosion problem; Proverif may report false attacks. An alternative approach is to use Coq. However, the effort required to verify protocols in Coq is high for two main reasons: correct protocol and property specification is a non-trivial task, and security proofs lack automation. This work claims that (1) using Coq for verification of cryptographic protocols can sometimes yield better results than Spin and Proverif, and (2) the verification process in Coq can be greatly alleviated if specification and proof engineering techniques are applied. Our approach is evaluated by verifying several representative case studies. Preliminary results are encouraging, we were able to verify two protocols that give imprecise results in Spin and Proverif, respectively. Further, we have automated proofs of secrecy and authentication for an important class of protocols.

Reconstructing system-level behavior from silicon traces is a critical problem in post-silicon validation of System-on-Chip designs. Current industrial practice in this area is primarily manual, depending on collaborative insights of the architects, designers, and validators. This paper presents a trace analysis approach that exploits architectural models of system-level protocols to reconstruct design behavior from partially observed silicon traces in the presence of ambiguous and noisy data. The output of the approach is a set of all potential interpretations of a system's internal execution abstracted to system-level protocols. To support the trace analysis approach, a companion trace signal selection framework guided by system-level protocols is also presented, and its impacts on the complexity and accuracy of the analysis approach are discussed. That approach and the framework have been evaluated on a multi-core System-on-Chip prototype that implements a set of common industrial system-level protocols.

This paper presents a compositional framework to address the state explosion problem in model checking of concurrent systems. This framework takes as input a system model described as a network of communicating components in a high-level description language, finds the local state transition models for each individual component where local properties can be verified, and then iteratively reduces and composes the component state transition models to form a reduced global model for the entire system where global safety properties can be verified. The state space reductions used in this framework result in a reduced model that contains the exact same set of observably equivalent executions as in the original model, therefore, no false counter-examples result from the verification of the reduced model. This approach allows designs that cannot be handled monolithically or with partial-order reduction to be verified without difficulty. The experimental results show significant scale-up of this compositional verification framework on a number of non-trivial concurrent system models.

Local state space construction is crucial for efficient compositional verification of local and global properties of concurrent systems. This paper presents such an approach where local state transition models are built by iteratively searching the joint state space of communicating processes. The resulting local models contain less unreachable states, which would reduce false counter-examples for verifying local safety properties. Alternatively, more precise transition dependence relations can be extracted from these local models for more effective partial order reduction when the global state space is searched. The prototype of this approach has been implemented in an explicit model checker, and experimented on several concurrent examples. The initial results are encouraging.

This paper presents an approach to more efficient partial order reduction for explicit model checking of concurrent systems. This approach utilizes a compositional reachability analysis to generate overapproximate local state transition models for all components in a concurrent system where a dependence relation and other useful information can be extracted. The extracted dependence relation, compared to what can be obtained by statically analyzing the system descriptions, is more precise and refined, and therefore leads to more efficient partial order reduction. This approach is demonstrated on a set of concurrent system examples. Significantly higher reduction in state space has been observed in the majority of the examples compared to what can be obtained with SPIN.

Divide-and-conquer is essential to address state explosion in model checking. Verifying each individual component in a system, in isolation, efficiently requires an appropriate context, which traditionally is obtained by hand. This paper presents an efficient modular model checking approach for asynchronous design verification. It is equipped with a novel abstraction refinement method that can refine a component abstraction to be accurate enough for successful verification. It is fully automated, and eliminates the need of finding an accurate context when verifying each individual component, although such a context is still highly desirable. This method is also enhanced with additional state space reduction techniques. The experiments on several nontrivial asynchronous designs show that this method efficiently removes impossible behaviors from each component including ones violating correctness requirements.

Compositional verification is essential for verifying large systems. However, approximate environments are needed when verifying the constituent modules in a system. Effective compositional verification requires finding a simple but accurate overapproximate environment for each module. Otherwise, many verification failures may be produced, therefore incurring high computational penalty for distinguishing the false failures from the real ones. This paper presents an automated method to refine the state space of each module within an overapproximate environment. This method is sound as long as an overapproximate environment is found for each module at the beginning of the verification process, and it has less restrictions on system partitioning. It is also coupled with several state-space reduction techniques for better results. Experiments of this method on several large asynchronous designs show promising results.

This paper presents a compositional method with failure-preserving abstraction for scalable asynchronous design verification. It combines efficient state-space reductions and novel interface refinement and can dramatically reduce the complexity of state space while decreasing the introduction of false failures. This allows much larger designs to be verified as demonstrated in the experimental results.

This paper presents a method to address state explosion in timed-circuit verification by using abstraction directed by the failure model. This method allows us to decompose the verification problem into a set of subproblems, each of which proves that a specific failure condition does not occur. To each subproblem, abstraction is applied using safe transformations to reduce the complexity of verification. The abstraction preserves all essential behaviors conservatively for the specific failure model in the concrete description. Therefore, no violations of the given failure model are missed when only the abstract description is analyzed. An algorithm is also shown to examine the abstract error trace to either find a concrete error trace or report that it is a false negative. This paper presents results using the proposed failure-directed abstractions as applied to several large timed-circuit designs.

We study the simultaneous switching noise(SSN) generated by the digital I/O buffers and its impact on VCO. A simple yet accurate model is developed to analyze the ground bounce and power supply fluctuation in each region respectively. Calculation results with the models show good agreements with HSPICE simulation results. Based on the noise model, we investigate the SSN effects on the timing jitter of a current starved VCO. In this study, the RMS jitter and jittery signal spectrum are characterized.

We present a method to address state explosion in timed circuit verification by using abstraction directed by the failure model. This method allows us to decompose the verification problem into a set of subproblems, each of which proves that a specific failure condition does not occur. To each subproblem, abstraction is applied using safe transformations to reduce the complexity of verification. The abstraction preserves all essential behaviors conservatively for the specific failure model in the concrete description. Therefore, no violations of the given failure model are missed when only the abstract description is analyzed. An algorithm is also shown to examine the abstract error trace to either find a concrete error trace or report that it is a false negative. We present results using the proposed failure directed abstractions as applied to two large timed circuit designs.

The major barrier that prevents the application of formal verification to large designs is state explosion. This paper presents a new approach for verification of timed circuits using automatic abstraction. This approach partitions the design into modules, each with constrained complexity. Before verification is applied to each individual module, irrelevant information to the behavior of the selected module is abstracted away. This approach converts a verification problem with big exponential complexity to a set of subproblems, each with small exponential complexity. Experimental results are promising in that they indicate that our approach has the potential of completing much faster while using less memory than traditional flat analysis.

In order to continue to produce circuits of increasing speeds, designers must consider aggressive circuit design styles such as self-resetting or delayed-reset domino circuits used in IBM's gigahertz processor (GUTS) and asynchronous circuits used in Intel's RAPPID instruction length decoder. These new timed circuit styles, however, cannot be efficiently and accurately analyzed using traditional static timing analysis methods. This lack of efficient analysis tools is one of the reasons for the lack of mainstream acceptance of these design styles. This paper discusses several industrial timed circuits and gives an overview of our timed circuit design methodology.

Describes a new method for the architectural synthesis of timed asynchronous systems. Due to the variable delays associated with asynchronous resources, implicit schedules are created by the addition of supplementary constraints between resources. Since the number of schedules grows exponentially with respect to the size of the given data flow graph, pruning techniques are introduced which dramatically improve the run-time without significantly affecting the quality of the results. Using a combination of data and resource constraints, as well as an analysis of bounded delay information, our method determines the minimum number of resources and registers needed to implement a given schedule. Results are demonstrated using some high-level synthesis benchmark circuits and an industrial example.

We present an efficient asynchronous VLSI architecture for calculating running maximum or minimum values over a sliding window. Running maximums or minimums are very useful for many signal and image processing tasks. Our architecture performs the calculation using the MAXLIST algorithm. In order to take advantage of the wide delay variations due to data-dependencies and operating conditions, an asynchronous approach is taken to achieve higher performance and lower power. Simulation results demonstrate that our asynchronous architecture is significantly faster than existing and potential synchronous architectures.