Malay K Ganai

Aarti Gupta

Pranav Ashar

Verification of Embedded Memory Systems using Efficient Memory Modeling

We describe verification techniques for embedded memory systems using efficient memory modeling (EMM), without explicitly modeling each memory bit. We extend our previously proposed approach of EMM in Bounded Model Checking (BMC) for a single read/write port single memory system, to more commonly occurring systems with multiple memories, having multiple read and write ports. More importantly, we augment such EMM to providing correctness proofs, in addition to finding real bugs as before. The novelties of our verification approach are in a) combining EMM with proof-based abstraction that preserves the correctness of a property up to a certain analysis depth of SAT-based BMC, and b) modeling arbitrary initial memory state precisely and thereby, providing inductive proofs using SAT-based BMC for embedded memory systems. Similar to the previous approach, we construct a verification model by eliminating memory arrays, but retaining the memory interface signals with their control logic and adding constraints on those signals at every analysis depth to preserve the data forwarding semantics. The size of these EMM constraints depends quadratically on the number of memory accesses and the number of read and write ports; and linearly on the address and data widths and the number of memories. We show the effectiveness of our approach on several industry designs and software programs.

Introduction

According to the Semiconductor Industry Association roadmap prediction, embedded memories will comprise more than 70% of the SoC by 2005. These embedded memories on SoC support diverse code and data requirements arising from ever increasing demand for data throughput in applications ranging from cellular phones, smart cards and digital cameras. In the past, there were efforts [START_REF] Pandey | Formal Verification of PowerPC Arrays using Symbolic Trajectory Evaluation[END_REF] to verify on-chip memory arrays using Symbolic Trajectory Evaluation [START_REF] Seger | Formal Verification by Symbolic Evaluation by Partially-ordered Trajectories[END_REF]. However, these embedded memories dramatically increase both design and verification complexity due to an exponential increase in the state space with each additional memory bit. In particular, this state explosion adversely affects the practical application of formal verification techniques like model checking [START_REF] Mcmillan | Symbolic Model Checking: An Approach to the State Explosion Problem[END_REF][START_REF] Clarke | Model Checking[END_REF] for functional verification of such large embedded memory systems.

To tame the verification complexity, several memory abstraction techniques, i.e., removing the memories partially or completely from the designs are often used in the industry. However, such techniques often produce spurious outcomes, adversely affecting overall verification efforts. In many refinement-based techniques [START_REF] Long | Model checking, abstraction and compositional verification[END_REF][START_REF] Clarke | Counterexample-guided abstraction refinement[END_REF][START_REF] Clarke | SAT based abstraction-refinement using ILP and machine learning techniques[END_REF][START_REF] Chauhan | Automated Abstraction Refinement for Model Checking Large State Spaces using SAT based Conflict Analysis[END_REF], starting from a small abstract model of the concrete design, spurious counter-examples on the abstract model are used to refine the model iteratively. In practice, several iterations are needed before a property can be proved correct or a real counter-example can be found. Note that after every iterative refinement step, the model size increases, making it increasingly difficult to verify. In contrast, abstraction-based approaches [START_REF] Mcmillan | Automatic Abstraction without Counterexamples[END_REF][START_REF] Gupta | Iterative Abstraction using SAT-based BMC with Proof Analysis[END_REF] use proof-based abstraction (PBA) techniques on a concrete design. As shown in [START_REF] Gupta | Iterative Abstraction using SAT-based BMC with Proof Analysis[END_REF], iterative abstraction can be used to apply such techniques on progressively more abstract models, thereby leading to significant reduction in model size. However, since these approaches use the concrete model to start with, it may not be feasible to apply them on designs with large memories. In general, both these refinement and abstraction based approaches are not geared towards exploiting the memory semantics.

Memory abstractions that preserve the memory semanticsdata read from a memory location is the same as the most recent data written at the same location -have been employed in various verification efforts in the past. Burch et al. introduced the interpreted read and write operations in their logic of equality with un-interpreted functions [START_REF] Burch | Automatic verification of pipelined microprocessor control[END_REF]. Such partial interpretation of memory has also been exploited in later derivative verification efforts [START_REF] Velev | Efficient Modeling of Memory Arrays in Symbolic Simulation[END_REF][START_REF] Bryant | Processor Verification Using Efficient Reductions of the Logic of Uninterpreted Functions to Propositional Logic[END_REF][START_REF] Velev | Automatic Abstraction of Memories in the Formal Verification of Superscalar Microprocessors[END_REF]. Specifically, Velev et al. used this partial interpretation in a symbolic simulation engine to replace memory by a behavioral model that interacts with the rest of the circuit through a software interface that monitors the memory control signals [START_REF] Velev | Efficient Modeling of Memory Arrays in Symbolic Simulation[END_REF]. Bryant et al. proposed [START_REF] Bryant | Modeling and Verifying Systems using a Logic of Counter Arithmetic with Lambda Expressions and Uninterpreted Functions[END_REF] modeling of memory as a functional expression in the UCLID system for verifying safety properties.

SAT-based Bounded Model Checking (BMC) [START_REF] Biere | Symbolic Model Checking without BDDs[END_REF] enjoys several nice properties over BDD-based symbolic model checking [START_REF] Mcmillan | Symbolic Model Checking: An Approach to the State Explosion Problem[END_REF][START_REF] Clarke | Model Checking[END_REF]; its performance is less sensitive to the problem sizes and it does not suffer from space explosion. To address the memory explosion problem, SAT-based distributed BMC has been proposed [START_REF] Ganai | Distributed SAT and Distributed Bounded Model Checking[END_REF] in which the BMC problem is partitioned over a network of workstations. However, this technique is not geared towards verifying embedded memory systems. In our previous work, we have proposed an efficient memory modeling (EMM) technique [START_REF] Ganai | Efficient Modeling of Embedded Memories in Bounded Model Checking[END_REF] that augments SAT-based BMC to handle large embedded memories without explicitly modeling each memory bit. We showed that EMM approach allows deeper BMC search in finding real bugs in comparison to explicit memory models. Moreover, our approach captures the exclusivity of a matching read and writes pair explicitly, reducing the overall SAT solve time. However, there are two main drawbacks to this previous work. First, the memory system considered was fairly simplistic, with a single memory having a single read/write port. In modern designs, it is quite common to have a large number of diverse memories, each with multiple read and write ports. Second, the approach was geared towards falsification i.e., finding real bugs, and not towards proving correctness of the specified property.

In this work, we extend our previous approach [START_REF] Ganai | Efficient Modeling of Embedded Memories in Bounded Model Checking[END_REF] of EMM in SAT-based BMC to the more commonly occurring embedded memory systems, with multiple memories having multiple read and write ports. More importantly, we augment the EMM techniques to providing correctness proofs in addition to finding real bugs. The novelties of our verification approach are in a) combining EMM with PBA that preserves the correctness of a property up to a certain analysis depth of SAT-based BMC, and b) modeling arbitrary initial memory state precisely and thereby, providing inductive proofs using SAT-based BMC for embedded memory systems. Similar to the previous approach [START_REF] Ganai | Efficient Modeling of Embedded Memories in Bounded Model Checking[END_REF], we construct a verification model by eliminating memory arrays, but retaining the memory interface signals with their control logic and adding constraints on those signals at every analysis depth to preserve the memory data forwarding semantics. The size of these memory-modeling constraints depends quadratically on the number of memory accesses and the number of read and write ports; and linearly on the address and data widths and the number of memories. We have implemented our techniques in a prototype verification platform, and demonstrate their effectiveness on several industry designs and software programs. Outline In Section 2 we give relevant background on memory semantics, SAT-based BMC, and PBA; in Section 3 we discuss the previous EMM approach; in Section 4 we describe our contributions; in Section 5 we discuss our experiments on several case studies, and conclude in Section 6.

Background

Bounded Model Checking (BMC)

In BMC, the specification is expressed in LTL (Linear Temporal Logic). Given a Kripke structure M, an LTL formula f, and a bound n, the translation task in BMC is to construct a propositional formula [M, f] n such that the formula is satisfiable if and only if there exists a witness of length n [START_REF] Biere | Symbolic Model Checking without BDDs[END_REF]. The satisfiability check is performed by a backend SAT solver. Verification typically proceeds by looking for witnesses or counter-examples (CE) of increasing length until the completeness bound is reached [START_REF] Biere | Symbolic Model Checking without BDDs[END_REF][START_REF] Sheeran | Checking Safety Properties using Induction and a SAT Solver[END_REF]. The overall algorithm (BMC-1) of a SAT-based BMC method for checking a simple safety property is shown in Figure 1 (ignore lines 10-11 for now). Note that P i denotes the property node at the i th unrolling of the transition relation, I denotes the initial state of the system, and LFP i denotes that the path of length i is loop-free. In lines 5-7, a SAT solver is used to check the forward and backward termination criteria for correctness [START_REF] Sheeran | Checking Safety Properties using Induction and a SAT Solver[END_REF]. In line 8, a SAT solver is used to check the existence of a counter-example.

Proof-based Abstraction (PBA)

A PBA technique for SAT-based BMC is shown in lines 10-11 in Figure 1. When the SAT problem at line 8 is unsatisfiable, i.e., there is no counter-example for the safety property at a given depth i, the unsatisfiable core (U_Core) is obtained using the procedure SAT_Get_Refutation in line 10. This procedure simply retraces the resolution-based proof tree used by the SAT solver and identifies a subset formula that is sufficient for unsatisfiability [START_REF] Mcmillan | Automatic Abstraction without Counterexamples[END_REF][START_REF] Zhang | Validating SAT Solvers Using an Independent Resolution-Based Checker: Practical Implementations and Other Applications[END_REF]. One can then use either a gate-based abstraction [START_REF] Mcmillan | Automatic Abstraction without Counterexamples[END_REF] or a latch-based abstraction [START_REF] Gupta | Iterative Abstraction using SAT-based BMC with Proof Analysis[END_REF] technique to obtain an abstract model from the U_Core. Here we show a latch-based abstraction technique in line 11, to obtain a set of latch reasons LR i at depth i. An abstract model is then generated for depth i by converting those latches in the given design that are not in the set LR i to pseudo-primary inputs. Due to the sufficiency property of U_Core, the resulting abstract model is guaranteed to preserve correctness of the property up to depth i [START_REF] Mcmillan | Automatic Abstraction without Counterexamples[END_REF][START_REF] Gupta | Iterative Abstraction using SAT-based BMC with Proof Analysis[END_REF]. Depending on locality of the property, the set LR i can be significantly smaller than the total latches in the given design. Specifically in [START_REF] Gupta | Iterative Abstraction using SAT-based BMC with Proof Analysis[END_REF], a depth d (< n) is chosen such that the size of set LR d does not increase over a certain number of depths, called stability depth. In many cases, the property can be proved correct on the abstract model generated at depth d and hence, for the given design. One can apply PBA techniques iteratively, called iterative abstraction [START_REF] Gupta | Iterative Abstraction using SAT-based BMC with Proof Analysis[END_REF], to further reduce the set LR d and hence, obtain a smaller abstract model.

Memory Semantics

Embedded memories are used in several forms such as RAM, stack, and FIFO with at least one port for data access. We model a design with an embedded memory, as a Main module interacting with the memory module using the following memory interface signals: Address Bus (Addr), Write Data Bus (WD), Read Data Bus (RD), Write Enable (WE), and Read Enable (RE). For the single-port memory at any given clock cycle: a) at most one address is valid, b) at most one write occurs, and c) at most one read occurs. In the write phase of the memory accesses, new data is assigned to WD in the same cycle when the Addr is valid and WE is active. Note that the new written data is available for read only after the current cycle. In the read phase, data is assigned to RD in the same cycle when the Addr is valid and RE is active.

Assume that we unroll the design up to depth k (starting from 0). Let X j denote a memory interface signal variable X, at time frame j. Let the Boolean variable E i,j denote the address comparison between time frames i and j, defined as E i,j =(Addr i =Addr j ). Then the data forwarding semantics of the memory can be expressed as follows, where j < k:

(E j,k ∧WE j ∧RE k ∧∀ j<i<k (¬E i,k ∨¬WE i )) ĺ (RD k =WD j ) ( 1 )
In the other words, the data read at depth k equals the data written at depth j if the addresses are equal at k and j, the write enable is active at j, the read enable is active at k, and for all depths strictly between j and k, no data was written at the address location Addr k .

EMM for Single Memory, Read/Write Port

EMM as proposed in [START_REF] Ganai | Efficient Modeling of Embedded Memories in Bounded Model Checking[END_REF], based on the data forwarding semantics, is described as follows: 1. The MEM module is removed but the memory interface signals and their control logic are retained with their inputoutput directionality with respect to the Main Module. 2. Constraints are added at every analysis depth k in BMC, on the memory interface signals to preserve the forwarding semantics of the memory. 3. In addition, exclusivity constraints are added to improve the performance of the backend SAT solver in BMC. The idea is that when the SAT-solver decides on a valid matching read and write pair, other pairs are implied invalid immediately. Note that although 1) and 2) are sufficient to generate an efficient model that preserves the validity of a correctness property, it has been shown [START_REF] Ganai | Efficient Modeling of Embedded Memories in Bounded Model Checking[END_REF] that 3) makes the performance of the SAT-based BMC superior.

The modified BMC algorithm using the EMM approach (BMC-2) for a single memory, single read/write port system (as in [START_REF] Ganai | Efficient Modeling of Embedded Memories in Bounded Model Checking[END_REF]) is shown in Figure 2. Note that the algorithm does not provide proofs with the EMM model. In this procedure, the memory modeling constraints are generated by the procedure EMM_Constraints, which is invoked after every unrolling. The updated constraints C i in line 5 capture the forwarding semantics of the memory up to depth i very efficiently using hybrid representations, i.e., 2-input gates and CNF clauses, in order to improve the SAT solve time. The procedure EMM_Constraints (lines 8-11 in Figure 2) generates the EMM constraints at a depth k by using the following 3 sub-procedures: Generate_Addr_Equal_Sig, Generate_Valid_Read_Sig, and Generate_Read_Data_Constraints.

Fig. 2. SAT-based BMC with EMM

Generation of address comparison signals:

To capture every address pair comparison E j,k =(Addr j =Addr k ), new variables e j,k i and following 4 CNF clauses are added for each address bit i (where 0i<m, and m is address width, AW) (E j,k ĺ(Addr j i =Addr k i )) , ((Addr j i =Addr k i )ĺ e j,k i ) Finally, add a clause to capture the relation between E j,k and e j,k i , (!e j,k 0 + …+!e j,k i + … + !e j,k m-1 +E j,k ). Generation of exclusive valid read signals: Let the Boolean variable s j,k be defined as s j,k =E j,k ∧WE j . The decision s i,k =1 does not necessarily imply RD k =WD i ; other read-write pairs need to be established invalid through the decision procedure as well, i.e., s i+1,k =0, s i+2,k =0, …,s k-1,k =0. Explicit constraints to capture the exclusivity of matching read and write pairs (i.e., once a matching read-write pair is chosen by the SAT-solver, the other pairs are implied invalid immediately) has been shown [START_REF] Ganai | Efficient Modeling of Embedded Memories in Bounded Model Checking[END_REF] to improve the SAT solve time significantly. Let the Boolean variables S i,k and PS i,k denote the exclusive valid read signal and the intermediate signal respectively. They are built recursively using gates for all depths i > 0 as follows:

∀ 0≤i<k PS i,k = !s i,k ∧PS i+1,k (= RE k for i=k) ∀ 0≤i<k S i,k
= s i,k ∧PS i+1,k (= PS 0,k for i=-1) Note that S i,k =1, immediately implies S j,k =0 where j≠i, i,j < k. Generation of constraints on read data signals: Using the above exclusive signals, equation ( 1) is expressed as

RD k =(S k-1,k ∧WD k-1 ) ∨ (S k-2,k ∧WD k-2 ) ∨…∨ (S -1,k ∧WD -1 ) (2)
where, WD -1 denote the initial memory state. Note, for all j<k at most one S j,k is equal to 1. The equation ( 2) is expressed compactly using the following CNF clauses:

∀ 0≤i<n, ∀ -1≤j<k (S j,k ĺ(RD k i =WD j i )) (DW, data width = n) To capture validity of read signal, the following clause is added, (!RE k + S -1,k +…+S j,k +…+S k-1,k ) At depth k, the hybrid representation adds (4Âm+2Ân+1)Âk+2Ân+1 clauses and 3Âk gates, as compared to (4Âm+2Ân+2)Âk+n gates in a purely circuit-based representation. It has also been shown that although the size of these accumulated constraints grows quadratically with depth k, they are still significantly smaller than the explicit memory-model [START_REF] Ganai | Efficient Modeling of Embedded Memories in Bounded Model Checking[END_REF].

Our Contributions

In this section, we describe our three main contributions: 1. We propose EMM for embedded systems with multiple memories, with multiple read and write ports. We show that the growth of the constraints is quadratic with analysis depth, similar to that of a single memory with a single read/write port. 2. We model arbitrary initial state of the memory precisely, and use it to provide SAT-based induction proofs in BMC. 3. We also propose combining PBA techniques with EMM.

We show that using this combined approach, we can identify fewer memory modules and ports that need to be modeled; thereby reducing the model size and verification complexity.

EMM for Multiple Memories, Read, and Write Ports

Before we delve into a discussion of efficient modeling, we first define memory semantics in the presence of multiple read and write ports. We assume there are no data races. In other words, a memory location can be updated at any given cycle through only one write port. (We can easily extend our approach to check for data races but details are beyond the scope of the paper.) Since each memory module is accessed only through its ports, the memory modules can be considered independent of each other.

In our following discussion, we first consider a single memory with multiple read and multiple write ports. Let the design be unrolled up to depth k (starting from 0). Let X j,p denote a memory interface signal variable X at time frame j for a port p. Let R and W be the number of read and write ports, respectively, for the given memory. Let the Boolean variable E j,i,w,r denote the address comparison of the read port r at depth i, and the write port w at depth j, defined as E j,i,w,r =(Addr i,r =Addr j,w ). Then the forwarding semantics of the memory can be expressed as:

(E j,k,w,r ∧WE j,w ∧RE k,r ∧∀ 0p<W ∀ j<i<k (¬E i,k,p,r ∨¬WE i,p )) ĺ (RD k,r = WD j,w ) ( 3 ) In other words, data read at depth k through read port r, equals the data written at depth j through write port w, if the addresses are equal at depth k and j, write enable is active at j for the write port w, read enable is active at k for the read port r, and for all depths strictly between j and k, no data was written at the address location Addr k,r through any write port.

Let the Boolean variable s j,k,w,r be defined as s j,k,w,r =E j,k,w,r ∧WE j,w . The decision s i,k,w,r =1 does not necessarily imply RD k,r =WD i,w ; other pairs need to be established invalid through the decision procedure as well, i.e., s i,k,w+1,r =0, ...,s i,k,W- 1,r =0, s i+1,k,0,r =0, …,s i+1,k,W-1,r =0, …,s k-1,k,0,r =0, …,s k-1,k,W-1,r =0. Similar to the single read/write port approach [START_REF] Ganai | Efficient Modeling of Embedded Memories in Bounded Model Checking[END_REF], we add explicit constraints to capture the exclusivity of the matching read-write pair, in order to improve the SAT solve time. Let the Boolean variables S i,k,w,r and PS i,k,w,r denote the exclusive valid read signal and intermediate signal respectively for a given read port r and write port w. They are defined recursively as follows:

PS k,k,0,r = RE k,r ∀ 0≤i<k ∀ 0≤p<W PS i,k,p,r = !s i,k,p,r ∧PS i,k,p+1,r (PS i,k,W,r = PS i+1,k,0,r ) ∀ 0≤i<k ∀ 0≤p<W S i,k,p,r = s i,k,p,r ∧PS i,k,p+1,r (4) Now the forwarding semantics for multiple read and write ports can be expressed as RD k,r = (∨ 0≤p<W,0≤i<k S i,k,p,r ∧WD i,p )∨(PS 0,k,0,r ∧WD -1 )

( 5 ) Note that S i,k,p,r =1, immediately implies S j,k,q,r =0 where either q≠p or j≠i, and i,j < k. Similar to [START_REF] Ganai | Efficient Modeling of Embedded Memories in Bounded Model Checking[END_REF], we use a hybrid representation to add the memory modeling constraints as part of the procedure EMM_Constraints, which is invoked after every unrolling as shown in Figure 2. Given DW = n and AW = m, we give the sizes of EMM constraints added in terms of clauses and gates for each read port at a given depth k. 1. Address comparison: We require (4Âm+1)ÂkÂW CNF clauses to represent address comparison signals.

Exclusive constraints:

We require 3ÂkÂW 2-input gates to represent the exclusivity constraints in equation ( 4). 3. Read data constraints: We require 2ÂnÂkÂW+2Ân+1 CNF clauses to represent read data constraints in equation ( 5). In total, we need (4Âm+2Ân+1)ÂkÂW+2Ân+1 clauses and 3ÂkÂW gates for a single read port and W write ports. For R read ports, we would need ((4Âm+2Ân+1)ÂkÂW+2Ân+1)ÂR clauses and 3ÂkÂWÂR gates. Note, the growth of constraints remain quadratic with analysis depth k and is WÂR times the constraints required for a single memory having a single read/write port. In the presence of multiple memories, we add these EMM constraints for each of them.

Arbitrary Initial Memory State

To model a memory with an arbitrary initial state, we introduce new symbolic variables at every time frame. Observe that for a (k-1)-depth analysis of a design, there can be at most k different memory read accesses from a single read port; out of which at most k accesses can be to un-written memory locations. Therefore, in total we need to introduce k symbolic variables for the different data words for each read port at analysis depth k-1. However, these variables are not entirely independent. Simply introducing new variables introduces additional behaviors in the verification model. Therefore, we need to identify a sufficient set of constraints that models the arbitrary initial state of the memory correctly.

Let V i,p and V j,q represent new data words introduced at depths i and j, for read ports p and q, respectively. Let RA i,p and RA j,q be the corresponding read addresses for the ports p and q (p and q need not be distinct). Let N i,p (and N j,q ) denote the condition that no write has occurred until depth i (and j) at address location RA i,p (and RA j,q ). We can then express the data read from the ports p and q at depths i and j, respectively, as: N i,p ĺ (RD i,p =V i,p ), N j,q ĺ (RD j,q =V j,q ) Note that, if read addresses RA i,p and RA j,q are equal, then V i,p and V j,q should also be equal. We add the following constraint to capture the same, (RA i,p =RA j,q ∧ N i,p ∧N j,q ) ĺ (V i,p =V j,q ) ( 6 ) For R read ports at (k-1)-depth analysis, we need to add kÂRÂ (R-1) such constraints. We add these constraints using a hybrid representation in a separate sub-procedure call within the procedure EMM_constraints. Note that the proof step in BMC-1, (line 6, Figure 1) requires correct modeling of the arbitrary initial state of the memory. Using the new set of memory constraints as in equation ( 6), we augment the proof steps of BMC with EMM constraints. The modified algorithm (BMC-3) is shown in Figure 3 (ignore lines 11-12 for now). Later, we will show that the correctness of safety properties can not be shown without adding these constraints.

EMM with Proof-based Abstraction

As discussed earlier, EMM can significantly reduce the size of the verification model for a SoC having multiple memories and multiple ports. However, for checking the correctness of a given safety property, we may not require all the memory modules or the ports. To further reduce the model, we can abstract out irrelevant memory modules or ports completely. In this case, we do not need to add the memory modeling constraints for the irrelevant memory modules or ports, thereby further reducing the BMC complexity.

For the purpose of automatically identifying irrelevant memory modules and ports, we propose a technique combining EMM constraints with PBA [START_REF] Gupta | Iterative Abstraction using SAT-based BMC with Proof Analysis[END_REF]. This can not only reduce the non-memory logic (from the Main module) but also identify the memory modules and ports that are not required for proving correctness up to a given bounded depth of BMC analysis. The overall BMC algorithm with PBA and EMM constraints (BMC-3) is shown in lines 11-12 of Figure 3. CP 0 =1; LR -1 =Ɏ; C -1 =Ɏ; 3.

for (int i=0; i<=n ; i++) { 4.

P i = Unroll(P,i); // property node at i th unrolling 5.

C i = C i-1 ∪ EMM_Constraints(i); // update the constraints 6.

if (SAT_Solve(I∧LFP i ∧C i )=UNSAT or 7.

SAT_Solve

(LFP i ∧¬P i ∧CP i ∧C i )=UNSAT) { 8.
return PROOF;} // bwd and fwd termination check 9.

if (SAT_Solve(I∧¬P i ∧C i )=SAT) return CE; 10.

CP i+1 = CP i ∧P i ; // update CP 11.

U_Core = SAT_Get_Refutation(); // get proof of UNSAT 12.

LR i = LR i-1 ∪ Get_Latch_Reasons(U_Core);} 13. return NO_CE; } // no counter-example found

Fig. 3. SAT-based BMC with EMM and PBA

The dependency of the property on any memory module for a given depth i is determined easily by checking whether a latch corresponding to the control logic for that memory module (the logic driving the memory interface signals) is in the set LR i . If no such latch exists in the set LR i , we do not add the EMM modeling constraints for that memory module. In other words, we abstract out that memory module completely. We perform similar abstraction for each memory port. This reduces the problem size and improves the performance, as observed in our experiments reported in the next section.

Experiments

We have implemented the proposed EMM techniques in a prototype verification platform, which includes standard verification techniques for SAT-based BMC and BDD-based model checking. We report our experiences on several case studies consisting of large industry designs and software programs that have embedded memory modules with multiple read and write ports. Two case studies correspond to industry designs with many reachability properties. Another case study involves a sorting algorithm with properties validating the algorithm. For each of the properties, we require modeling of the embedded memory, and the case studies were chosen to highlight the use of our different contributions. We compare our approach (labeled EMM), with explicit memory modeling (labeled Explicit Modeling) to show the effectiveness of our approach. We experimented on a workstation with 2.8 GHz Xeon processors with 4GB running Red Hat Linux 7.2.

Case Study on Quick Sort: This case study makes use of EMM for multiple memories, EMM that models arbitrary initial state, and EMM with PBA to identify irrelevant memory modules.

We implemented a quick sort algorithm using Verilog HDL (Hardware Description Language). The algorithm is recursively called, first on the left partition and next on the right partition of the array (Note: a pivot partitions the array into left and right). We implemented the array as a memory module with AW=10 and DW=32, with 1 read and 1 write port. We implemented the stack (for recursive function calls) also as a memory module with AW=10 and DW=24, with 1 read and 1 write port. The design has 200 latches (excluding memory registers), 56 inputs, and ~9K 2-input gates. We chose two properties: a) P1: the first element of the sorted array (in ascending order) can not be greater than the second element, b) P2: after return from a recursive call, the program counter should go next to a recursive call on the right partition or return to the parent on the recursion stack. The array is allowed to have arbitrary values to begin with. This requires precise handling of the arbitrary initial memory state (equation ( 6)) to show the correctness of the property.

For different array sizes N, we compared the performance of EMM and Explicit Modeling approaches, using the forward induction proof checks in BMC-3 and BMC-1 respectively. We used a time limit of 3 hours for each run. We present the results in Table 1. Column 1 shows different array sizes N; Column 2 shows the properties; Column 3 shows the forward proof diameter; Columns 4-5 and 6-7 show performance time and space used by EMM and Explicit Modeling, respectively. Note that using EMM we were able to prove all properties in the given time limit, while Explicit Modeling simply times out. Note that property P1 depends on both the array and the stack, while property P2 depends on only the stack for correctness. In other words, for P2, the contents of the array should not matter at all. We used the PBA technique to examine this. For property P2, we compared performance of EMM with PBA using BMC-3, with that of PBA on Explicit Modeling using BMC-1. We used a stability depth of 10 to obtain the stable set LR. We present the results in It is interesting to note that by use of PBA, the reduced model in Column 2 did not have any latch from the control logic of the memory module representing the array. Therefore, we were able to automatically abstract out the entire array memory module, while doing BMC analysis on the reduced model using EMM. Note that this results in significant improvement in performance, as clear from a comparison of the performance figures of EMM on property P2 in columns 4-5 of Tables 1 and2. Moreover, we see several orders of magnitude performance improvement over the Explicit Modeling, even on the reduced models. Note, for N=5 we could not generate a stable latch model in the given time limit for the Explicit Modeling case. Case Study on Industry Design I: This case study makes use of our approach of EMM for multiple memories and EMM with induction proofs. The industry design is a low-pass image filter with 756 latches (excluding the memory registers), 28 inputs and ~15K 2input gates. It has two memory modules, both having address width, AW = 10 and data width, DW = 8. Each module has 1 write and 1 read port, with memory state initialized to 0. There are 216 reachability properties. EMM: We were able to find witnesses for 206 of the 216 properties, in about 400s requiring 50Mb. The maximum depth over all witnesses was 51. For the remaining 10 properties, we were able to obtain the proofs by induction using BMC-3, in less than 1s requiring 6Mb. Note that the introduction of new variables to model arbitrary initial memory state, without the constraints in equation ( 6), was sufficient for the proofs although they capture extra behavior in the verification model. Explicit Modeling: We required 20540s (~6Hrs) and 912Mb to find witnesses for all 206 properties. For the remaining 10 properties, we were able to obtain the proofs by induction using BMC-1 in 25s requiring 50Mb.

Case Study on Industry Design II: This case study makes use of EMM for memory with multiple ports, and for finding invariants that can aid proofs by induction.

The design has 2400 latches (excluding the memory registers), 103 inputs and ~46K 2-input gates. It has one memory module with AW=12 and DW=32. The memory module has 1 write port and 3 read ports, with memory state initialized to 0. There are 8 reachability properties.

We found spurious witnesses at depth 7 for all properties, if we abstract out the memory completely. Thus, we needed to include the memory module. Using EMM, we were not able to find any witnesses for these properties up to depths of 200 in about 10s. Next, we tried obtaining a proof of unreachability for all depths. Using EMM with PBA, we were able to reduce the model to about 100 latches requiring 4-5 minutes. However, the model was not small enough for our BDD-based model checker or SAT-based BMC to provide a proof. We also noticed that the WE (write enable) control signal stayed inactive in the forward search of 200 depth. Observing that, we hypothesized that the memory state does not get updated, i.e., it remains in its initial state. This is expressed using the following LTL property: G(WE=0 or WD=0) i.e., always, either the write enable is inactive or the write data (WD) is 0. Using BMC-3, we were able to prove the above property using backward induction at depth 2 in less than 1s. Explicit Modeling using BMC-1 takes 78s to prove the same.

The above invariant implies that the data read is always 0 (could potentially be a design bug). Next we abstracted out the memory, but applied this constraint to the input read data signals. We used PBA to further reduce the design to only 20-30s latches for each property (taking about a minute). We then proved each property unreachable on the reduced model using forward induction proof in BMC-1 in less than 1s. (Our BDDbased model checker was unable to build even the transition relation for these abstract models.)

Fig. 1 .

 1 Fig. 1. SAT-based BMC with PBA

1 .

 1 BMC-3 (n, P){// Check safety property P within bound n 2.

Table 1 . Performance summary on Quick Sort

 1

	N	P r o p D	EMM Sec MB	Explicit Sec MB
	3	P1	27	64	55	>3hr	NA
	3	P2	27	30	44	>3hr	NA
	4	P1	42	601	105	>3hr	NA
	4	P2	42	453	124	>3hr	NA
	5	P1	59 6376	423	>3hr	NA
	5	P2	59 4916	411	>3ht	NA

Table 2 .

 2 Column 1 shows different array sizes N, Columns 2-5 show performance figures for EMM. Specifically, Column 2 shows the number of latches in the reduced model size using EMM with PBA. The value in bracket shows the original number of latches. Column 3 shows the time taken (in sec) for PBA to generate a stable latch set. Columns 4-5 show the time and memory required for EMM to provide the forward induction proof. Columns 6-9 report these performance numbers for the Explicit Modeling.

Table 2 . Performance summary on Quick Sort on P2

 2

	N	EMM +PBA	EMM-Proof on Red. Model	Explicit+PBA	Explicit on Red. Model
		FF (orig) Sec	Sec	MB FF (orig)	Sec	Sec MB
	3 91 (167) 10	5	13 293 (37K)	293	2K 274
	4 93 (167) 38	145	40 2858 (37K) 2858	10K 456
	5 91 (167) 351 2316 116	-(37K)	>3hr	NA NA

Proceedings of the Design, Automation and Test in Europe Conference and Exhibition (DATE'05) 1530-1591/05 $ 20.00 IEEE

Conclusions

We have proposed several techniques for verifying embedded memory systems using EMM. We extend the previous EMM approach for a single memory with a single read/write port, to the more commonly occurring memory systems of multiple memories with multiple read and write ports. We also extend the previous EMM approach for falsification to derivation of proofs. We have proposed a precise modeling of the arbitrary initial state of memory, for use in SAT-based induction proofs using BMC. We have also proposed combining PBA techniques with EMM. We showed that using this combined approach, we can identify fewer memory modules that need to be modeled; thereby reducing the model size and verification problem complexity. We applied these EMM techniques on several case studies to show their effectiveness in practice, in comparison to an explicit memory modeling approach. In one case study, EMM techniques also helped to efficiently check invariants, which were then used to prove several properties unreachable.