Guillaume Plassan

Hans-Jörg Peter

Katell Morin-Allory

Shaker Sarwary

Dominique Borrione

Improving the Efficiency of Formal Verification: The Case of Clock-Domain Crossings

Keywords: Formal verification, clock-domain crossing, synchronizers, CEGAR, SOC

We propose a novel semi-automatic methodology to formally verify clock-domain synchronization protocols in industrial-scale hardware designs. To establish the functional correctness of all clock-domain crossings (CDCs) in a system-on-chip (SoC), semi-automatic approaches require non-trivial manual deductive reasoning. In contrast, our approach produces a small sequence of easy queries to the user. The key idea is to use counterexample-guided abstraction refinement (CEGAR) as the algorithmic back-end. The user influences the course of the algorithm based on information extracted from intermediate abstract counterexamples. The workload on the user is small, both in terms of number of queries and the degree of design insight he is asked to provide. With this approach, we formally proved the correctness of every CDC in a recent SoC design from STMicroelectronics comprising over 300,000 registers and seven million gates.

Introduction

Modern large hardware designs typically contain tens of clock domains: different modules use different clocks, adapting consumption and performance to the ongoing tasks, thereby reducing the overall power consumption of the chip.

Moreover, an SoC typically assembles IP blocks coming from various teams, and each block may be optimized for a specific operating frequency. As a result, such architectures create many interconnections between the various clock domains, so-called clock-domain crossings (CDCs). To ensure a correct propagation of data through a CDC, hardware designers have to implement specific protocols and modules: synchronizers.

With the increasing number of CDCs and synchronization protocols as well as the huge complexity of modern SoCs, proving the functional correctness of all synchronizers became a major challenge. While incomplete functional verification methods, such as testing based on simulation, scale for large designs, they are only able to show the absence of functional errors in a subset of the full design behavior. For exhaustively and automatically proving the correctness of functional properties, model checking is the prevalent technique in a modern VLSI design flow.

But, as model checking a property is not scalable on large hardware designs, the question arises whether it is really necessary in practice to have a completely automatic verification procedure. That is, can we somehow take the user into the loop and abandon the high degree of automation of model checking to make formal verification scalable?

This paper addresses this question and proposes a new comprehensive methodology for verifying clock-synchronization properties over industrial-scale SoC hardware designs.

Unlike other semi-automatic approaches that require non-trivial manual work in form of deductive reasoning, our approach produces a small sequence of easy queries that only require local design knowledge from the user. The key idea is to use the CEGAR principle [START_REF] Clarke | Counterexample-guided abstraction refinement[END_REF] as the algorithmic back-end, where we let the user influence the course of the algorithm based on information extracted from intermediate abstract counterexamples. The workload on the user is deliberately kept small both in terms of number of queries and the degree of design insight to be provided.

More precisely, this paper makes the following contributions:

-A general semi-automatic algorithm based on CEGAR-based model checking.

-A heuristic to automatically infer design constraints from abstract counterexamples, which are then proposed to the user. -A comprehensive methodology for verifying CDCs, based on this interaction between the model checking algorithm and the user. -The application of this new methodology to conclusively prove the correctness of all CDCs on a recent industrial SoC design.

The paper continues as follows. Section 2 recalls the CDC challenges and the various synchronizers. Section 3 presents the state-of-the-art CDC verification flow and its limitations. We provide a novel automated flow in Section 4, and the results obtained with it in Section 5. We finally compare our approach with the related works before concluding the paper.

Clock-domain Crossing Issues

A CDC typically manifests itself as a digital signal path between two sequential elements receiving clocks from out-of-phase domains (Figure 1). Even if those clocks have the same frequency, any difference between their phases introduces a latency between their rising edges. This non-predictable behavior is precisely the challenge of designing CDCs.

Multiple problems arise from CDCs [START_REF] Sarwary | Critical clock-domain-crossing bugs[END_REF], and designers need to implement specific structures to avoid any issue [START_REF] Ginosar | Fourteen ways to fool your synchronizer[END_REF]. Consequently, the CDC verification tool must check that all the potential problems have been addressed and corrected.

DATA_IN DATA_OUT

Fig. 1. A simple CDC

Metastability and Multi-flops

The definition of clock domains directly implies that when data changes in the source domain of a CDC, the destination register can capture it at any moment: compliance with the setup and hold time requirements is not guaranteed. Hence, because of a small delay between the rising edges of the two clocks, the data is captured just when it changes, and a metastable value may be propagated (as shown in Figure 2).

Fig. 2. Metastability behavior

The metastability phenomenon has been identified a few decades ago [START_REF] Chaney | Anomalous behavior of synchronizer and arbiter circuits[END_REF]: if a metastable value is propagated through combinational logic, it can lead to a so-called dead system. And it would be very difficult to find the source of this issue after fabrication, as post-production testers do not understand non-binary values.

A first solution would be to introduce a latency in the destination domain, in order to wait for a stabilization of the value. This timing can be estimated by considering the clock frequencies and the production technology, as is commonly performed in the Mean Time Between Failure computation [START_REF] Gabara | Metastability of cmos master/slave flipflops[END_REF]. A single dedicated register could then, if properly sized, output a stable data. However, such synchronizing registers would result in a significant overhead on the circuit size. Another technique [START_REF] Karimi | Detection, diagnosis, and recovery from clock-domain crossing failures in multiclock SOCs[END_REF][START_REF] Leong | Built-in clock domain crossing (CDC) test and diagnosis in GALS systems[END_REF] involves embedding a monitor in the design which detects and corrects metastable values. However, the overhead would also be significant.

The most common solution is to add latency by implementing cascaded registers [START_REF] Ginosar | Metastability and synchronizers: A tutorial[END_REF] (see Figure 3). While this multi-flop structure guarantees within a certain probability that the propagated value is stable, there is no way of telling if it is a '0' or a '1'. Indeed, the data being captured during a change, the multiflop may output the old or the new value during one cycle; then, at the next destination cycle, the new value is propagated. The drawback of this structure is thus a delay in the data propagation.

Coherency with Gray-Encoding or Enable Control

When synchronizing buses, there can be coherency issues: if some bits of a bus have separate multi-flop synchronizers (see Figure 3), it cannot be guaranteed that all these synchronizers require a strictly identical latency to output a stable value. When capturing a toggling signal, some multi-flops may settle to the old value and some to the new one. The resulting bus value may then become temporarily incoherent. If multiple synchronized bits converge on a gate, a transient inconsistent value may even be generated.

DATA_CDC[0] D Q D Q D Q DATA_OUT[0] DATA_CDC[1] D Q D Q D Q DATA_OUT[1] DATA_XOR Fig. 3. Bus synchronization
For instance, in Figure 4, two bits of DATA CDC are toggling at the same cycle. After being synchronized by separate multi-flops, the DATA OUT bus value is not consistent anymore. If both bits are converging on an exclusive OR gate, a glitch can be observed. However, we can add some encoding so that only one bit can change at a time [START_REF] Cummings | Clock domain crossing design & verification techniques using systemverilog[END_REF] (Gray-encoding in the case of a counter, or mutual exclusion in some other cases). Even if the multi-flops stabilize this toggling signal with different latencies, the bus output value will either be correct regarding the previous or the next cycle. Thus, no false value is propagated. This can create some data loss, but avoids incoherency.

An alternative solution is using a control signal connected to the enable pin of the destination registers (Figure 5). This CTRL signal is set to '1' only after DATA IN stabilizes. Hence, no metastability can be propagated in the destination domain, and there is no need for further resynchronization [START_REF] Cummings | Clock domain crossing design & verification techniques using systemverilog[END_REF]. Of course, this 'stable' information comes from the source clock domain, so this control signal must be resynchronized in the destination domain (here with a multi-flop). Note that different synchronization schemes are derived from this structure. The control signal is here connected to the enable pin of the flop (the

DATA_CDC[0] DATA_OUT[0] DATA_XOR CLK2 DATA_CDC[1]
DATA_OUT [START_REF] Alkassar | Formal correctness of an automotive bus controller implementation at gate-level[END_REF] Fig. 4. Bus incoherency behavior selection of a recirculation mux), but it could also be connected to a clock-gate enable, or even an AND gate on the data path.

DATA_IN DATA_OUT

Fig. 5. Enable-based synchronization

Data Loss and Handshake

The enable-based synchronizer structure only propagates stable data. However, if the source register keeps sending data, the destination might wait for their stability and lose some packets. The source should then wait for the data to be captured before sending a new one. This can be done with a handshake protocol using request/acknowledge signals, as shown on Figure 6. (In Figures 5, 6 and7, clock domains are shown in blue or red, data is in green and control logic is in yellow or purple.)

Performance with FIFO

The delay introduced by handshake protocols may not be acceptable for a highrate interface. Putting a FIFO in the CDC allows the source to write and the

D Q DATA_IN ACK REQ D Q D Q Q D Q D D Q Q D D Q E E
EN DATA_OUT Fig. 6. Handshake synchronization destination to read at their own frequencies, and increases the data propagation efficiency. In a FIFO, all the previous schemes are implemented (see Figure 7). The main controls of the CDC are the write and read pointers, which need to be Gray-encoded before being synchronized by a multi-flop. In order to activate the source or destination access, global write and read control signals can be implemented in a handshake protocol. Using a FIFO implies some data latency (caused by the handshake and the resynchronization of pointers), but allows a higher transfer rate. All the previously mentioned issues are avoided (metastability, coherency, data loss), but its complexity makes the FIFO the most difficult synchronizer to design and verify.

DATA_IN RD_PTR D Q D Q Q D Q D D Q E D Q E WR_PTR one-hot WR FSM RD FSM D Q E WRITE READ DATA_OUT DATA_CDC Fig. 7. FIFO synchronization
While some hardware bugs can sometimes be resolved by the firmware or software layers, incorrect synchronizers typically lead to non-correctable, so-called chip-killer bugs. To guarantee the absence of CDC issues in a design, a methodology is needed to check that all the necessary synchronizers are implemented, and that their protocol is followed (Figure 8).

Identified Pattern

Conclusive Unknown

Model Checking

Structural Checks

After register-transfer-level (RTL) synthesis, on a net-list, it seems easy to structurally detect a CDC between two registers, and even to detect a multi-flop. In contrast, for complex FIFO protocols, identifying the correct control logic is nontrivial. If a single synchronizer structure was used, a proper pattern matching could try to identify it on each CDC. Unfortunately, in industry, many designers create their own synchronizing structures, and the structural library used for pattern matching would never be exhaustive on complex structures such as FIFOs.

In order to provide a robust and automated analysis, state-of-the-art CDC tools provide a more flexible approach which identifies more general patterns (like the one based on enables), without relying on the rigid FIFO or Handshake structures. This is a first quick step to check multi-flops and sort out missing synchronizers. However, a structural approach cannot check protocols and assumptions on the control signal. A functional check must then be run.

Functional Checks

From the recognition of a synchronizer structure, the extracted information is reused to run functional checks. Formal safety properties to be checked are as-sociated to the generic structures we are using, among which:

1. Stability The destination register only propagates DATA CDC when it is stable.

2. Coherency (Gray-encoding check ) At most one bit at a time can change in DATA.

As an aid to the user, these formal properties are embedded in the CDC tools and linked to the matched patterns. When a pattern is detected, the properties are automatically synthesized in hardware, mapped to the corresponding RTL signals and formally checked.

Limitation

After running the structural and functional checks of Figure 8, the user expects to know which data is correctly resynchronized and which is not. However, experience shows that model checking may not achieve a conclusive result on the properties: some of them reach a timeout even after several days. When this occurs, no information is returned on the cause of the timeout, and the designer is left with no clue on the possible presence of a metastability in the design.

It is well-known that inconclusive results in formal verification are caused by the so-called state-space explosion problem which is intrinsic to model checking of hardware designs. In practice, the typical approach to overcome this challenge is, for each property, to extract the CDC logic. The verification is then focused on just a small but relevant part of the design. However, this approach comes with the following issues: First, the verification engineer needs to have a very good understanding of the underlying design, which is not realistic for large RTL models; Then, strong time-to-market constraints do not allow a manual laborintensive selection of appropriate abstractions for each property; Finally, even with such a high manual effort, a conclusive result cannot be guaranteed.

The approach presented in this paper is also based on focusing on a subpart of the design, but tries to overcome the aforementioned issues by following a CDC-oriented methodology that is based on an interaction between the user and a refinement algorithm.

Root Causes of Inconclusive Results

In this subsection, we report on common root causes of inconclusive results we observed in the verification of CDCs.

Operation modes. An SoC can operate in many different modes (initialization, mission mode, test, scan, etc) controlled by configuration signals, the values of which cannot be automatically inferred by the verification tool. The user must then provide functional design constraints such as clock frequencies, static value of configuration signals, etc. to perform the verification on a realistic mode. This method is user time consuming and error prone, as the user may fail to provide some essential signal constraint.

Clock gating. In complex low-power designs, some modules can be enabled or disabled via a clock-gate for power saving. If the clock enable signals take inconsistent values, the tool produces unrealistic failures by exercising unreachable states of the design. The user should provide constraints on the value of the clock enable signals.

Protocols. In addition to design setup, functional assumptions should be given on the primary inputs of the design, e.g., for handshake protocols.

Considering all the above, in all practical cases we encountered, inconclusiveness was primarily caused by missing constraints. But even with all this information -that is not always trivial to write -a model checker may still not reach a conclusive result, due to the design complexity. We need a new approach both to tackle this complexity issue and to identify missing constraints.

User-Aided Abstraction Refinement

The objective of our approach is to avoid the state-space explosion problem in model checking hardware designs. To that end, our key idea is to let the user aid the model checking process by replying yes/no to a series of questions whose answers only require local design knowledge.

Technically, our underlying framework is a counter-example-guided abstraction refinement (CEGAR) [START_REF] Clarke | Counterexample-guided abstraction refinement[END_REF] algorithm: we maintain a sequence of abstractions with increasing precision until a definite result can be established. In contrast to fully automatic CEGAR approaches, the user here influences the refinement process. We therefore call our approach user-aided abstraction refinement (UsAAR). Figure 9 gives an overview on the semi-automatic algorithm in the context of the overall methodology.

Localization Abstractions

Our abstractions are obtained via localization reduction [START_REF] Kurshan | Computer-aided Verification of Coordinating Processes: The Automata-theoretic Approach[END_REF]: we replace some nets in the original design with primary inputs, called cut points. An abstraction A is more precise than an abstraction B if the cone-of-influence (with cut-points) of the property in A is an extension of the one in B.

The rationale for this notion of abstraction is that, in practice, all the relevant control logic for a given CDC is implemented locally. Thus, properties requiring the correctness of synchronizing protocols should have small abstractions that suffice to either prove the property or to reveal bugs.

Figure 10 illustrates the abstraction process for a correct, hard to prove, property. By removing parts of the circuit from the cone-of-influence of the property (keeping only A 1 from COI), and leaving the unconnected nets free, the set of reachable states is enlarged (i.e., it represents an over-approximation). As a result, states in which the property fails (the error states), initially unreachable, may become reachable (A 1 ). In this context, refining the abstraction consists in iteratively adding back some of the removed circuit, and as a consequence reducing the reachable state space (from A 1 to A 2 ), until a sufficiently precise abstraction is obtained (A suff ), for which no error state is reachable. The challenge here is to find that part of the design that can be pruned away without spuriously making any error state reachable.

The Core Algorithm

The algorithmic core of our methodology (Algorithm 1, in pseudo code) is a semiautomatic algorithm which is based on the automatic counterexample-guided abstraction refinement (CEGAR) [START_REF] Clarke | Counterexample-guided abstraction refinement[END_REF] principle. A localization abstraction of the design is incrementally made more precise in a sequence of refinement rounds.

In each round, the safety property is checked on the abstraction: if the property is satisfied, the algorithm terminates with Result "proof"; if a counterexample is found, a refinement heuristic decides whether and how the abstraction should be refined, or it concludes that the counterexample is concretizable, i.e., the counterexample is also valid for the full design, and the algorithm can terminate with Result "fail".

Algorithm 1 UsAAR for a design D and a property P Throughout the algorithm, we maintain a set of constraints C global and a set of nets F . We call F the focus: it induces a localization abstraction D # of design D (Line 5). The constraints C global are used when property P is checked on D # (Line 6). Starting with no constraints (Line 2) and F just holding the nets in the combinational fan-in of P (Line 3), we incrementally add elements to both sets, thereby making the over-approximation more precise. Based on the abstract result R # obtained in Line 6, we either immediately terminate (in case R # = proof ), or continue analyzing the abstract counterexample cex # (in case R # = fail). The next subsection details this analysis.

Analysis of Abstract Counterexamples

In our variant of CEGAR, the refinement heuristic first determines a set of cut points that are logically relevant for the abstract counterexample. This is done by computing (an over-approximation of) the justifiable set of cut points J (Line 11). The validity of the counterexample is independent of any cut point that is not part of J. Intuitively, any net that is not contained in a minimal justifiable set can be set to a random value without invalidating the reachability of the error state. But since computing a minimal justifiable set is a hard problem on its own, heuristics are used to compute a small but not necessarily minimal set. A common technique is to use ternary simulation to identify inputs that do not impact the overall validity of the counterexample.

Once J is obtained, the heuristic Analyze classifies each element in J into specific categories (Line 12): clock, reset, data, control, etc, using a backward traversal of the RTL which starts at the synchronizer pattern. Then, realistic constraints corresponding to each category are inferred. For instance, when encountering a potential setup issue such as a missing clock-gating constraint, Analyze proposes to assume that the control input of the clock-gate is always set to an enabling value. Or if a net is found to be logically irrelevant for the user, Analyze infers a stopper constraint to ensure that the net (and its fan-in) will not be part of any future abstraction. In the asynchronous FIFO of Figure 7, this stopper constraint would be applied on the net DATA IN. Indeed, in this case, the property is independent of the DATA IN value. Only the following control logic is relevant.

All constraints C prop inferred by Analyze are then reported for review (Line 13). In case the user rejects a constraint, the corresponding net is marked for automatic refinement. After the manual classification process, the accepted constraints C acc are added to the set of global constraints C global (Line 20). For all nets that are marked for automatic refinement ref , we extend the focus so that the subsequent abstraction are more precise by additionally comprising those nets (Line 21).

Soundness, Completeness, Validity

The algorithm terminates if either the model checker reports a proof or if no new constraints or nets for automatic refinement can be inferred, in which case a fail is reported (Line 15). The soundness of reported proofs follows straight forward from the fact that our localization abstraction represents an over-approximation. The soundness of reported fails follows from the definition of the justifiable set: the abstract counterexample cex # only depends on nets within the focus, i.e., on nets that were not abstracted out or for which the user provided constraints. Hence, cex # remains a valid counterexample for any greater set F ⊃ F , and in particular, on the full design D.

In every non-terminating round, we either monotonically make the abstraction more precise or constrain the design behavior. Hence, since the underlying design is finite, the algorithm terminates. Completeness follows from the fact that the algorithm either terminates with a sufficient abstraction, or it ultimately reaches the full design, i.e., D # = D.

When manually adding constraints one runs the risk of over-constraining the design's behavior, which can lead to vacuous proofs. However, our UsAAR methodology is designed to minimize the risk of over-constraining. The setup constraints inferred by our heuristics are combinational and structurally close to the CDC control logic, which makes them easy for the user to review. Then, they do not over-constrain but ensure that the design does not exhibit spurious behavior. On the other hand, stopper constraints (i.e., static cut points) are conservative: they lead to an over-approximation that preserves all safety properties.

Case Study

We applied our new methodology on two hardware designs: a small parametric FIFO and a complex SoC from STMicroelectronics. The first one reveals the benefits of the different steps of the flow. The second one proves the validity of the methodology on an SoC from industry.

Asynchronous FIFO

Design Presentation. This hardware design includes a FIFO similar to the one presented in Figure 7. To mimic a state-space explosion on the DATA IN and WRITE paths of the source domain, an FSM was implemented with a selflooping counter on 128 bits, along with some non-deterministic control logic. Also, the source and destination clocks are enabled by sequential clock-gates, controlled by two independent primary inputs.

This design is parameterized by the width of the data being propagated, and by the depth of the FIFO. By varying these two size parameters, we increase the design complexity and analyze the corresponding performance of the methodology.

Results

. Using an industrial tool to structurally analyze the design, three formal properties were extracted.

-A data stability property is created on signal DATA CDC.

-Two coherency properties are extracted on the address buses after synchronization, one on RD PTR and one on WR PTR. Indeed, the write and read pointers are synchronized with multi-flops, and should then follow Grayencoding (see Section 2.2).

To verify them, the open source model checker ABC [START_REF] Brayton | ABC: an academic industrial-strength verification tool[END_REF] is used with the engines PDR [START_REF] Eén | Efficient implementation of property directed reachability[END_REF] and BMC3 [START_REF] Biere | Symbolic model checking without BDDs[END_REF] in parallel. For each property, the runtime limit for timeout is set to 15 minutes (denoted T/O in Table 1). We run the experiments on a workstation with 24 Intel Xeon 2.6GHz CPUs and 220GB of memory. Four different schemes are applied to generate the results in Table 1: 1. Standard: Model-checking each property on the full (non-abstracted) design. 2. CEGAR: A UsAAR variant where we reject all constraints. It can be seen as a reduction of UsAAR to standard CEGAR. 3. UsAAR: The full semi-automatic algorithm presented in Section 4 including automatic refinement and constraint inference together with manual constraint classification. 4. Standard w/ constraints: Repeated run of the standard scheme with all the accepted constraints from the UsAAR scheme.

A first observation is that the coherency properties are proved in less than a second in all four schemes and variations of the design. This is not surprising considering that the Gray-encoding implemented in this design does not depend on any non-deterministic control logic. Henceforth, we will then focus on the data stability property.

The standard scheme is not able to prove the property in all 35 variations of the design (Column "Standard"). Using the simple CEGAR approach, the property is proved in all variations within 4 to 15 minutes (Column "CEGAR"). Interestingly, the proof runtime is stable when the FIFO depth is fixed and the data width increases. By looking at the last abstraction exercised, we notice that DATA IN is always abstracted out. Its value does not depend on the source logic. Hence, heuristics from the proof engine inferred that the proof does not depend on the data value, which make the analysis as simple for 8 bits as it is for 128 bits. Actually, even if the source logic of the data was greatly more complex, the CEGAR result would be the same.

Along the UsAAR run, two static constraints are automatically inferred on the enables of the clock-gates. Because having a non-deterministically enabled clock is not a realistic design behavior, we decide to accept them. As a result, the stability property is solved in all 35 variations of the design within 10 seconds each (Column "UsAAR"). Same as with simple CEGAR and contrary to the standard scheme, the complexity of the data source logic is irrelevant for the proof.

Interestingly, even when applying the inferred enabling constraints on the standard scheme, not all properties can be solved (Column "Standard w/ constraints"). Also in this case, by comparing with column "UsAAR", we notice that the runtime is always higher than when using both the inferred constraints and CEGAR. This observation along with Figure 11 points out the importance of using both CEGAR and constraints in order to reach a conclusive result.

CPU Subsystem

Design Presentation. The second case study is a complex SoC hardware design from STMicroelectronics, intended for a gaming system. It is a low-power architecture, with a state-of-the-art quad-core CPU and many different interfaces. In total, it holds over 300,000 registers and 7 million gates. The CDC setup is mainly done in a clock and reset control module, which selects configurations for the whole system among its 38 clock domains and 17 primary resets. However, many configuration signals (such as clock-enable signals) are not controlled by this module. Since the design has a Globally Asynchronous Locally Synchronous (GALS) intent, CDC signals are always synchronized in the destination module. Figure 12 gives an overview of some synchronizations around the CPU. Data communication with the CPU environment (the rest of the SoC) is synchronized by a customized FIFO with a 4-phase protocol based on the one described in Section 2.4, with additional low power and performance optimizations. Only one communication is shown in Figure 12, among the ten in each direction. The figure also shows the communications with the clock and reset controller, and the handshake with the low power management block. Note that the CPU is one central module which, due to its complexity, is likely to cause a timeout in the model checking algorithm when considered in its entirety.

Many synchronizers (mostly FIFOs) are split between modules of this subsystem. Hence, we cannot proceed in a module-by-module CDC analysis. Working at this hierarchy level is particularly relevant for us. Results. We used an industrial tool to structurally analyze the STMicroelectronics design. Only some straightforward constraints regarding reset and clock setup were applied; we did not use any other design insight. All clock multiplexers were constrained to select the mission-mode clock, and static primary inputs were constrained to the value given in the design specification (subsystem configuration). The structural analysis identified several thousand synchronizers, most of them multi-flops which do not need a functional check. It also extracted 78 stability and 47 coherency properties. We verify each extracted property in the same four schemes that were presented previously.

Table 2 shows the results for model checking the stability and Gray-encoding properties. Without any automatic refinement, the standard scheme can only prove 40 out of 125 properties (Column "Standard"). After increasing the timeout limit to several hours, the same results are obtained. Using automatic refinement (the CEGAR scheme), 33 more properties can be proved (Column "CEGAR"). Also, it should be noted that all proofs from the standard scheme get confirmed by the CEGAR scheme. CEGAR proves to be particularly efficient for proving Gray-encoding properties, as the encoding logic is generally local to the synchronizer.

The most striking observation, however, is that during the first UsAAR run, 40 setup constraints are automatically inferred and are all easily accepted. These By reviewing them, we observe spurious behaviors in the handshakes, which are fixed by adding 22 missing Boolean assumptions enabling the protocols. Indeed, in some cases the WRITE or READ of the FIFO represents an information coming from the CPU, and would depend on a software execution. When these signals are abstracted out, they take random values which do not follow the handshake protocol, hence creating a failure. After consulting STMicroelectronics, we decide to constrain them to a realistic behavior. Here, the worst case would be to set them to '1' which would mean the CPU always transfers data. We stress the fact that no deep design knowledge is needed during this process, and the constraints represent a realistic design behavior.

With these new constraints, the second UsAAR run is able to conclude all 125 properties correctly. Compared to the fully automatic approaches, the final UsAAR proof runtime is accelerated by more than 20x. In fact, the most difficult property concludes in only 7 minutes.

Finally, the last column shows that having the proper constraints is not sufficient to get proofs; the efficiency of UsAAR indeed relies on the combination of automatic CEGAR and manual constraint classification.

Regarding the size of the abstractions: on the full design, some properties have a cone-of-influence of more than 250,000 registers. Interestingly, our variant of CEGAR is able to find sufficient abstractions containing only up to 200 registers. This ratio confirms our assumption that only the local control logic has a real influence on the correctness of a CDC property.

Overall, a relevant metric to score the different flows would be the total time spent by the verification engineer starting with the design setup and ending with achieving conclusive results for all properties. It would allow us to conclude on the complexity and usability of different methodologies, as for instance the manual extraction and constraining explained in Section 3.3. However, this time depends very much on the design complexity, reuse, and user insight. Such an experiment would assume the availability of two concurrent verification teams on the same design, an investment that could not be made by our industrial partners.

Related Work

The implementation of CDC synchronizers recalled in Section 2 is well known in the hardware design community. Tools for verifying such synchronizers are provided by leading EDA vendors (Synopsys SpyGlass CDC [START_REF]Synopsys: Spyglass CDC. Online[END_REF], Mentor Questa CDC [START_REF]Mentor Graphics: Questa CDC. Online[END_REF], Real Intent Meridian CDC [START_REF]Real Intent[END_REF], . . . ). Most of these tools provide a verification flow including structural checks up to the generation of related formal properties.

Academia is also active in this research area. Some approaches focus on functionally verifying CDC synchronizers; e.g., Burns et al. proposed a new verification flow using xMAS models [START_REF] Burns | GALS synthesis and verification for xMAS models[END_REF]. However, the user needs to define the boundaries of the synchronizers, which is not scalable.

Kwok et al. presented a verification flow [START_REF] Kwok | Using assertion-based verification to verify clock domain crossing signals[END_REF] purely based on a structural analysis that matches parts of the design with a property library to generate assertions. These assertions can be model checked for functional verification. Litterick proposed a similar flow [START_REF] Litterick | Pragmatic simulation-based verification of clock domain crossing signals and jitter using SystemVerilog Assertions[END_REF], replacing model checking by simulation on SVA assertions. Kapschitz and Ginosar published an overview [START_REF] Kapschitz | Formal verification of synchronizers[END_REF] on the general CDC verification flow, showing the need for multiple clock modeling and formal verification. However, they did not detail how synchronizers can be identified, nor their flow automation, nor how to deal with a high design complexity.

Li and Kwok described a CDC verification flow [START_REF] Li | Automatic formal verification of clock domain crossing signals[END_REF] similar to ours, including the extraction of a formal property from an automatic structural identification. They performed abstraction refinement along with synthesis to prove some properties, but the underlying techniques were not explained in detail. In their flow, inconclusive properties after the abstraction refinement are promoted to the top-level and the user needs another methodology to proceed with the formal verification.

Recently, Kebaili proposed to improve the structural checks in order to detect the main control signals of the synchronizer [START_REF] Kebaili | Clock domain crossing formal verification: a meta-model[END_REF]. The properties to be verified would only rely on these control signals (with a handshake-based protocol), hence avoiding the state-space explosion in the data path.

In other hardware verification domains, some methodologies combine manual with automatic reasoning. For instance, for verifying the FlexRay physical layer protocol, Schmaltz presented a semi-automatic correctness proof [START_REF] Schmaltz | A formal model of clock domain crossing and automated verification of time-triggered hardware[END_REF] in which the proof obligations are discharged using Isabelle/HOL and the NuSMV model checker. This proof was also applied to larger verified system architectures [START_REF] Alkassar | Formal correctness of an automotive bus controller implementation at gate-level[END_REF].

Localization abstractions and related refinement techniques were pioneered by Kurshan in the 1980s and eventually published in the mid 1990s [START_REF] Kurshan | Computer-aided Verification of Coordinating Processes: The Automata-theoretic Approach[END_REF]. The fully automatic variant of the CEGAR principle was introduced by Clarke et al. in the context of over-approximating abstractions defined through state-space partitionings [START_REF] Clarke | Counterexample-guided abstraction refinement[END_REF][START_REF] Clarke | Model checking and abstraction[END_REF]. The works by Andraus et al. propose a CEGAR approach for data-paths in hardware designs [START_REF] Andraus | Refinement strategies for verification methods based on datapath abstraction[END_REF][START_REF] Andraus | Automatic abstraction and verification of Verilog models[END_REF]. Orthogonal to our approach, their abstractions are obtained by replacing data-path components by uninterpreted functions which, in turn, also requires a more powerful model checker based on SMT. Our methodology can be seen as an extension of these works mentioned above, as it enables the integration of user insight into the refinement process.

Conclusion and Outlook

This paper presents a complete formal verification flow for conclusively proving or disproving CDC synchronizations on industrial-scale SoC hardware designs. Our core contribution is a semi-automatic model checking algorithm, where the user aids the (otherwise fully automatic) verification process by classifying a sequence of automatically inferred constraints.

We demonstrated the efficiency of our approach on an STMicroelectronics SoC design which was persistently difficult to verify: prior approaches required to manually extract the cone-of-influence of the synchronizers, which resulted in a tedious (and costly) work for verification engineers.

In contrast, our new methodology allowed the full verification without requiring any deep design knowledge. This very encouraging practical experience suggests that we identified an interesting sweet-spot between automatic and deductive verification of hardware designs. On the one hand, it is a rather easy manual task to classify simple design constraints that refer to single nets where, on the other hand, this information can be crucial to guide an otherwise automatic abstraction refinement process.

Another positive side-effect of our methodology is that it gradually results in a functional design setup. Note that all accepted constraints (except the stopper constraints) do not depend on a certain property, but reflect general design properties and are therefore globally valid. This does not only speed-up the overall CDC verification time, when constraints are reused while verifying multiple properties, it also helps further functional verification steps in the VLSI flow. For instance, the same design constraints can be reused for functionally verifying false and multi-cycle paths.

As a next step, we plan to improve the constraint inference in order to generate sequential SVA assumptions. This feature would guide the user into creating more complex constraints representing realistic design behaviors without decreasing the proof coverage. Also, we investigate into other functional properties. The long-term goal is to extend our methodology to many critical functional verification steps in the VLSI flow.

Fig. 8 .

 8 Fig. 8. CDC formal verification methodology

Fig. 9 .Fig. 10 .

 910 Fig. 9. The UsAAR algorithm of our CDC verification methodology

Fig. 11 .

 11 Fig. 11. comparison for FIFO depth 8

Fig. 12 .

 12 Fig. 12. Overview on the synchronizers at the interface of the CPU

Table 1 .

 1 CDC properties proof CPU runtime (in sec) on the asynchronous FIFO

	FIFO depth Data width Standard CEGAR UsAAR	Standard w/ constraints
		8	T/O	389	7	22
		16	T/O	390	7	35
	3	32	T/O	392	7	66
		64	T/O	390	7	870
		128	T/O	391	7	T/O
		8	T/O	592	6	15
		16	T/O	591	6	28
	4	32	T/O	594	6	57
		64	T/O	593	6	145
		128	T/O	594	6	243
		8	T/O	641	7	14
		16	T/O	651	7	53
	5	32	T/O	641	7	69
		64	T/O	640	7	180
		128	T/O	693	7	374
		8	T/O	558	7	13
		16	T/O	558	7	55
	6	32	T/O	563	7	62
		64	T/O	563	7	203
		128	T/O	562	7	414
		8	T/O	574	7	10
		16	T/O	574	7	49
	7	32	T/O	575	7	68
		64	T/O	574	7	150
		128	T/O	575	6	841
		8	T/O	589	7	11
		16	T/O	590	7	36
	8	32	T/O	579	7	60
		64	T/O	580	7	150
		128	T/O	580	7	463
		8	T/O	868	9	14
		16	T/O	863	9	43
	9	32	T/O	868	9	74
		64	T/O	864	9	210
		128	T/O	865	9	475
	TOTAL PROVED	0	35	35

Table 2 .

 2 Results on the CDC stability and Gray-encoding properties enables (scan or test enables, internal configuration signals, ...), and also internal soft resets and clock-gate enables which were missing in the design specification. It leads to 87 proved properties and provides counterexamples for the remaining 38. Note that in those abstract counterexamples, many irrelevant signals are automatically hidden using the justifiable subset, which makes debugging easier.

			Standard CEGAR	UsAAR first run second run w/ constraints UsAAR Standard
	Stability	# Proof # Fail # Inconclusive CPU time [min]	29 0 49 771	31 0 47 734	45 33 0 583	78 0 0 31	43 0 35 557
	Gray-enc.	# Proof # Fail # Inconclusive CPU time [min]	11 0 36 540	42 0 5 86	42 5 0 27	47 0 0 15	11 0 36 540
	include global interface

Acknowledgement

We wish to thank Mejid Kebaïli and Jean-Christophe Brignone from STMicroelectronics for reviewing and confirming the validity of our methodology.


Alexander W Rath

Sebastian Simon

Volkan Esen

Wolfgang Ecker

Earth Mover's Distance as a Comparison Metric for Analog Behavior

Keywords: Mixed-signal verication, Analog behavior, Earth mover's distance, Pearson correlation coecient, Fréchet distance

Evaluating the outcome of analog simulations is a common, mostly manually carried out task in the pre-silicon verication process of mixed-signal ICs. Its non-automated nature makes it an error-prone and time-consuming procedure. For this very reason, we introduce a novel approach for performing this evaluation automatically resulting in signicantly reduced turnaround times as well as a considerably increased reliability of verication results. The presented concept is motivated by an algorithm that is used in optical pattern recognition and is called Earth Mover's Distance. Furthermore, we compare our approach with already existing algorithms, namely Fréchet Distance and Pearson Coecient, in order to analyze its capability. Finally, we present a case study in which we prove the algorithm by applying it to the results of a mixed-signal simulation at chip-level demonstrating the eciency of our approach.

Introduction

Due to better technology scaling of digital blocks compared to analog blocks more and more parts of the analog implementation of modern IC designs are shifted to the digital domain. However, certain analog components are still indispensable, leading to mixed-signal designs. Hence, the demand for comprehensively verifying such designs is continuously growing and compared to the highly automated verication methodologies in the digital domain, pre-silicon verication in the analog domain usually implies a substantial amount of manual work and computational eort.

On analog module level, pre-silicon verication primarily targets the analysis of electrical characteristics as for instance gain, distortion or input resistance.

Although determining electrical characteristics is also targeted on chip top and system level, conrming the functional correctness and the application tness of the design by means of simulation is the main goal in this regard. The authors of [START_REF] Khan | From spec to verication closure: a case study of applying uvm-ms for rst pass success to a complex mixed-signal soc design[END_REF], e. g., point out that it is still a common practice to manually inspect waveforms when performing the latter. This eectively obstructs the usage of automated checking and regression-based simulations inevitably leading to an increased error-proneness as well as vast expenditures of time. Therefore, they advise to leverage automated solutions to overcome these problems. We were also able to identify these diculties and we still see room for improvement in this eld. For that reason we set ourselves the goal to oer an approach which enables an automated way of comparing analog behavior and allows mixed-signal system level functionality to be veried in a regression-based way.

The contribution is structured as follows. First, we give an overview of related work that covers approaches for comparing analog behavior. Their results form the basis for the motivation of our work. Following this, we explain the theoretical principles of our developed approach. In Section 4 we select two competitive algorithms and dene a number of comparison criteria in order to show the strengths of our approach. Finally, a case study is outlined in which we point out the achieved benets.

Related Work

If analog behavior of a design shall be checked, one of the most common approaches is to make use of analog assertions. There are dierent works [START_REF] Yang | Mixed-signal system-on-a-chip (soc) verication based on systemverilog model[END_REF] [START_REF] Neumann | Uvmbased verication of smart-sensor systems[END_REF] which successfully apply this technique for mixed-signal verication. However, assertions generally lack in abstraction since they have to be dened at signal level. Apart from that, they can usually be applied to check only one particular property of the behavior and are therefore highly application-specic.

Further works, which deal with this topic, are presented in [START_REF] Sharma | Predicting the correlation between analog behavioral models and spice circuits for robust soc verication[END_REF][1] [START_REF] Khan | Metric driven verication of mixed-signal designs[END_REF]. They propose approaches which are based on application-specic checkers. These checkers continuously monitor and evaluate circuit characteristics like, for instance, openloop gain or output noise. However, their solutions require a recurring eort for the development of checkers since they have to be elaborated and implemented for each design characteristic.

Due to the aforementioned deciencies it is necessary to look for more generic approaches. For this reason we investigated several metrics that are capable of determining the similarity between discrete signals. One frequently used metric is, for instance, the Pearson correlation coecient (PC). The authors of [START_REF] Rath | A transaction-oriented UVM-based library for verication of analog behavior[END_REF] demonstrate how to employ this measure for the purpose of mixed-signal ver-

ication. An overview of other potential metrics like quadratic mean error or

Fréchet distance (FD) can be moreover found in [START_REF] Ohlendorf | Comparing Two Analog Waveforms -A Trivial Task?[END_REF]. Their results marked the starting point of our work, in which we strove for nding a better suited similarity measure. This newly developed approach is presented and assessed in the subsequent sections.

Earth Mover's Distance

The algorithm we propose is based on the so-called earth mover's distance (EMD). This measure is widely used in the eld of content-based image retrieval and is capable to determine the degree of similarity between two distributions.

An essential part of this algorithm is the repetitive application of a ground distance. Therefore, we rst show how to construct an appropriate ground distance before dwelling on the overall concept of our EMD approach.

Ground Distance

In order to quantify the similarity of analog signals it is necessary to operate on discrete-time signals. A discrete-time signal x[i] ∈ R is a series of data with the discrete time i ∈ N 0 and i < n, where n ∈ N is the number of sample points, i. e.

the length of the signal.

In this publication, however, we rely on an alternative denition that regards the signal x[i] as a vector x ∈ R n :

x = (x 0 , . . . , x i , . . . , x n-1 )

= (x[0], . . . , x[i], . . . , x[n -1])
For our ground distance δ G (x i , y j ), we claim the following fundamental requirement:

The ground distance should be bounded to the interval [0, 1], as it can be shown that a bounded ground distance is a prerequisite for the EMD to be bounded as well.

Several publications [8][9][10] utilize the Euclidean distance |x i -y j | as ground distance. This measure is obviously not compatible with the requirement of boundedness. However, there are methods to subsequently bound such distances, e. g. one could use a division by a parameter that incorporates information about maximum and minimum signal values. Alternatively, one could apply an appropriate function like hyperbolic tangent to it. All these methods have the crucial drawback that the resulting distance functions still treat pairs (x i , y j ) of big values dierently than pairs of small values, although the ratios of the pairs are the same. For example consider

x 0 = 1000

y 0 = 900 = x 1 = 10 y 1 = 9 , but tanh |x 0 -y 0 | ≈ 1 = tanh |x 1 -y 1 | ≈ 0.1
This phenomenon eectively cancels out all sections of the involved signals where the signal's values have a relatively small magnitude. Thus, we claim another requirement:

The magnitude of the ground distance's arguments should not aect the result, i. e. the ground distance has to be scale-invariant, such that the following property holds:

δ G (x i , y j ) = δ G (ax i , ay j ), a ∈ R * (1)
In order to fulll this requirement, we drop the Euclidean distance and use a scaled version of the Tanimoto distance [START_REF] Theodoridis | Pattern Recognition[END_REF][12] instead:

δ T (x i , y j ) = -0.75•xi•yj x 2 i +y 2 j -xi•yj + 0.75 if (x i , y j ) = (0, 0) 0 else (2)
A 3D-Plot of the function is shown in Fig. 1.

Tanimoto distance

There are a number of important properties to be mentioned about the scaled Tanimoto distance: It is limited to the interval [0, 1] and becomes 0, whenever x i = y j . Also, it becomes 1 if the arguments are equivalent in magnitude, but dier in sign (for

x i = 0): δ T (x i , -x i ) = 1.
Furthermore, it is continuous for (x i , y j ) = (0, 0) and it is scale-invariant, i. e. the distance does not depend on the order of magnitude of the arguments.

Therefore it satises Equation 1.

Since the scaled Tanimoto distance does not take the position of the elements

x i and y j into account, we need to extend it. This extension is done by calculating the dierence between the positions normalized to the biggest possible dierence n -1. The extension and the scaled Tanimoto distance are then combined using the hypot function. Thus, the ground distance is dened as follows:

δ G (x i , y j ) = 1 √ 2 • δ T (x i , y j ) 2 + (i -j) 2 (n -1) 2 (3)
The division by √ 2 is required to retain the limitedness to the interval [0, 1]. Note that this expression can only be applied for n > 1. For the very unusual case that n = 1 we set δ G (x i , y j ) = δ T (x i , y j ).

Algorithmic Concept

The earth mover's distance is an approach for measuring the distance between two multi-dimensional distributions. Informally, if one must successively transport soil from one pile to another in order to equalize them, the earth mover's distance calculates the minimum cost for the total transport. The distributions are also called signatures and represent weighted feature vectors of both signals

x and y. In the following the concept of this approach, which is based on [START_REF] Cohen | Finding Color and Shape Patterns in Images[END_REF], shall be explained.

Given are two signatures X and Y where x i , y j denote elements from the respective feature vectors x and y. Each signature consists of n clusters.

X = {(x 0 , w x0 ), . . . , (x n-1 , w xn-1 )} Y = {(y 0 , w y0 ), . . . , (y n-1 , w yn-1 )}
For each element x i , y j a particular weight w xi , w yj can be assigned. In our case a constant weight W is sucient since no element shall be prioritized:

W = w xi = w yj = 1 n 0 ≤ i ≤ n -1, 0 ≤ j ≤ n -1 (4)
Moreover the possibility for transports between both signatures is dened as

ow F = [f ij ],
with f ij the ow between x i and y j . Now the idea is to nd a ow F that minimizes the costs C for the overall work:

C(x, y, F ) = n-1 i=0 n-1 j=0 δ G (x i , y j ) • f ij (5)
For our ground distance we chose the combined distance from Equation 3 since this distance can be used for scalars and is bounded above and below.

The optimization problem in Equation 5 must furthermore satisfy the following constraints where constraint 79 can be simplied according to our assumption in Equation 4:

f ij ≥ 0 0 ≤ i ≤ n -1, 0 ≤ j ≤ n -1 (6) n-1 j=0 f ij ≤ w xi = 1 n 0 ≤ i ≤ n -1 (7) n-1 i=0 f ij ≤ w yj = 1 n 0 ≤ j ≤ n -1 (8) n-1 i=0 n-1 j=0 f ij = min   n-1 i=0 w xi , n-1 j=0 w yj   = 1 (9)
Constraint 6 allows only unidirectional ows from X to Y. Constraint 7 ensures that the weight in Y matched to x i does not exceed n -1 , while constraint 8 ensures that also the weight in X matched to y j does not exceed n -1 . Finally, constraint 9 forces the total amount of weight matched to be equal to the overall weight of each signature.

In summary this particular metric consists in solving the following transportation problem for a pair of distributions on condition that the above-stated constraints are satised:

d EM (x, y) = min F =[fij ] C(x, y, F ) (10)
This expression represents a linear optimization problem. Hence, we can solve it by an appropriate algorithm like the simplex method. However, this method shows an exponential worst-case but polynomial average complexity [START_REF] Klee | How good is the simplex algorithm?[END_REF], which in turn has a determining inuence on the overall performance of this measure.

The results for d EM eventually yield values within the interval [0, 1] where 1 symbolizes complete dissimilarity and 0 a full match.

Assessment

In order to assess the eciency of EMD, we compare its behavior with two other algorithms mentioned in Section 2; the Pearson correlation coecient and the Fréchet distance.

In this section we describe how we carried out the assessment and discuss its results. The assessment setup consists of a set of deviation algorithms that are used to generate distorted variants of a given source signal as well as implementations of the EMD, the PC and the FD that compare the source signal with its distorted variants. In this way, we can analyze the behavior of the dierent algorithms with respect to various types of signal deviations.

Deviations

A deviation D(x i , p) is dened as a function that maps the elements of a signal x to the elements of a signal y of the same length:

y i = D(x i , p), (11)
where p ∈ R is the severity of the deviation.

In addition, we introduce the following symbols for the sake of readability:

The amplitude x of a signal x

x = max i |x i |, (12)
and the swing ∆x of a signal x 1

∆x = max i x i -min i x i (13)
1 Please note that we assume that x is not a constant signal, i. e. ∆x = 0 and hence x = 0. We make this limitation as constant signals would unnecessarily complicate Oset The rst deviation to be dened here is the oset. An oset is a constant, global shift of the source signal along the signal axis. Parameter p oset species the severity of the oset:

D oset (x i , p oset ) = x i + p oset • ∆x (14)
In this denition, the actual oset is p oset • ∆x. This causes p oset to be relative to the swing of the signal. The advantage of this denition is that an oset with, say, p oset = 1 is always signicant. This allows for comparing dierent values of p oset independent of the actual signal. Edge Steepness This deviation describes a change in the edge steepness of the signal while retaining the signal's original characteristics:

D edge (x i , p edge ) =        x•tanh p edge •x i x tanh p edge if p edge > 0 x•artanh p edge •x i x artanh p edge if -1 < p edge < 0 x i if p edge = 0 (15)
The applied changes to the signal can be regarded as a three-step process: The values of x are scaled to the interval [-1, 1]. Then, the signal is compressed using tanh or artanh, respectively, and nally, it is rescaled to the original scale. some of the deviation denitions that we give in the following subsections without providing any further insight. For example, consider Equation 14, where ∆x = 0 would cancel out the eect of p oset .

The rst branch using tanh causes the signal's edges to become more convex, while the second branch using artanh causes the edges to become more concave. Neither of both branches is dened for p edge = 0, but it can be shown that lim p edge →0 D edge = x i for both branches. Hence, it makes sense to dene a third branch D edge = x i for p edge = 0, leaving the signal as it is. Examples are illustrated in Fig. 3. Delay The delay is a constant, global shift of the signal along the time axis.

When shifting a signal along the time axis, it is necessary to ll the emerging gap. Here we have chosen to ll the gap with the value x 0 leading to an acyclic delay. Thus, we dene the delay for 0 ≤ p delay ≤ 1 as follows:

D delay (x i , p delay ) = x i-n•p delay if i ≥ n • p delay x 0 else (16)
The severity p delay is relative to the signal's length n.

An example for delay deviation can be found in Fig. 4.

Scaling Scaling means that the signal is vertically stretched or compressed through multiplying its function by a constant factor p scale :

D scale (x i , p scale ) = x i • p scale (17)
Fig. 5 shows the eect of adding scale to a signal. Peak In contrast to any other deviations presented here, a peak is only a local phenomenon. For n being odd, we dene the peak as single spike in the middle of the signal:

D peak (x i , p peak ) = x i + p peak • ∆x if i n 2 x i else (18)
For n being even, we vary the two adjacent points in the middle of the signal:

D peak (x i , p peak ) = x i + p peak • ∆x if i ∈ n 2 -1, n 2 x i else ( 19
)
Examples for peak deviations are illustrated in Fig. 6.

Noise In principal, adding noise to a signal is like adding oset, except that the oset is now random over time rather than constant:

D noise (x i , p noise ) = x i + u i , (20)
where u i is a uniformly distributed random number with

|u i | ≤ p noise • ∆x 2 . ( 21
)
An example for noise deviation is provided in Fig. 7.

Comparable Algorithms

In this section, we present two additional algorithms that we use to evaluate our EMD approach. Pearson Correlation Coecient The Pearson correlation coecient is dened as

s pea (x, y) = n-1 i=0 (x i -x) • (y i -ȳ) n-1 i=0 (x i -x) 2 • n-1 i=0 (y i -ȳ) 2 , (22)
where x and ȳ represent the arithmetic mean:

x = 1 n n-1 i=0 x i and ȳ = 1 n n-1 j=0 y j
The result of s pea is a value in the interval [-1, 1], where 1 indicates a full match, 0 a total mismatch and -1 a full match except the sign.

It can be moreover shown that there is a direct relation between Pearson correlation coecient and normalized cross-correlation. The latter is given in [START_REF] Yang | Fast Template Matching Based on Normalized Cross Correlation with Centroid Bounding[END_REF] and dened as

(x y) norm (j) = n-j-1 i=0 (x i -x) • (y i+j -ȳ) n-1 i=0 (x i -x) 2 • n-j-1 i=0 (y i+j -ȳ) 2 (23)
With the help of this equation it can be seen that Pearson correlation coefcient is equivalent to normalized cross-correlation at position j = 0:

s pea (x, y) = (x y) norm (0)
In other words, an evaluation of the Pearson correlation coecient additionally embraces an analysis of normalized cross-correlation, which in turn is a widely used measure of similarity in the eld of signal processing. Fréchet Distance For discrete time signals, the Fréchet distance can be dened as

d F (x, y) = min α,β max k δ G (x α(k) , y β(k) ), (24)
where α(k) and β(k

) are non-decreasing surjections k ∈ N 0 → [0, n -1].
Values for d F are in the same interval as for δ G . Since we use the ground distance δ G as given in Equation 3, the interval is [0, 1] where 0 indicates a full match and 1 a total mismatch.

The denition in Equation 24 is not very intuitive, which is why a more intelligible explanation featuring a dog and its owner has become popular [START_REF] Yoon | Computation of Discrete Fréchet Distance using CNN[END_REF]:

The Fréchet distance is the shortest length of a leash required for a dog and its owner to walk on two routesrepresented by our signalsfrom one endpoint to the other. Both are allowed to change their speed, but they are not allowed to walk back.

Furthermore, the denition does not indicate how to implement the Fréchet distance. Luckily, [START_REF] Eiter | Computing Discrete Fréchet Distance[END_REF] provides a pseudo implementation for discrete-time signals.

Results

The results of the assessment are shown in Fig. 8. In order to make the metrics comparable, we mapped the results of the FD and the EMD to the interval of the PC by subtracting their results from 1. Thus, 1 indicates a full match, 0 a total mismatch and -1 full match except the sign. Please note that the interval [-1, 0) is only applicable to the PC. The source signal x that was used to generate the results is a sine signal with an amplitude of 1 going over two full periods. Furthermore, n is set to 200. From the results it can be seen that the comparison algorithms judge the delay deviation very dierently. FD and PC react very pessimistic and, thus, suggest that source and deviated signal are hardly related to each other. In contrast, EMD detects the deviation but does not drop very low, indicating that there is still a relation between the two signals. The edge deviation is treated similarly by all algorithms, with FD being somewhat more pessimistic than the others. Noise is detected by all algorithms; again, FD being very pessimistic.

In addition, FD is not able to dierentiate between the noise severities. The oset deviation is detected well by EMD and FD. However, FD shows a peculiar behavior in the sense that it returns bigger values for severity 1 and 10. PC is not sensitive regarding oset. The peak is very well analyzed by PC, while not being detected at all by EMD. The FD detects the peak, however, it can't dierentiate between dierent severities. Scaling is being detected well by EMD and FD, whilst PC is not sensitive, except on the sign. horizontal axis shows the applied algorithms. The vertical axis shows the result of the comparison between the source signal and the deviated signal with the severity p of the deviation indicated by color. A value of 1 on the vertical axis stands for a full match, i. e. the metric states that the signals being compared are identical; 0 stand for a full mismatch, i. e. the metric states that the signals are completely dissimilar; -1 stands for a full match except the sign (note that only PC can produce such a result). For an interpretation of the results, see Table 1.

In order to summarize the assessment, we compressed the results from Fig. 8 into Table 1. That table indicates, whether a metric is able to detect (D) a distortion and whether it can still see a similarity (S) between the original signal and its distorted version. We count a distortion as detected if the average of the absolute value of resulting metric M is signicantly smaller than 1:

D = + if | M | < 0.99 -else (25)
For example, PC can't detect a scale distortion, as all four result in Fig. 8 are ±1 leading to an average of the absolute of 1 ≥ 0.99.

As a criterion for similarity being counted as detected, we dene the average of the absolutes to be greater than 0.66:

S = + if | M | > 0.66 -else (26)
It can be seen that the EMD can detect all kind of signal distortions, except peak. Referencing the explanation of EMD, where soil is transported from one pile to another, the peak is not detected because the amount of work that is needed to transport the peak is low. This is due to the peak being used in our assessment is very narrow, i. e. it does not contain much soil. However, the biggest advantage of EMD is that it is always able to correctly detect similarity between source and deviated signal.

Case Study

In order to test the reliability of the presented approach, we applied the EMD to a chip level verication of a real-world design. This case study is outlined in the following paragraphs. The design we applied the EMD to is micro-controller-based and features a LIN interface and power switches (see Fig. 9). Its application is focused on driving small electric motorse. g. for window lifts or cooling fansin cars.

Application

Being an automotive application, power consumption is of great concern for the design. In order to fulll the requirements regarding power consumption, the design features a sleep mode as well as wake-up mechanisms. The verication of sleep and wake-up on chip level is crucial, since it aects three design domains digital and analog hardware as well as software. The chip level verication was performed as a mixed-signal simulation in which the hand-shaking between the domains and the voltage curves of the power rails were checked for correctness.

The checking was done in such a way that the results of the initial simulation were inspected manually and stored in the le system. The results of all subsequent simulations were then automatically compared against the results of the initial run using EMD.

In Fig. 10, we show the voltage curve of a rail in the power management unit gained during dierent simulations. The rst curve is the one recorded during the initial simulation and serves as a reference for all subsequent simulations. The colored phases have been dened after the initial simulation, such that the automatic comparison of subsequent results with the ones gained during later simulations could be done phase-wise. Curves A to D represent simulation results after several modications to the design.

Results

Table 2, 3 and 4 show the results of the comparison between signal curves A to D and the reference using EMD, PC and FD, respectively. In order to detect a low similarity, we empirically assume a threshold value of 0.97 for each analysis. "Empirically" means that the threshold value, which serves as a pass/fail criterion, is application dependent and is therefore to be dened by verication engineers on a per-circuit basis. Results which fall below this threshold indicate an insucient degree of similarity (i. e. fail) and are marked red in the tables.

First, it can be clearly seen that due to a bug the design does not wake up in curve A, resulting in an EMD value of approximately 0.5. This unintended functional behavior is also detected by the other two metrics.

A less obvious signal deviation can be found in curve B. The obtained results reveal a change of certain capacitors in the design leading to a slightly dierent discharging behavior in phase 3 (EMD ≈ 0.96 and FD ≈ 0.93). For this case PC already shows the rst deciencies since the metric is not able to detect the deviation (PC ≈ 0.99). The aforementioned change of particular external capacitances was actually not a bug, but a specication-compliant adjustment.

Therefore, the reference curve had to be replaced by curve B.

In the third case (signal C), wake-up is triggered at a later point in time from the test bench. In this application, this has no impact on the functional behavior of the design. Therefore, the second active phase, which is consequently being altered by a delay, shall not be agged as too dissimilar to the reference. However, Switching on an external high load during wake-up leads to the signal shape illustrated by curve D. It is characterized by a peak in the fourth phase at 2000 µs, which can be traced back to a short-time voltage sag. Except for the peak, there is no signicant dierence between curve D and the reference signal.

However, PC and FD are again not able to compensate this deviation and would ag a mismatch (PC ≈ 0.86 and FD ≈ 0.87) whereas EMD correctly detects the functionally unchanged wake-up behavior (EMD ≈ 1.0).

While the critical sleep mode-bug in the above-stated mixed-signal design was detected by all three metrics, EMD reveals its strengths in particular when deviations like delay or peak are distorting the signals. In these cases PC and FD are not able to identify correct functional behavior, which in turn conrms our analyses from Section 4. A concluding summary of our results can be found in Table 5. We furthermore observed the aforementioned deciencies when analyzing several other metrics like Euclidean distance, cosine similarity and Hausdor distance, inspiring us with condence that our approach represents the most reliable one.

Conclusion and Outlook

In this contribution we introduced and described a novel technique for the au- Furthermore, we assessed the approach by comparing it with related techniques and presented a case study, in which we applied the approach to a realword project conrming its usefulness and high reliability compared to other metrics.

Aside from the outlined benets in the eld of mixed-signal verication, the developed approach has also high impact on several other topics. It can, for instance, be leveraged to optimize objective functions, which in turn is helpful when performing model calibration. In this case an automated regression could be set up to successively t model parameters of interest. Another eld of application is the regression testing of SPICE-style simulators, which can be used to identify diverging simulation behavior caused by diering simulator versions.

Our future work will focus on the extension of the presented methodology regarding usability and exibility. The long-term goal is to provide a building box that covers the need of verication engineers to simulate and verify mixed-signal designs. This building box shall include methods and techniques for driving, monitoring and checking analog signals, as well as for coverage collection and reference modeling.

  Fig. 1. Tanimoto distance

Fig. 2 5 Fig. 2 .

 252 Fig. 2 depicts the signal change in case of an oset deviation.

9 Fig. 3 .

 93 Fig. 3. Sine signal with deviations in edge steepness.

4 Fig. 4 .

 44 Fig. 4. Sine signal with deviations in delay.

Fig. 5 .

 5 Fig. 5. Sine with deviations in scale.

Fig. 6 .

 6 Fig. 6. Sine signal with deviations in peak.

5 Fig. 7 .

 57 Fig. 7. Sine signal with noise deviation.

Fig. 8 .

 8 Fig. 8. Results of the assessment. Each diagram stands for a type of deviation. The

Fig. 9 .

 9 Fig. 9. Block diagram of the SoC used for our analyses.

Fig. 10 .

 10 Fig. 10. Voltage curves of a power rail in an automotive design during dierent design states gained by chip level simulation. The red phase shows the power-up of the design, green stands for the active state and yellow for sleep mode.

  tomated comparison of analog behavior. The technique tackles the necessity of being able to automatically check the functional correctness of analog and mixedsignal ICs during design and verication. It moreover opens the possibility of reducing verication eorts by avoiding manual and error-prone investigations of waveforms since it can be easily leveraged for regression tests. Beyond that,

Table 1 .

 1 Qualitative analysis of the assessment. The table shows whether an algorithm is able to detect (D) the deviation and whether it still correctly reports a similarity (S) between source and deviated signal.

Table 2 to

 2 [START_REF] Sharma | Predicting the correlation between analog behavioral models and spice circuits for robust soc verication[END_REF] show that the results for PC and FD fall below the predened threshold while EMD is able to compensate this deviation. This observation goes

Table 2 .

 2 Comparison of the curves from Fig. 10 using EMD.

	Signals	Phase 1 Phase 2 Phase 3 Phase 4
	Ref vs Ref	1.0000 1.0000 1.0000 1.0000
	Ref vs A	1.0000 1.0000 0.9999 0.5118
	Ref vs B	1.0000 0.9999 0.9577 0.9998
	Ref vs C	1.0000 1.0000 1.0000 0.9741
	Ref vs D	1.0000 1.0000 1.0000 0.9980

Table 3 .

 3 Comparison of the curves from Fig. 10 using Pearson Correlation Coecient.

	Signals	Phase 1 Phase 2 Phase 3 Phase 4
	Ref vs Ref	1.0000 1.0000 1.0000 1.0000
	Ref vs A	1.0000 0.9920 1.0000 -0.4070
	Ref vs B	1.0000 0.9369 0.9883 0.9998
	Ref vs C	1.0000 1.0000 1.0000 0.5380
	Ref vs D	1.0000 1.0000 1.0000 0.8599

Table 4 .

 4 Comparison of the curves from Fig. 10 using Fréchet Distance.

	Signals	Phase 1 Phase 2 Phase 3 Phase 4
	Ref vs Ref	1.0000 1.0000 1.0000 1.0000
	Ref vs A	0.9998 0.9998 0.9993 0.5009
	Ref vs B	0.9998 0.9989 0.9250 0.9965
	Ref vs C	1.0000 1.0000 1.0000 0.9413
	Ref vs D	1.0000 1.0000 1.0000 0.8718

Table 5 .

 5 Overview of results: EMD is the only metric that correctly detects, i. e. compensates all four deviation scenarios.

	Signal Deviation in phase Reason for deviation	Supposed to be detected? Detected by
	A	4	Bug in the design	yes	EMD, FD, PC
	B	3	Modied external capacitance	yes	EMD, FD
	C	4	Delayed wake-up	no	FD, PC
	D	4	Voltage sag due to temporary	no	FD, PC
			high load
	applying the presented concept consequently leads to signicantly reduced costs
	and speeds time to market.