This paper presents a method for automatic rectification of design bugs in processors. Given a golden sequential instruction-set architecture model of a processor and its erroneous detailed cycle-accurate model at the micro-architecture level, we perform symbolic simulation and property checking combined with concrete simulation iteratively to detect the buggy location and its corresponding fix. We have used the truth-table model of the function that is required for correction, which is a very general model. Moreover, we do not represent the truth-table explicitly in the design. We use, instead, only the required minterms, which are obtained from the output of our backend formal engine. This way, we avoid adding any new variable for representing the truth-table. Therefore, our correction model is scalable to the number of inputs of the truth-table that could grow exponentially. We have shown the effectiveness of our method on a complex out-of-order superscalar processor supporting atomic execution of instructions. Our method reduces the model size for correction by 6.0x and total correction time by 12.6x, on average, compared to our previous work.

This paper introduces methods to modify a buggy sequential gate-level circuit to conform to the specification. In order to preserve the optimization efforts, the modifications should be as small as possible. Assuming that the locations to be modified are given, our proposed method finds an appropriate set of fan-in signals for the patch function of those locations by iteratively calculating the state correspondence between the specification and the buggy circuit and applying a method for debugging combinational circuits. The experiments are conducted on ITC99 benchmark circuits, and it is shown that our proposed method can work when there are at most 30,000 corresponding reachable state pairs between two circuits. Moreover, a heuristic method using the information of data-path FFs is proposed, which can find a correct set of fan-ins for all the benchmark circuits within practical time.

This paper presents a new approach for circuit matching using signatures. We have defined a signature based on topology of the fanin cones of the circuit elements. Given two circuits, first we find all the circuit elements with unique signature between the two input circuits. After that, we try to expand the matching area by our expansion rules as much as possible. We iteratively find the unique matches and expand the matching area until no further matching is possible. Our experiments on IWLS2005 benchmark suite show that our method is able to find the perfect matching between two 160,000-gate IP in 5 minutes. In addition, our method is more than one order of magnitude faster than our previous signature-based matching method, while the size of the matched area is comparable or larger.

In this paper, we have addressed the problem of ordering transactions in network-on-chips (NoCs) for post-silicon validation. The main idea is to extract the order of the transactions from the local partial orders in each NoC tile based on a set of “happened-before” rules, assuming transactions do not have a timestamp. The assumption is based on the fact that implementation and usage of a global time as timestamp in such systems may not be practical or efficient. When a new transaction is received in a tile, we send special messages to the neighboring tiles to inform them regarding the new transaction. The process of sending those special messages continues recursively in all the tiles that receive them until another such special message is detected. This way, we relate local orders of different tiles with each other. We show that our method can reconstruct the correct transaction orders when communication delays are deterministic. We have shown the effectiveness of our method by correctly ordering the transaction in NoCs with mesh and torus topologies with different sizes from 5*5 to 9*9. Also, we have implemented the proposed method in hardware to show its feasibility.

In the process of VLSI design, ECO (Engineering Change Order) may occur at any design phase. When ECO happens after the netlist is generated and optimized, designers may like to modify the netlist directly. This is because if ECO is performed in the high-level description, the netlist should be resynthesized and the result may be significantly different from the original one, even if the modification in the high-level description is small. As the result, the efforts spent on optimization so far may become useless. When the netlist is modified directly, the C description should be revised accordingly. This paper proposes a method to reconstruct a C description from the revised netlist. In the proposed method, designers need to provide a template represented in C, which has some vacant (blanked) places and is created from the original C description. The vacant places are automatically synthesized using a CEGIS-based method (Counter Example Guided Inductive Synthesis). Using a set of use-cases, our method tries to find the correct expressions for the vacant places so that the entire description becomes functionally equivalent to the given modified netlist, by only simulating the netlist. Experimental results show that the proposed method can reconstruct C descriptions successfully within practical time for several examples including the one having around 9,000 lines of executable statements. Moreover, the proposed method can be applied to equivalence checking between a netlist and a C description, as shown by our experimental results.