Sequence-Based Incremental Concolic Testing of RTL Models

TL;DR

This paper introduces an incremental concolic testing method for RTL models that effectively covers complex corner cases by treating hard-to-activate branches as sequences of easier events, improving test coverage.

Contribution

It presents a novel sequence-based incremental concolic testing algorithm that enhances coverage of complex branches in hardware models, outperforming existing methods.

Findings

Successfully covers complex corner cases in RTL models.

Outperforms state-of-the-art methods in activating hard-to-reach branches.

Demonstrates effectiveness through experimental validation.

Abstract

Concolic testing is a scalable solution for automated generation of directed tests for validation of hardware designs. Unfortunately, concolic testing also fails to cover complex corner cases such as hard-to-activate branches. In this paper, we propose an incremental concolic testing technique to cover hard-to-activate branches in register-transfer level models. We show that a complex branch condition can be viewed as a sequence of easy-to-activate events. We map the branch coverage problem to the coverage of a sequence of events. We propose an efficient algorithm to cover the sequence of events using concolic testing. Specifically, the test generated to activate the current event is used as the starting point to activate the next event in the sequence. Experimental results demonstrate that our approach can be used to generate directed tests to cover complex corner cases while state-of-the-art methods fail to activate them.

Tables

Table 1. TABLE I : Comparison of system-level target activation using [ 14 ] , [ 4 ] , and our approach

Cases	Unroll Cycles (Bound)	EBMC [14]			Concolic [4]			Our Approach
		Activated	Memory  (MB)	Time (s)	Activated	Memory  (MB)	Time (s)	Activated	Memory (MB)	Time (s)
1	20	No	-	-	Yes	82.34	20.13	Yes	20.00	14.55
2	20	No	-	-	No	-	-	Yes	34.67	25.78
3	50	No	-	-	Yes	215.84	50.67	Yes	67.89	20.78
4	50	No	-	-	No	-	-	Yes	182.56	82.91
5	20	No	-	-	No	-	-	Yes	19.78	14.43
6	20	No	-	-	No	-	-	Yes	30.24	23.91
7	20	Yes	597.81	2.01	Yes	20.56	4.93	Yes	15.23	4.81
8	20	No	-	-	No	-	-	Yes	45.89	25.89

Table 2. TABLE II: Memory(MB) and time(s) taken to verify Case 2.

Unroll cycles	Concolic [4]			Our Approach
	Activated	Mem	Time	Activated	Mem	Time
10	No	52.4	29.92	Yes	10.9	0.59
20	No	86.3	70.59	Yes	11.4	1.75
30	No	121.2	137.25	Yes	12.9	7.09
40	No	154.8	225.37	Yes	12.1	6.22
50	Yes	164.6	286.09	Yes	13.1	11.75

Full text

I Introduction

Functional validation is a major bottleneck for modern System-on-Chip (SoC) designs. According to the Wilson Research 2020 functional verification study [1], more than 50% of development time in hardware designs were spent in verification. Simulation is the most widely used form of functional validation. Even millions of random tests may not be able to activate complex corner cases such as hard-to-detect branches in Register-Transfer Level (RTL) designs. As a result, it is unlikely to achieve 100% functional coverage using random or constrained-random tests for industrial designs. To improve the coverage, verification engineers typically write manual tests to cover the remaining functional scenarios. Manual test writing can be cumbersome and error-prone. There is a critical need for automated generation of directed tests.

Concolic testing has been successfully used as a directed test generation method in both software [2, 3] and hardware domains [4]. Figure 1 shows an overview of the concolic testing framework. The design is instrumented so that the tool can identify the executed path during simulation. Next, the instrumented design is simulated using an initial vector. The initial test vector can be generated using random or any other test generation methods. The execution path of the design is identified by analyzing the simulation trace. Next, an alternate path is selected by negating one of the branch constraints. The path constraints to activate the selected branch (alternate branch) will be sent to a constraint solver. Constraint solver will produce a solution if the constraints are satisfiable. This solution is used to generate a new test vector to activate the selected branch. If the constraint solver cannot solve the constraints (solution is unsatisfiable), an alternate branch is selected. This process continues until the expected coverage is achieved. Since concolic testing explores one path at a time, it overcomes the state space exploration problem. However, concolic testing faces the path exploration problem due to the exponential number of possible paths to explore. Path exploration problem can be mitigated by using a profitable alternate branch selection approach.

Alternate branch selection depends on the coverage goal. Existing approaches try to maximize the overall coverage [5] as well as specific branch targets [4, 6]. In this paper, we are considering activation of corner cases which are hard-to-activate. Some branches become hard-to-activate due to the complex temporal dependencies that should be preserved in-order to activate that branch. Consider line 36 in Listing 1 that reads a value ($r\_data$) from a specific memory address ($addr)$. For this condition to be true, a write should happen to that specific memory address with the exact values. The read can only happen when read flag ($r\_en$) is true and write flag ($w\_en$) is false. However, write can only proceed when read flag ($r\_en$) is false and write flag ($w\_en$) is true. These are contradictory constraints that must be satisfied in-order to activate the branch. Existing concolic testing [4] fails unless the design is sufficiently unrolled in such cases. Unrolling for a large number of cycles is not feasible for large designs.

In this paper, we propose a sequence-based incremental concolic testing. Our proposed technique uses edge exploration by traversing the Control Flow Graph (CFG) of the RTL design to identify the event sequence. Next, it solves each sequence while maintaining the order and preserving each solution for solving the next sequence incrementally. This paper makes the following three major contributions.

Proposes an event sequence based approach for concolic testing. For a given branch, the sequence of events is identified by statically analyzing the concurrent CFGs of the RTL design. 2. 2.

Incrementally applies concolic testing on an event sequence and preserves the test vectors to build the directed test to activate the target (corner case). 3. 3.

Extensive experimental evaluation using a memory design demonstrates the effectiveness of our approach.

II Related Work

Concolic testing is a promising alternative to model checking based test generation. Specifically, it provides an effective combination of concrete simulation and symbolic execution [4]. Unlike model checking that tries to explore all possible (exponential) execution paths at the same time, concolic testing explores only one execution path at a time. Concolic testing has been successfully applied on both software [2, 3, 7, 8] and hardware designs [9, 10, 4]. Although concolic testing can avoid state explosion problem, it faces path explosion problem since it needs to select a profitable path is each iteration. While there are promising solutions for selecting beneficial branches [4], they are not suitable for complex corner cases such as hard-to-detect branches with complex branch conditions. We propose an efficient mechanism to activate complex branch conditions by identifying it as a sequence of simple conditions and incrementally applying concolic testing to activate these simple conditions.

III Incremental Concolic Testing

Figure 3 presents an overview of our proposed incremental concolic testing framework. It consists of three major tasks: sequence identification, design instrumentation, and incremental concolic testing. Algorithm 1 shows the relation between the three tasks. Given a design (D) and a branch target ($B_{i}$), the first step is to identify the set of sequences ($SS$) such that $B_{i}\rightarrow$ $<S_{1},S_{2},....,S_{n}>$. The second step is to instrument the design by converting each sequence to a branch statement. The second step results in instrumented design ($iD$) and the target queue ($TQ$). The third step is to apply concolic testing for each of the branch statements in the order of the sequence. The generated test can be used to activate the branch target during functional validation.

Example 1: We use a simple Verilog design (Listing 1) to describe various concepts in this paper. Listing 1 has three $always$ blocks corresponding to three functionalities in a simple memory module: write functionality (line 9 - 18), read functionality (line 19 - 28), and system functionality (line 29 - 42). While read and write are basic memory operations, the system functionality can be viewed as the top module (e.g., processor) trying to check a write followed by a read. For the ease of illustration, we are not showing all the else blocks for the $if$ statements. $\Box$

Figure 2 presents the control and data flow for Listing 1. The three always blocks presented in the example corresponds to the three CFGs as $CFG_{1}$ (memory write), $CFG_{2}$ (memory read), and $CFG_{3}$ (check). The solid black lines represent control flow when the branch condition is true, while the flow for the false condition is represented using black dotted lines.

III-A Sequence Identification

Algorithm 2 shows the procedure for sequence detection for a given branch target. This algorithm consists of four major steps. The first step constructs the CFG for the design. This step can be performed using any existing Verilog language parser. Figure 2 shows the CFG representation of the design in Listing 1. The next step extracts the branch condition for the target. This condition is an expression of the signals ($SE$). The third step uses DependencySearch function to recursively identify the assignment blocks that are relevant for each of the signal in $SE$. The final step returns the sequence of assignment blocks for activating the branch target.

Example 2: In Listing 1, consider the target as line 37 where the block is ($B_{15}$) and this is represented in Figure 2 as the “Target”. Line 1 of Algorithm 2 produces three concurrent CFGs with inter-CFG edges in Figure 2. Line 2 of Algorithm 2 produces the branch condition (line 36 in Listing 1) as $SE\leftarrow<r\_data$ == DATA$>$. This signal expression consists of one signal ($r\_data$) and one constant value ($DATA$). Since no action needed for $DATA$, the DependencySearch routine only tries to find the assignment block corresponding to signal $r\_data$. The signal $r\_data$ appears in one assignment (Line 25 in Listing 1) where $r\_data$ is assigned the value of $mem[addr]$ in $CFG_{2}$ block $B_{8}$. The block $B_{8}$ is pushed into $SS$. Then the dependency search is executed for the signals $mem$ and $addr$. Since the $addr$ is a primary input, the search will not continue for $addr$. An assignment exists for $mem$ in line 15 where $mem[addr]$ is assigned the value of $w\_data$ in $CFG_{1}$ block $B_{3}$. The block $B_{3}$ is pushed into $SS$. Since $w\_data$ is a primary input and there are no more assignments for $w\_data$, the recursion will end. Once the algorithm terminates, $SS$ will have $<B_{3},B_{8}>$. The dependency search for $r\_data$ is shown in Figure 2 using the two purple dotted lines. $\square$

III-B Design Instrumentation

Algorithm 3 shows the procedure for branch generation for a given sequence set $SS$. As shown in the algorithm, breadth first search (BFS) is performed along the predecessors of the target block in the CFG (Intra-BFS) to extract the conditions to activate the target. Line 1 of the algorithm identifies the constraints for the target. For each sequence in the $SS$, it tries to identify the constraints using the similar intra-BFS (line 3). The constraints can have either resolved Boolean expressions or unresolved expressions. In the next step, constraints from the target are used to resolve the unresolved constraints of the sequence. First an intersection is performed between the unresolved constraints from the sequence and constraints from the target. The results of the intersection are the new resolved constraints for the sequence. If still some of the constraints are unresolved in the sequence, it searches through dependencies to identify any dependent signals for the target. If any of the dependent signals are in the target constraints, the value of the target constraint is used to resolve the sequence constraint.

Example 3: To identify the constraints for “Target” block ($B_{15}$ in Figure 2 and line 37 in Listing 1), intra-BFS is performed in $CFG_{3}$. This search is represented using blue dotted lines in Figure 2. Intra-BFS for “Target” is $<B_{15}$, $B_{13}$, $B_{12}$, $B_{9}>$. Based on this traversal, we get the constraints to activate “Target” as $r\_en=1$, $w\_en=0$, $addr=ADDR$ and $r\_data=DATA$. Next, Intra-BFS is performed for the blocks in $SS$ ($<B_{3},B_{8}>$). The constraints for $B_{3}$ are $r\_en=0$, $w\_en=1$, $mem=UR$, $addr=UR$ and $w\_data=UR$, and the constraints for $B_{8}$ are $r\_en=1$, $w\_en=0$, $mem=UR$, $addr=UR$ and $r\_data=UR$. Here, $UR$ means unresolved. There are three unresolved constrained for $B_{3}$. We can resolve the first constraint $addr=UR$ to $addr=ADDR$. We need to search for dependencies to address the remaining two unresolved constraints ($mem$ and $w\_data$). The search of dependencies for $w\_data$ is shown in Figure 2 using red dotted lines. $w\_data$ is assigned to $mem[addr]$ and $mem[addr]$ is assigned to $r\_data$. Once the search is complete, final dependency for $w\_data$ can be identified as $r\_data$. Since $r\_data$ is included the target constraints, $w\_data$ gets the value of $r\_data$. After discarding the unresolved constraints, the final values for $B_{3}$ are $r\_en=0$, $w\_en=1$, $addr=ADDR$ and $w\_data=DATA$, and for $B_{8}$ are $r\_en=1$, $w\_en=0$, $addr=ADDR$ and $r\_data=DATA$. $\square$

In Algorithm 3, for each of the sequences in $SS$, conditional branches are created using the modified constraints (line 5) and these branches are embedded in the design. The newly created branches are stored in the $TQ$ (Target Queue) preserving the order in the $SS$. When the first sequence is removed from the $SS$, corresponding branch of that sequence is the first element to insert in the $TQ$. This process continues until $SS$ is empty. Finally, the modified design is instrumented (line 6). The goal of the instrumentation is to identify which path is executed by analyzing the simulation log. Specifically, we add print statements for all the branch conditions and end of the blocks by using a unique identifier.

III-C Incremental Concolic Testing

In this section, we present the incremental concolic testing scheme to activate a set of sequence events in the preserved order. Figure 4 presents a pictorial representation of incremental test generation. As shown in the figure, there are two sets: sequence set $<S_{1}$, $S_{2}$, ….., $S_{N}>$ and the corresponding test set $<T_{1}$, $T_{2}$, …., $T_{N}>$. To activate a sequence $S_{x}$, the required test is $\sum_{k=1}^{x}T_{k}$. For example, $T_{1}$ can activate $S_{1}$ but to activate $S_{2}$, we need both $T_{1}$ and $T_{2}$. A test set is a combination of different test vectors. A test $T_{x}$ includes $\sum_{i=a}^{b}t^{i}_{x}$ where $a,b\leq n$ (unroll cycle). The test vectors in $T_{1}$ is $<t^{1}_{1}$, $t^{2}_{1}$, …., $t^{d}_{1}>$ and the test vectors in $T_{2}$ is $<t^{d+1}_{2}$, $t^{d+2}_{2}$, …., $t^{d^{\prime}}_{2}>$.

Algorithm 4 describes the incremental test generation using concolic testing to activate a sequence of events preserving the order of events. Specifically, the test generated to activate the current event is used as the starting point to activate the next event in the sequence. For each target in $TQ$, we run concolic testing while changing the test set and the starting clock cycle (line 4). For the first target, the test set ($T$) is generated randomly and it contains test vectors up to the unroll cycle ($n$). The first step of concolic framework is to calculate the distance from the target to all the blocks. From the target breadth-first traversal is performed in the direction along the predecessors. The distance is initialized to 0 and incremented by 1 when an edge traversal is completed. Next, path ($P$) is generated by simulating the design with test set $T$. All the alternate branches from the current path $P$ is selected as the next step. When selecting the alternate branches, the clock is set to a specific starting clock cycle value so that we only select the branches after the starting clock cycle value. The path up to the starting clock cycle is set and unchanged. Then the selected alternate branches are sorted using the distance and the clock value. This will lead to the most profitable alternate branch. Using the trace of $P$ and the chosen branch, constraint vector is generated. The constraint vector contains the value of the constraints for each of the clock cycles. Then the constraint vector is solved using a constraint solver. The constraint solver produces a new test set and this is used to simulate the design and get a new path. If the new path activates the target, the test set will be added to $T$. Also, the clock cycle of the selected branch will be set as the new starting clock cycle. Hence, the test set generated for the target will be preserved and used as a starting point to the next target in $TQ$.

Example 4: Target Queue ($TQ$) contains 2 branch targets $<B_{17}$, $B_{19}>$ which are shown in Listing 2. Assume that the unroll cycle ($n$) is 10 and search $limit$ is 10 iterations. Concolic testing is used to activate the first branch ($B_{17}$) which is corresponding to writing a value to the memory. The $start$ value is 1 and a random test set is used as initial setting. If the tests to activate the target ($B_{17}$) is identified in unroll cycle 3, then the starting cycle is set as 4 for the next target ($B_{19}$). $\square$

IV Experiments

IV-A Experimental Setup

For experimental evaluation, we have selected a re-configurable cache implementation, IOb-Cache [11]. It interfaces with a processor and main memory. For the case studies in Section IV-B, we have selected configurations as follows: (address width=16, data width=32, write back, LRU replacement, and 4-way set-associative design). With the above configuration, we flattened the IOb-Cache module eliminating its hierarchy with Yosys synthesis tool. The flattened RTL netlist is about 10,000 lines of code. This configuration is used for validation of different functional scenarios outlined in Section IV-B. In order to generate the abstract syntax tree of the RTL model, we use Icarus Verilog Target API [12]. We use Yices SMT solver [13] for solving constraints. Incremental concolic testing is implemented on top of the concolic testing framework [4]. In order to ensure validity of the generated test vectors, we simulate the original design with the generated test and analyze the Value Change Dump (VCD) to confirm the activation of the target (corner case). We ran our experiments on Intel i7-5500U @3.0GHz CPU with 16GB RAM.

IV-B Corner Case Scenarios

We have created different memory verification cases to validate corner case functionalities of the cache and memory. Specifically, we consider the following eight corner cases.

Case 1: Write a specific value to memory (Listing 3).

Case 2: Read a specific data form a specific address (Listing 4). This scenario is similar to the target in Listing 1.

Case 3: Back to back writes to the same address. We copied the entries in Listing 3 for 5 times and changed the data values.

Case 4: Back to back reads from the same address. We copied the entries in Listing 4 for 5 times and changed the data values.

Case 5: Write data to a boundary location in memory. We used the Listing 3, created two copies, and changed the address value to 4’h0000 and 4’hFFFF, respectively.

Case 6: Read data from a boundary location in memory. We used the same Listing 4, created two copies, and changed the address value to 4’h0000 and 4’hFFFF, respectively.

Case 7: Verify front-end and back-end addresses for correct address translation as shown in Listing 5. The specifc address translations are identified by analyzing the RTL models of front-end and back-end modules.

Case 8: Verify cache hit for a specific memory read. As shown in Listing 6, when the required write happens before the read, the cache hit should get triggered.

IV-C Results

In this section, we present the results of our case study. We compare our approach with EBMC [14] and the concolic testing framework presented in [4]. EBMC is a state-of-the art formal verification framework that uses bounded model checking. The concolic testing framework [4] is state-of-the-art in activating RTL branch statements using concolic testing. The number of unrolled cycles are determined based on the complexity of the scenarios. This can be achieved by starting from a reasonable number of unroll cycles and increment until the scenarios are covered. The number of unroll cycles is analogous to the bound determination for bounded model checking. We set the bound for EBMC to be equal to the number of unroll cycles for concolic testing.

The corner case activation results at system level are shown in Table I. The first column represents different corner case scenarios outlined in Section IV-B. The second column provides the unroll cycles (bound for EBMC). For each approach, we provide information about if the target (corner case) is activated (Yes or No) within the bound, and if yes, what is the memory requirement (in MB) and run time (in seconds). As shown in Table I, EBMC only covers one scenario, and concolic [4] covers only three scenarios. Our approach successfully covered all the 8 scenarios. EBMC is expected to fail for most of the scenarios due to state space exploitation problem. The concolic framework in [4] activates some of the branches, however, when dealing with contradictory and complex sequences, it fails to activate the target due to path explosion problem ([4] selects branches based on the distance heuristics).

To understand the limitation of the state-of-the-art RTL concolic framework in [4], we only consider the iob_ram module with ‘Case 2’ and compare the memory and time requirements. The experimental results are shown in Table II. The concolic framework in [4] was able to activate the target (Case 2) only when unrolled for 50 cycles whereas our approach is able to activate the branch in 10 unroll cycles. The performance improvement of our approach compared to [4] in terms of time and memory is 24 times and 12 times, respectively. It also highlights that state-of-the-art can activate corner cases if the design is sufficiently unrolled, which can be infeasible for industrial designs since various components in concolic testing (e.g., constraint solver) may not be able to handle such a large number of constraints.

V Conclusion

Concolic testing provides a scalable test generation framework using an effective combination of simulation and formal methods. While it is promising for branch coverage in register-transfer level (RTL) deigns, it cannot activate complex corner cases such as hard-to-activate branches. We have developed an incremental concolic testing framework to cover such corner case scenarios in RTL models. Specifically, this paper made three important contributions. First, we show that a complex branch condition can be decomposed as a sequence of easy-to-activate events by traversing respective control and data flow graphs. Next, we map the branch coverage problem to the coverage of a sequence of events such that the test generated to activate the current event can be used as the starting point for activating the next event in the sequence. Finally, we have developed an efficient algorithm to cover the sequence of events by iterative invocation of concolic testing. Our experimental results demonstrated that our approach can be used to generate directed tests to cover complex branch targets in modern memory designs, while state-of-the-art methods fail to activate them.