Laurence Pierre
email: laurence.pierre@univ-grenoble-alpes.fr

Refinement Rules for the Automatic TLM-to-RTL Conversion of Temporal Assertions

Keywords: SoC verification, TLM properties, temporal refinement

Today's systems on chip (SoCs) require a complex design and verification process. In early design stages, high-level debugging of the SoC functionality is feasible on TLM (Transaction-Level Modeling) descriptions. To ease debugging of such SoC's models, Assertion-Based Verification (ABV) enables the runtime verification of temporal properties. In the last design stages, RTL (Register Transfer Level) descriptions of hardware blocks expose microarchitectural details. To gain confidence in the validity of system level properties after this TLM-to-RTL synthesis, transaction level assertions must be reverifiable on RTL models. To address that issue, we propose refinement rules for the automatic system level to signal level transformation of PSL assertions (Property Specification Language, IEEE standard 1850). We sketch the architecture of a prototype tool that automates this refinement, and we give some illustrative examples for a realistic use case.

Introduction

With the growing complexity of today's applications, the design and validation of hardware/software systems on chip (SoC's) become demanding tasks, requiring advanced methodologies. In that context, SystemC TLM (Transaction-Level Modeling) [START_REF] Grötker | System Design with SystemC[END_REF], [START_REF]IEEE, IEEE Std 1666-2005, IEEE Standard SystemC Language Reference Manual[END_REF] has gained acceptance, as it favors architecture exploration and early software development while improving simulation performance [START_REF] Avinun | Validate hardware/software for nextgen mobile/consumer apps using software-on-chip system development tools[END_REF]. As shown on Figure 1, the SoC design flow [START_REF] Le↵tz | A Design Flow for Critical Embedded Systems[END_REF], [START_REF] Rogin | Debugging at the Electronic System Level[END_REF] usually starts from the system specification. From this specification, the global SoC architecture is defined by system architects, and a virtual prototype of the hardware platform can be developed as soon as the functional specification of the IP blocks is available. SystemC TLM enables the description of such virtual platforms [START_REF] Sangiovanni-Vincentelli | Defining platform-based design[END_REF] used as golden reference models of the SoC for further developments [START_REF] Goering | Transaction models o↵er new deal for EDA[END_REF]. More precisely, LT models (Loosely Timed, formerly PV, Programmer's View) have no timing information and are used for early functional and software design, and AT models (Approximately Timed, formerly PVT, Programmers's View with Timing) facilitate performance analysis and architecture exploration [START_REF] Narasimhachar | Methodology for Rapid Development of Loosely Timed and Approximately Timed TLM Peripherals[END_REF]. In later stages of the design flow, RTL (Register Transfer Level) descriptions of hardware blocks are generated, to take into account greater timing accuracy and microarchitectural details. Verification at every abstraction level is a crucial issue, [START_REF] Jindal | Verification of Transaction-Level SystemC models using RTL Testbenches[END_REF] mentions that SoC design verification takes a 60% to 70% of the total product development time, and comments on the consistency of the approach across abstraction layers and on the use of similar testbenches for the early functional validation of TLM hardware/software models and the (co-)simulation of RTL models.

System requirements (expected properties) can be defined in the initial system specification step, to be reused throughout the flow. To alleviate their verification, ABV (Assertion-Based Verification) can be of valuable interest. ABV is the runtime (i.e., simulation-based) verification of formal temporal properties, such as PSL assertions (Property Specification Language) [START_REF]IEEE, IEEE Std 1850-2005, IEEE Standard for Property Specification Language (PSL)[END_REF]. This method is getting widely adopted in industry [START_REF] Foster | Applied Assertion-Based Verification: An Industry Perspective[END_REF] at the RT level, due to the large amount of available tools. For example, in addition to support for PSL assertions in commercial simulation tools (e.g., [START_REF]Mentor Modelsim[END_REF], [START_REF]Cadence Incisive Enterprise Simulator[END_REF], [START_REF]Synopsys VCS[END_REF]), several solutions have been proposed to generate synthesizable RTL assertion checkers from PSL assertions (e.g., [START_REF] Morin-Allory | Horus: A tool for Assertion-Based Verification and on-line testing[END_REF], [START_REF] Boulé | Automata-Based Assertion-Checker Synthesis of PSL Properties[END_REF]). These verification components receive as inputs the same clock signal as the DUT (design under test), and signals that are the operands of the PSL operators in the assertion. They output signals that inform about the satisfaction / violation of the property.

But clearly, SoC verification can also benefit from ABV at the Electronic System Level (ESL), typically for SystemC TLM virtual plaforms. At that level of abstraction, a central need is to verify the satisfaction of properties that specify the functional correctness of communications between the SoC components, and hardware/software interoperability. The method implemented in our ISIS tool [START_REF] Pierre | Dynamic Verification of SystemC Transactional Models (Chapter 22)[END_REF] enables to automatically instrument SystemC platforms with SystemC assertion checkers produced from such transactional properties formalized as PSL assertions. During simulation, those checkers report any property violation. This solution has been applied to industrial use cases e.g., [START_REF] Pierre | Runtime Verification of Typical Requirements for a Space Critical SoC Platform[END_REF], [START_REF] Pierre | Integrating PSL Properties into SystemC Transactional Modeling -Application to the Verification of a Modem SoC[END_REF]. Some other methods have been proposed, for instance [START_REF] Dahan | Combining System Level Modeling with Assertion Based Verification[END_REF], [START_REF] Ecker | Implementation of a Transaction Level Assertion Framework in SystemC[END_REF] and [START_REF] Tabakov | Optimized temporal monitors for Sys-temC[END_REF].

Since TLM-to-RTL SoC synthesis is a complex, partly manual, and errorprone process, it must be possible to reverify, during (co-)simulation of RTL concrete models, the counterpart of the properties checked on TLM golden models. To that goal, assertions should also undergo a refinement procedure (see Figure 1). As will be explained in section 4, they must mainly be adapted to take into account the concretization of the communication channels i.e., interfaces and timing details induced by the corresponding communication protocols (e.g., AMBA AXI or AHB).

Existing Approaches

A less arduous solution could be based on the well-known concept of "transactors", commonly used to create interconnections of hybrid IP blocks or to communicate with RTL components using TLM transactions. Many examples are reported in the literature. In [START_REF] Rose | Advanced Verification Methodology Cookbook[END_REF], "driver" and "responder" components are defined: a driver converts a stream of transactions into pin-level activity, and a responder responds to activity on pins. Figure 2 (a) from [START_REF]System-on-Chip Design -Course Material[END_REF] provides the example of a transactor that concretizes a four phase handshake protocol while converting from transaction to pin-level modelling, and [START_REF] Rose | Transaction Level Modeling in SystemC[END_REF] describes the modeling of a simple peripheral bus at various levels of abstraction, from a TLM-2.0 PV model down to an RTL implementation (Figure 2 (b)): the transactor gets an abstract request from the master in the tlm req rsp channel and sends it over a RT level bus; when it receives a response on the RTL bus it puts the abstract response into the tlm req rsp channel.

(a) Four phase handshake transactor [START_REF]System-on-Chip Design -Course Material[END_REF] (b) TLM master / RTL slave [START_REF] Rose | Transaction Level Modeling in SystemC[END_REF] Figure 2: Examples of TLM-to-RTL "transactors"

Note also that methods have been proposed to automate the creation of transactors. For example in [START_REF] Balarin | Functional Verification Methodology Based on Formal Interface Specification and Transactor Generation[END_REF], interface protocols are specified formally using PSL SEREs (extended regular expressions), and transactors are automatically generated from such a specification, using a SERE to finite state machine transformation. The authors of [START_REF] Janin | CSP Transactors for Asynchronous Transaction Level Modeling and IP Reuse[END_REF] notice that most ESL tools are designed to deal with synchronous interconnects. They discuss asynchronous transaction level modeling and show that CSP (Communicating Sequential Processes) based transactors can be used to perform CSP to TLM-PV and TLM-PV to CSP translations, and that RTL interfaces can also be generated.

A similar concept is part of the UVM, Universal Verification Methodology [START_REF]Universal Verification Methodology tutorial[END_REF] (maintained by an Accellera working group). Figure 3 summarizes the approach for building a UVM testbench. Such a structure enables to verify the behaviour of a RTL description of the DUT using high-level transactions produced by the "sequence" instance. A UVM "agent" connects a "sequencer", a "driver" and a "monitor". The sequencer connects a sequence to the driver, the driver decodes transactions obtained from the sequencer, and the monitor creates transactions based on the activity on the interface of the DUT. The "scoreboard" is the verification component, it implements the specification and verifies the correspondence between the actual and expected outputs. One could envision to embed assertion checkers for PSL assertions inside this verification component (or in similar blocks for other kinds of simulation infrastructures). The assertion checker would receive TLM transactions issued by the "monitor", or a responder, thus checking whether the DUT satifies the TLM assertions (without any transformation) already used to validate its TLM version.

Proposed Alternative

However this latter technical solution would have some limitations. On the one hand, it does not provide the designers with a semantic formalization of the adaptation of their original temporal properties. Indeed an alternative actual assertion refinement, as illustrated on Figure 1, produces new temporal formulas which are adapted, among others, with respect to the timing characteristics of the implemented communication protocol(s). Designers get not only runtime results about the satisfaction/violation of properties, but also a concrete and precise expression (meaning) of the properties that are validated/violated at the RT level. In addition to this accuracy for the specification that drives runtime verification, the availability of explicit refined assertions also enables to go through a certification process if needed (automotive, avionics,. . . ) and to use a formal verification tool (model-checker) to complement runtime verification, if envisaged.

On the other hand, it is worth noticing that components of the SoC could also be concretized progressively in the stepwise TLM-to-RTL design flow. It means that some phases of the verification process may have to consider hybrid TLM/RTL descriptions. In that context, the availability of formal temporal specifications at both levels can improve verification accuracy and ease debugging.

Therefore, as an alternative, we propose the transformation of properties by means of refinement rules. After recalling the principles of ABV at the transactional level, we discuss the challenges of the refinement of temporal assertions and we propose a set of refinement rules. This work extends our original proposal [START_REF] Pierre | Automatic Refinement of Requirements for Verification throughout the SoC Design Flow[END_REF]: some rules are improved, and new rules have recently been developed to consider more complex timing schemes (e.g., the duration of a communication action is not bound). We also sketch the implementation of a prototype tool for the automation of this refinement, and we illustrate with some examples for an industrial use case. Before concluding, we give an overview of the state of the art.

Brief Overview of PSL

PSL shows a high degree of similarity with the other IEEE standard SVA [START_REF]IEEE Standard for System Verilog: Unified Hardware Design, Specification and Verification Language[END_REF], the assertion sub-language of SystemVerilog. However PSL is prefered here because it is multi-purpose, multi-level, and multi-flavor language [START_REF] Havlicek | PSL and SVA: Two Standard Assertion Languages Addressing Complementary Engineering Needs[END_REF] that can easily suit assertions associated with various hardware description languages (HDL) e.g., SystemC. This section only gives a very brief overview of PSL. For more details, we refer the reader to the tutorial [START_REF]Property Specification Language Tutorial[END_REF], and to [START_REF]IEEE, IEEE Std 1850-2005, IEEE Standard for Property Specification Language (PSL)[END_REF], [START_REF] Eisner | A Practical Introduction to PSL[END_REF].

PSL and its Trace Semantics

PSL assertions are built upon four layers. Among them, the Boolean layer provides basic expressions commonly used by the other layers, a Boolean expression is written using the operators of the associated HDL and is evaluated in a single evaluation cycle. The core of the language is the Temporal layer which gives the possibility to describe complex temporal relations, evaluated over a set of evaluation cycles. The Modeling layer can be used to characterize the behavior of design inputs and to model auxiliary variables; its SystemC flavor consists of those declarations and statements which would be legal in the context of the SystemC module to which the PSL assertion is bound [START_REF] Eisner | A Practical Introduction to PSL[END_REF].

Formulas of the FL (Foundation Language) class of the Temporal layer essentially represent linear temporal logic. In [START_REF]IEEE, IEEE Std 1850-2005, IEEE Standard for Property Specification Language (PSL)[END_REF], the semantics of FL formulas is defined with respect to execution traces (words). In the definitions recalled below, the length of a trace v is denoted |v|, the i th evaluation point over v is denoted v i 1 , and v i.. means the su x of v starting at v i .

Traces are built using a sampling expression, also known as "clock expression". In other words, a clock expression determines when temporal assertions are evaluated. Any Boolean expression can be used as a clock expression.

This FL class contains Boolean expressions, Sequential Extended Regular Expressions (SEREs), and formulas built using temporal operators. In particular, if ' and are FL formulas and r is a SERE, then the following are also FL formulas : ¬ ', ' ^ , next! ', ' until! , and r 7 ! '.

The basic temporal operators of the FL class are the next! operator and strong until, denoted until!. The formula next! ' means that ' should hold from the next evaluation point of the trace:

v |= next! ' , |v| > 1 and v 1.. |= '
Roughly speaking, ' until! holds i↵ there exists an evaluation point in the trace from which holds, and ' holds until that point:

v |= ' until! , 9k < |v| s.t. v k.. |= and 8j < k, v j.. |= '
Note that the weak version of this operator, denoted until, is defined as:

' until def = [' until! ] _ always '
Many other temporal operators are defined using the previous ones and Boolean operators, in particular we recall the following ones:

• The formula always ' means that ' must be verified on each evaluation point of the trace.

• The next event!(b)(') formula requires the satisfaction of ' the next time the Boolean expression b holds:

next event!(b)(') def = [¬b until! b ^'] next event(b)(') def = [¬b until b ^']
• Formula ' before! means that ' must hold at least once strictly before holds. It is also expressed with respect to the until operator:

' before! def ' before = [¬ until! ' ^¬ ] def = [¬ until ' ^¬ ]
• The next a![i..j](') operator specifies that ' holds at all cycles of the range i..j, and the next e![i..j](') operator specifies that ' holds at least once within the range i..j.

PSL also supports some built-in functions. Among them, prev() returns the previous value of its argument. If a second argument i is specified, prev() gives the value of the expression in the i th previous cycle.

SEREs represent subordinate behaviours, occurring in successive cycles in the trace. Various operators are supported, among them:

• The concatenation operator (;) is used to build the concatenation r 1 ; r 2 of two SEREs. Its trace semantics is: • The consecutive repetition operator enables the construction of r[⇤] or r[+], the repeated consecutive concatenation of a sequence r (0, 1 or more times for r[⇤], and 1 or more times for r[+]). If a count number is specified, the repeated SERE describes exactly that number of repetitions of r.

v |= r 1 ; r 2 , 9v 1 , v 2 s.t. v = v 1 v 2 , v 1 |=
• The overlapping su x implication operator 7 ! is used to specify that a FL formula holds if some pre-requisite sequence holds.

Simple Examples at the Signal Level

At the synchronous RT level, sampling is usually performed on the rising edges of the DUT synchronization clock i.e., the "clock expression" refers to clock rising edges.

The atomic propositions that constitute the letters of the word (trace) v refer to the values of the signals of the system (e.g., if a letter is made of (a, not b), it means that the current values of signals a and b are 1 and 0 respectively). The Boolean expressions involved in the PSL assertions are conditions over the values of those signals.

Example 1. The following assertion means "it is always true that, if req holds then, starting from two cycles after, grant occurs before end", where req, grant and end are signals of the DUT.

assert ALWAYS (req -> NEXT! [START_REF]IEEE, IEEE Std 1666-2005, IEEE Standard SystemC Language Reference Manual[END_REF](grant BEFORE! end));

Example 2. The property below is part of the specification of an HDLC (High-level Data Link Control) controller IP. It states that, when the receiver is enabled (signal En) and upon reception of an abort sequence (a zero followed by seven consecutive ones on signal Data), the signal AbortFound shall be set high before the arrival of a new frame (signal StartOfFrame): Note that SEREs are commonly used to specify requirements for synchronous RTL designs. As in this latter example, they are relevant for expressing successions of specific input data on successive clock ticks. However, verifications for TLM or hybrid TLM/RTL platforms rather relate to precedences/orders between events, and are therefore expressed by means of temporal operators.

Dynamic Verification and the Simple Subset

Dynamic verification must comply with assertions of the "simple subset" of PSL, which conforms to the notion of monotonic advancement of time. This subset is defined in [START_REF]IEEE, IEEE Std 1850-2005, IEEE Standard for Property Specification Language (PSL)[END_REF] as restriction on the operands of some operators, as follows:

• The operand of a negation operator is a Boolean.

• The operand of a never operator is a Boolean or a Sequence.

• The operand of an eventually! operator is a Boolean or a Sequence.

• At most one operand of a logical or operator is a non-Boolean.

• The left-hand side operand of a logical implication operator is a Boolean

• Both operands of a logical i↵ operator are Boolean.

• The right-hand side operand of a non-overlapping until operator is a Boolean.

• Both operands of an overlapping until operator are Boolean.

• Both operands of a before operator are Boolean.

• The operand of next e is Boolean.

• The FL Property operand of next event e is Boolean.

In fact this definition is more restrictive than actually necessary. Some authors investigated this simple subset and proposed less restrictive variants, such as [START_REF] Ben-David | The safety simple subset[END_REF] that proposes an interesting alternative.

Though the authors target model checking, and therefore concentrate on safety formulas, they define a useful subset of linear temporal logic (LTL) with regular expressions. This subset is called RLTL LV (Regular-LTL "linear violation" -violation can be detected by an automaton on finite words with size linear in the size of the formula). It is defined as follows [START_REF] Ben-David | The safety simple subset[END_REF]:

If b is a boolean expression, r is an RE and ', ' 1 and ' 2 are RLTL LV then the following are in RLTL LV :

1. b 3. ( ( b b ^' ' 1 ) ) W ( ( b ¬b '' ) 2 ) 5. r X' 2. ' 1 ^'2 4. ^1 _ ¬ ^2 6. 7 ! '
Compared to the simple subset as specified in [START_REF]IEEE, IEEE Std 1850-2005, IEEE Standard for Property Specification Language (PSL)[END_REF], the authors emphasize the major di↵erence for the operators _ and W (weak until): while the simple subset allows only one operand to be non-boolean, RLTL LT allows both nonboolean provided that they can be conjuncted with some Boolean and its negation. Indeed, in formula 3., we remark that both operands of the until operator are not required to be Boolean expressions. This very interesting feature will be used in section 5, to refine the PSL formulas while respecting an acceptable "simple subset".

Assertion-Based Verification for SystemC TLM Models

Overall principles

SystemC is in fact a library of C++ classes for modeling hardware systems, which covers various levels of accuracy [START_REF] Grötker | System Design with SystemC[END_REF]. Its mainstream abstraction level is TLM which provides communication models for complex "transactions" between IP blocks. Communications are implemented as function (method) calls, and a function usually receives as arguments the necessary information (address, data, flags,. . . ). Of course there is no synchronization clock at this system level.

At this transactional level, assertions of interest model temporal properties about the interactions in the SoC. Consequently Boolean expressions involved in PSL assertions are conditions over communication actions and their arguments.

To observe all relevant actions, the sampling "clock expression" has to be the disjunction of these transactional events.

Examples given hereinafter use the predicates defined in the ISIS tool [START_REF] Pierre | Dynamic Verification of SystemC Transactional Models (Chapter 22)[END_REF] i.e., conditions over communication actions can be expressed as follows:

• name.fct_CALL() denotes that the communication function fct of the component name has just been called,

• name.fct_END() expresses that the communication function fct of the component name just ended,

• name.fct.p# denotes the argument in position # of function fct (0 is used for the return value).

Use Case: Image Processing SoC

This use case that will be used to illustrate the refinements of section 5. It was designed by Astrium (EADS), this is an image processing platform that performs spectral compression on incoming images, see Figure 4. Raw data are first sub-sampled (left part, with the "Leon a" processor and the "DMA a" component). A 2D-FFT is applied to obtain the corresponding spectrum, and the latter is compressed and encoded to reduce the output throughput (right part of the figure, with the "Leon b" processor and the "DMA b"). The IO module generates periodic IRQs, received by Leon a, which configures DMA a to copy data from the IO module to Mem a. At the end of the transfer, Leon a sub-samples the data and writes the result to Mem a. It then configures DMA a to copy the results from Mem a to Mem b. Leon b configures the FFT module A set of requirements has been defined by the designers of this platform, and processed with the ISIS tool [START_REF] Pierre | Automatic Refinement of Requirements for Verification throughout the SoC Design Flow[END_REF]. Some of them are presented below.

DMA a Configuration. This first property is an essential assertion about the use of the DMA: (P I 1 ) DMA a must not be configured before the end of the transfer.

The formalization of this property is given below, with the component and function identifiers of this virtual platform. It states that, each time the Leon a processor finishes the DMA a configuration (i.e., writes a "start" in its control register), the DMA a end-of-transfer interrupt must be generated before the next configuration.

The PSL Modeling layer is used to store the address of the DMA a control register and the value associated with a "start" (both are constants). Note that the IRQ from the dma_a is not sent using a signal but a call to the method generate_irq. The sampling expression for this assertion is FFT Configuration. This second property is related to the behaviour of the FFT coprocessor: (P I 2 ) The FFT module must not be configured before the end of the computation.

Its formalization is close to the previous one. It states that, each time the Leon b processor finishes the FFT configuration (i.e., writes in its read address register), the end of the computation must occur (it corresponds to a reading from the Leon b, in the write length register of the FFT, of a value which is equal to the image size) before the next configuration.

The PSL Modeling layer is used here to store the addresses of the FFT control registers (constants), and to update the value fft_size that is transferred (written) from Leon b to the FFT (each time the Leon b calls its write_block function with the address read_length as first parameter), and the value that is read by Leon b (each time it calls its read_block function with the address write length as first parameter), called write_length_value. i.e., the assertion is evaluated everytime there is an occurrence of write_block or read_block operations of leon_b.

No Loss of Input Data. This third property is simple and used to check whether the reading rate prevents the loss of data.

(P I 3 ) An input data packet must be read before the IO module generates a new interrupt.

It is formalized below as follows: every time the IO module generates an IRQ, the DMA a must read the data in the IO module before the next IRQ. The IRQ from the IO module is sent by calling its method generate_irq. Simulations instrumented with such properties enable assessing the feasibility of various hardware configurations (bus frequency, average memory read and write cycle, processor frequency,. . . ), thus supporting architecture exploration.

Discussion about Data and Temporal Refinement

In the ESL-to-RTL refinement (synthesis) process, the virtual platform will be subject to the concretization of communication channels (introduction of actual channels in place of abstract components). It means that interface signals and timing details of the communication protocols are made explicit. Function calls (doPVtransport, write_block,. . . ) will be transformed into actual descriptions of data transfers conforming to a given protocol.

For the assertions, beyond simple issues such as the concretization of data and signal identifiers, the most salient concern is related to the modification of temporal granularity of the communication description. Indeed, a Boolean condition like leon_a.write_block_CALL() && leon_a.write_block.p2[0] == start becomes irrelevant in general, because the beginning of the write action and data transmission cannot be considered simultaneous anymore. It is necessary to map the high-level notion of transaction into clocked sequences of signals representing the implemented communication protocol.

Let us exemplify with some cases of single write transfers. In the single write of the Wishbone protocol [START_REF]SoC Interconnection: Wishbone[END_REF] (Figure 5 (a)), most control signals as well as address and data are set simultaneously. Similar conditions are found in the basic write operation of the IBM CoreConnect on-chip peripheral bus, OPB (Figure 5 (b), [START_REF]Designing Custom OPB Slave Peripherals for MicroBlaze[END_REF]). However a simple write operation of the AMBA Highperformance Bus (AHB) [START_REF] Arm | AMBA Specification[END_REF] (Figure 5 (c)) includes two phases: a one-cycle address phase in which control and address signals are sent, followed by a onecycle data phase for data transfer. And a single write operation in the PCI (Peripheral Component Interconnect) local bus specification [START_REF]PCI Local Bus Specification[END_REF] (Figure 5 (d)) performs consecutive address and data phases on the same bus, identified using various control signals. Therefore it is clear that a direct reuse of TLM assertions at the RT level is generally not possible, due to the fact that the successive actions that constitute a transfer, for a given communication protocol, is made explicit at that level.

Example. As a simple example, let us consider the condition leon_a.write_block_CALL() && leon_a.write_block.p2[0] == start in assertion (P I 1 ) of section 3.2, in the case where the abstract view of the communication channel is concretized into an AMBA AHB bus.

• The beginning of a simple write transfer by the Leon a processor (seen as leon a.write block CALL() at the abstract level) is expressed by the following conjunction of conditions on signals:

leon_a_HBUSREQ && leon_a_GRANTED && leon_a_HREADY && leon_a_HWRITE && leon_a_HTRANS == AMBA_NONSEQ && leon_a_HBURST == AMBA_SINGLE
which means that the processor has been granted access to the bus, and starts a simple write transfer.

• And the condition on the data leon a.write block.p2[0] == start now becomes leon a HWDATA == start.

However, the condition leon_a.write_block_CALL() && leon_a.write_block.p2[0] == start cannot be simply transformed into the conjunction of the two Boolean expressions detailed above. This is due to the fact that, in the original condition, function call and its parameter transmission are executed atomically (thus the value of the second parameter of leon a.write block can be accessed when this function is called) whereas after concretization, start of transfer and data transfer are not simultaneous.

More precisely, Figure 6 roughly depicts possible evaluations of property (P I 1 ), on a TLM virtual platform (with a fictional sampling), and after TLMto-RTL synthesis where the communication channel has been concretized into an AHB bus. After synthesis, the simulation trace is sampled using clock rising edges and the condition over the transferred data could only be checked one clock cycle after the beginning of the simple write transfer (cf. Figure 5 (c)). There are even more complex timing schemes than the simple write example of Figure 5 (c) in which control/address and data transmissions are realized on two consecutive clock cycles. For example, a slave may insert wait states into a read transfer (Figure 7) which means additional, potentially indefinite, time for completion. For a relevant adaptation of the temporal assertions, such timing details induced by the ESL to RTL synthesis flow must be taken into account. In section 5, we address two typical transformation contexts:

• Refinement of a communication into a sequence of events: a communication action considered as atomic at the transactional level (function call) is transformed into a sequence of actions in an implementation compliant with the targeted communication protocol (like in the previous write example where a communication request and its data transfer are made successively),

• Specific delay induced by an action: a certain number of clock cycles is required for a given communication action (e.g., estimated access time).

The refinement rules proposed respectively in sections 5.3 and 5.4 address those issues. If possible, any PSL assertion specified at the TLM level will be transformed into the corresponding one at the RT level by application of one or several of these rules on its sub-expressions. Note also that these transformations comply with the fact that, for dynamic verification, assertion statements must respect the constraints of the PSL simple subset (section 2.3).

Refinement Rules

Overview

Here we improve and extend the set of PSL transformation rules originally proposed in [START_REF] Pierre | Automatic Refinement of Requirements for Verification throughout the SoC Design Flow[END_REF]. Before formalizing these rules and their justification, let us give an intuitive explanation of these transformations, as pictured by Figure 8.

Rules (1) to [START_REF] Goering | Transaction models o↵er new deal for EDA[END_REF] are related to the refinement of a communication into a sequence of events. We focus on the before! and logical implication operators, which are commonly involved in TLM properties, and likely to be a↵ected by this type of refinement. Rule (1) addresses the transformation of the expression a before! (b ^c) in the case where, after synthesis, c occurs in fact X cycles after b (for example, b is the beginning of a write operation and c is a condition on the transferred data, or b is the beginning of a read operation and c is a condition on the read data). In the original TLM context, a must hold at least once strictly before b ^c holds. Whereas in the RTL context, a must hold at least once strictly before both b and c hold, separated by X cycles. Rule (2) is a generalization of rule (1) to any number of cycles between b and c.

Rule (3) addresses the transformation of expression (a ^b) before! c in the case where b occurs in fact X cycles after a. In the original TLM context, a ^b must hold at least once strictly before c holds. Whereas in the RTL context, both a and b, separated by X cycles, must hold at least once strictly before c holds. Rule (4) is a generalization of rule (3) to any number of cycles between a and b. And rule ( 5) is a generalization of rule (3) in the case where we know that b occurs after a and before a given event e.

Rule (6) addresses the transformation of expression (a ^b) ! c in the case where b occurs in fact X cycles after a. In the original TLM context, if a ^b Rules ( 8) to [START_REF]IEEE, IEEE Std 1850-2005, IEEE Standard for Property Specification Language (PSL)[END_REF] are related to the case where a precedence between events (e.g., until, before) is concretized into a specific delay for a communication action. Rules ( 8) and ( 9) address the transformation of expression a until! b in the case where the protocol description specifies that b is in fact expected 1 (resp. X) cycles after the beginning of the sub-trace on which this formula is evaluated. The transformation expresses the fact that, in the RTL context, this specific delay must be made explicit. Finally, rule [START_REF]IEEE, IEEE Std 1850-2005, IEEE Standard for Property Specification Language (PSL)[END_REF] addresses the transformation of expression a before! b under the same constraint.

We have recalled in section 2.1 that all temporal operators can be defined using a small amount of core operators. This set of rules should be extendable using most of those definitions.

It is worth noticing that both the formulas and the sampling expressions are di↵erent for TLM / RTL models. Indeed we have explained that, at the synchronous RT level, the sampling expression refers to clock rising edges, whereas at the transactional level, it usually corresponds to the disjunction of transactional events (in an unclocked context). Hence the interpretation of the transformations can be considered as follows: if ' is the TLM formula (with trace v), and ' 0 is the RTL formula (with trace v 0 ), then v 0 |= ' 0 guarantees that the original v |= ' is preserved.

Transformation Automation

Each rule presented hereinafter is of the form L R, it transforms a TLM temporal expression L into the corresponding RTL or hybrid expression R, taking into account given time constraints (that drive the selection of the appropriate transformation rule). As seen in section 4, an example constraint expresses that, for an AHB simple write operation, there is a one-cycle delay between sending the control and address and sending data.

A prototype tool has been implemented to automate the application of these rules to a TLM assertion [START_REF] Bel Hadj Amor | A Tool for the Automatic TLMto-RTL Conversion of Embedded Systems Requirements for a Seamless Verification Flow[END_REF]. Its architecture is sketched by Figure 9. It takes as input a transactional PSL assertion and a characterization of the targeted implementation of transfer functions (chronograms, described under a specific format in an Excel file). First the timing constraints for the assertion under consideration are extracted from those chronograms, under the form of an XML file. Then, unification is performed to find the subset of rules for which the left hand side L can match a sub-expression of the TLM assertion (if any). The outcome of this unification procedure is a set of candidate rules together with their identifier substitutions. Note that, by definition of the refinement rules, this system of rewrite rules is convergent. The substitutions are automatically applied to the right side R of each transformation rule.

Finally, by a bottom-up traversal of the syntactic tree of the TLM property, the instanciated rules are applied, thus resulting in the refined RTL assertion (if no applicable transformation rule has been found, only a purely "structural" transformation is performed i.e., signal-level expressions coming from the bus concretization are substituted to the original high-level Boolean expressions with function calls). The transformation of the expression a before! (b ^c) is considered here, in the case where c occurs X clock cycles after b in the actual implementation of the communication protocol (X is known).

Refinement of a Communication into a Sequence of Events

As an example, (b ^c) was a communication action seen as atomic at the transactional level (typically b denotes the call to a given communication function, and c is a condition on one of its parameters), which becomes a sequence of events (typically b corresponds to the communication request, and c to the data transfer). [⇤]}}} Such a transformation (that brings the assertion to the simple subset) is su cient for a pure RTL verification. To perform verifications on hybrid descriptions (i.e., platforms in which only some components have been synthesized into RTL descriptions, and some other components are still TLM modules), the assertion must preferably involve temporal operators. Thus we transform the SERE formula above as follows: This formula has the form B until! ', where B is a boolean expression and ' is a temporal formula. Such a formula does not belong to the PSL simple subset as specified in [START_REF]IEEE, IEEE Std 1850-2005, IEEE Standard for Property Specification Language (PSL)[END_REF], because the right-hand side operand of until! is not Boolean, but it satisfies the form of formula 3. of the subset defined in [START_REF] Ben-David | The safety simple subset[END_REF] (see section 2.3). Indeed, this formula is of the form (¬a ^b1 ) until! (a ^'1 ), where b 1 is a boolean and ' 1 is a temporal expression. The right operand is a conjunction with a boolean (a) while the left operand is a conjunction with the negation of this boolean (¬a).

v |= {(¬b ^¬c ^¬a)[⇤]; ¬b ^¬c ^a; {{(¬c ^¬b)[⇤]} | {(¬c ^¬b)[⇤]; b; [⇤]}}} is 9k < |v| s.t.
(3) Transformation of (a ^b) before! c in the case where b occurs X cycles after a

We target now the transformation of (a ^b) before! c in the case where b occurs X clock cycles after a in the actual implementation of the communication protocol (X is known). Like for transformation (2), the formula is of the form (¬a^b 1 ) until! (a^' 1 ), where b 1 is a boolean and ' 1 is a temporal expression. The right operand is a conjunction with a boolean (a) while the left operand is a conjunction with the negation of this boolean (¬a). It does not belong to the PSL simple subset as specified in [START_REF]IEEE, IEEE Std 1850-2005, IEEE Standard for Property Specification Language (PSL)[END_REF] but it satisfies the form of formula 3. of the subset of [START_REF] Ben-David | The safety simple subset[END_REF].

(5) Transformation of (a ^b) before! c in the case where b occurs before a given event e

The transformation of the same expression (a ^b) before! c is considered again, but in the more general case where b occurs any number of clock cycles after a, but before a given event e (usually an event that determines the end of a communication). Proof. We are under the constraint b occurs after a and before e, and all of them must occur prior to c, which is expressed by the following SERE: Here too, each until! sub-formula is of the form (¬B ^b1 ) until! (B ^'1 ), where b 1 is a boolean and ' 1 is a temporal expression. The right operand is a conjunction with a boolean (B) while the left operand is a conjunction with the negation of this boolean (¬B). Once again, the formula belongs to the "simple subset" as defined in [START_REF] Ben-David | The safety simple subset[END_REF].

v |= {(¬c ^¬a)[⇤]; ¬c ^¬b ^¬e ^a; (¬c ^¬e ^¬b)[⇤]; ¬c ^b ^¬e; (¬c ^¬e)[⇤]; ¬c ê; [⇤]} i.e., 9k, k < |v| s.t., 9j, k + 1  j < |v| s.t., 9m, j + 1  m < |v| s.t. v 0..k |= (¬c ^¬a)[⇤]
(6) Transformation of (a ^b) ! c in the case where b occurs X cycles after a

We consider now the transformation of (a^b) ! c in the case where b occurs X clock cycles after a in the implementation of the communication protocol.

(a ^b) ! c a ! (next a![0..(X 1)](¬b) _ next![X](¬b _ c))
Proof. Since we are under the constraint b occurs X cycles after a, and c must hold if (and when) both of them have occurred, the following SERE-based formula should be verified in this context where a and b are Boolean expressions:

v |= a ! ({¬b[⇤X] ; b} 7 ! c) i.e., v 0 |= a ! (v 0.. |= {¬b[⇤X] ; b} 7 ! c) i.e., v 0 |= a ! (v 0..X |= {¬b[⇤X] ; b} ! v X |= c) i.e., v 0 |= a ! ((v 0..X 1 |= {¬b[⇤X]} and v X |= b) ! v X |= c) i.e., v 0 |= a ! ((v 0 |= ¬b and . . . and v X 1 |= ¬b and v X |= b) ! v X |= c)
i.e., using the definition of next!,

v 0 |= a ! ((v 0.. |= ¬b and . . . and v 0.. |= next![X 1](¬b) and v 0.. |= next![X]b) ! v 0.. |= next![X]c) and we recall that the definition of next a![i..j](') is next![i](')^. . .^next![j]('), thus we get: v 0 |= a ! ((v 0.. |= next a![0..(X 1)](¬b) and v 0.. |= next![X]b) ! v 0.. |= next![X]c) i.e., v |= a ! ((next a![0..(X 1)](¬b) ^next![X]b) ! next![X]c) i.e., v |= a ! (next a![0..(X 1)](¬b) _ next![X](¬b _ c))
Though this formula does not formally belong to the simple subset as defined in [START_REF]IEEE, IEEE Std 1850-2005, IEEE Standard for Property Specification Language (PSL)[END_REF], because both operands of the _ operator are temporal expressions, its evaluation clearly conforms to the monotonic advancement of time. Proof. Since we are under the constraint b occurs any number of cycles after a, and c must hold if (and when) both of them have occurred, the following SEREbased formula should be verified in this context where a and b are Boolean expressions:

v |= a ! ({¬b[⇤] ; b} 7 ! c) i.e., v 0 |= a ! (v 0.. |= {¬b[⇤] ; b} 7 ! c) i.e., v 0 |= a ! (8j, j < |v|, s.t. v 0..j 1 |= {¬b[⇤]} and v j |= b, v j |= c) i.e., v 0 |= a ! ((9 j 0 < |v| s.t. v 0..j0 1 |= {¬b[⇤]} and v j0 |= (b ^c)) or (8j, j < |v|, v 0.. |= {¬b[⇤]})) i.e., v 0 |= a ! ((9 j 0 < |v| v j0 |= (b ^c) and 8k, k < j 0 , v k |= ¬b) or (8j, j < |v|, v 0.. |= {¬b[⇤]}))
i.e., v |= next e![0..X-1](a ^¬b) ^next a![0..X-1](¬b) ^next![X](b) i.e., v |= next e![0..X-1](a) ^next a![0..X-1](¬b) ^next![X](b)

Summary

The database of rules that is used by the tool described in section 5.2 is summarized in Table 1.

TLM expression RTL expression Constraint C

Refinement of a communication into a sequence of events (1) a before! (b ^c)

((b ! next[X](¬c)) until! a) ^next event!(a)(b ! next[X](¬c))) c occurs X cycles after b (

Illustration on the Use Case

We illustrate the TLM-to-RTL assertion refinement on the use case of section 3.2, with a concretization of the abstract bus component into an AHB bus.

Simple Case: No Loss of Input Data

Let us first consider the simple case of property (P I 3 ). The conjunction of conditions dma a.read block CALL() and dma a.read block.p1 == io module add expresses that a read transfer occurs, together with a condition on the read address. Since control and address transmission are simultaneous, the assertion keeps its original temporal pattern. It is structurally transformed into: Note that conditions of the form io module.generate irq CALL() remain in this assertion, instead of conditions on an IRQ signal. This is due to the fact that the virtual platform has only undergone a partial RTL refinement step. We deal with an hybrid description: a RTL description of AHB bus has been substituted to the TLM channel and the connected components have been modified to respect this protocol, but they have kept a part of their original behaviour. The TLM function generate irq() is still present in the DMA and IO components. The sampling expression for this new assertion uses both generate irq() calls and rising edges of the bus clock.

DMA a Configuration

Let us now consider the refinement of assertion (P I 1 ) which involves conditions on the transferred data, second argument of function write_block (leon_a.write_block.p2).

Those conditions occur both in the left hand side of the implication and in the right hand side of the before! operator. Therefore both transformation rules ( 6) and (1) of section 5.3 are applied, where X equals 1. We obtain an assertion of the form below (for the sake of conciseness, some signals have been omitted):

FFT Configuration

For property (P I 2 ), a condition on the transferred data appears in the left hand side of the before! operator. This before! expression is of the form (a ^b) before! c where a is leon b.read block END() && leon b.read block.p1 == write length i.e., a reading from the Leon b in the write length register of the FFT, and b is write length value == fft size i.e., the interpretation of the value that is read (leon b.read block.p2) equals the image size.

Under the hypothesis that b occurs 1 clock cycle after a i.e., the slave reacts in one clock cycle, the transformation of (a ^b) before! c uses rule (3) of section 5.3, where X equals 1. We obtain an assertion of the following form (triggered upon rising edges of the bus clock): Under the hypothesis that the completion of the reading operation may take an unknown number of clock cycles, the transformation of (a ^b) before! c uses rule (4) of section 5.

Some Observations

The advantage of performing such transformations automatically is twofold. First, automation using verified rules prevents manual errors. Second, the RTL assertions may be much more complex than the original TLM ones, and it would be hard work to write them by hand. To illustrate this claim, Table 2 summarizes the complexities of the assertions for the TLM and resulting RTL versions (actual assertions, where no signal has been omitted). This complexity is evaluated in terms of the number of PSL operators and in terms of the total size of the Boolean expressions (number of atomic expressions). As a counterpart, the characterization of the protocol concretization must be made in an easily readable form (inside an Excel file in our case). It is necessary to specify the names of the signals involved in each communication (e.g., HBUSREQ, HWDATA,. . . for leon a.write block()). Using this information, our tool generates an Excel sheet that must be filled, as in Figure 10. Note however that, once created, this file is reusable for every assertion transformation. On the other hand, to compare simulation results before and after SoC concretization, Table 3 summarizes some experiments, realized on an Intel Core2 Duo under Debian Linux, for this case study. We consider a pure TLM simulation for 1000 images and a mixed RTL/TLM simulation for 100 images. Due to the presence of the RTL bus, simulation is much slower in that case, this is why we ran it for 100 images only. For each property, we report the CPU time monitoring overhead and the "number of property activations", which is related to the sampling expressions. For TLM monitors, it corresponds to the number of communication actions that triggered the property evaluation during simulation. For hybrid monitors, it corresponds to the number of clock rising edges for the second property, and to the number of clock rising edges + IRQ generations for the other ones.

The monitors report comparable information in both simulations. We can remark that the CPU time overhead decreases in the hybrid context even though the number of activations increases. This is due to the fact that the complexity of the virtual platform increases more significantly than the complexity of the refined monitors.

Some Related Work

Refinement of Temporal Properties in the TLM-to-RTL Design Flow

Few results have been presented so far for the formal refinement of temporal assertions from TLM to RTL. Some requirements for the transformation of temporal assertions are presented in [START_REF] Ecker | Requirements and Concepts for Transaction Level Assertion Refinement[END_REF]. The follow-up work of [START_REF] Steininger | Automated Assertion Transformation Across Multiple Abstraction Levels[END_REF] broadens this interesting discussion about the major concerns for the refinement of temporal assertions, expressed in an in-house specification language called UAL (Universal Assertion Language). However, the principles and the implemented framework impose the preservation of the syntactic structure of the assertions. Temporal patterns are unchanged through transformations: the assertion structure, including the exact number of subcomponents (properties, sequences,. . . ) and the way they are connected, is not changed. Only replacing an element by another element of the same type is allowed (for example, changing a required time from 10 ns to 2 clock cycles). Therefore this approach is more restrictive than the transformations presented here, which significantly modify the syntactic form of the temporal properties to adhere to the RTL behaviour.

The automation of a TLM-to-RTL property refinement is addressed in [START_REF] Herdt | Towards Fully Automated TLMto-RTL Property Refinement[END_REF] that works under the assumption that transactors are available. The authors propose to extract a characterization of the RTL protocol as a Finite State Machine, from the transactor. The main contribution is the description of the procedure that enables to obtain this specification as a FSM from a symbolic execution of the transactor. Then the idea is also to preserve the temporal structure of the TLM property (it keeps its temporal operators: always, before, next event,...) and to use the FSM specification of the protocol to replace TLM events by the corresponding sequence of RTL signals (SERE). This is illustrated with the refinement of two realistic properties, the first one uses the before operator and the second one contains next event operators. The key idea is interesting but, due to the fact that it systematically replaces Boolean expressions by sequences, this solution has some shortcomings: in particular it does not respect the definition of the next event operator (the first operand must be a Boolean expression), and it can produce PSL formulas that do not belong to the "simple subset". Nevertheless, using symbolic execution to get a formalization of the protocol could be an attractive alternative to our manual creation of Excel files, when transactors are available.

Complementary Solutions in the TLM-to-RTL Design Flow

Instead of transforming assertions, a transactor-based solution (as explained in section 1.1) is proposed in [START_REF] Bombieri | On the Evaluation of Transactorbased Verification for Reusing TLM Assertions and Testbenches at RTL[END_REF] in order to reuse TLM testbenches and assertions for TLM-RTL co-simulations.

Assertion transformations are considered in [START_REF] Bombieri | Hybrid, Incremental Assertion-Based Verification for TLM Design Flows[END_REF], but these assertions are pure Boolean expressions that express computational invariants which relate primary outputs to primary inputs for a given platform component. Complementarily, the work presented in [START_REF] Bombieri | Reusing RTL Assertion Checkers for Verification of SystemC TLM Models[END_REF] addresses the opposite context in which RTL IPs are abstracted into TLM models, and proposes to abstract the assertions accordingly.

As a complementary solution, RTL test generation from TLM specifications is investigated in [START_REF] Chen | Towards RTL Test Generation from Sys-temC TLM Specifications[END_REF]. First, coverage-driven directed TLM test generation is performed from the TLM SoC model, preliminarily transformed into a CPN (Colored Petri Net) representation. The goal is to cover all the functionalities of the TLM design, and TLM tests are produced by model checking properties that express CPN transition coverage. Then transformation rules (informally described) are used to translate the TLM tests into RTL tests. They mainly rewrite identifiers using RTL-to-TLM name mapping information (correspondence between TLM identifiers and RTL signals) and insert delays based on the protocol timing information.

The focus of [START_REF] Chen | Assertion-Based Functional Consistency Checking between TLM and RTL Models[END_REF] is on the issue of preserving functional consistency between di↵erent abstraction layers, in the context of assertion-based verification. The assertions under consideration are of the form eventually! p, they target the verification of the transaction flow: the goal is either to examine the data contents or to check the data flow by inspecting all branch conditions. TLM tests are applied both to the TLM model and to the RTL implementation (using a transactor). Thus TLM assertions and their RTL counterparts can be checked by assertion checkers, and consistency checking is performed by comparing simulation traces recorded by these TLM and RTL assertion checkers. The refinement of the TLM assertions follows a method that is close to the one of [START_REF] Chen | Towards RTL Test Generation from Sys-temC TLM Specifications[END_REF]: it also utilizes name mapping between TLM variables and RTL signals and timing information (mainly the clock expression).

Comparison with the Correct-by-Construction Approach

As was illustrated by Figure 1, the context addressed here is the typical SoC design flow, in which a golden model of the hardware system (as a virtual platform) is concretized into a RTL description of the actual implementation. To support the verification process along this flow, temporal assertions that formalize expected system properties are refined into concretized ones.

In contrast, an alternative notion of refinement is found in the correct-byconstruction approach advocated by methods such as Event-B [START_REF] Abrial | Modeling in Event-B -System and Software Engineering[END_REF]. The principle of this method (which is an extension of the original B method for software design [START_REF] Abrial | The B-book -Assigning programs to meanings[END_REF]) consists in manually refining an abstract model of the system itself i.e., the original specification, using a series of refined intermediate models.

Each event of the model describes a specific change in the system (state variable updating), and is refined along the system refinement process (i.e., details are gradually added to make each event more concrete / precise). Boolean invariants express system requirements. Proof obligations are automatically produced during refinement, their proof guarantees that each event preserves the invariant of the model. If the first, most abstract, system model satisfies the invariants, and if the proof obligations can be discharged, then the most concrete model satisfies the invariants too. Hence the implementation of the correct-by-construction paradigm. Applications of this method can be found for example in [START_REF] Méry | Modeling an Aircraft Landing System in Event-B[END_REF], [START_REF] Singh | Stepwise formal modeling and verification of Self-Adaptive systems with Event-B. The automatic rover protection case study[END_REF]. As shown on Figure 11, this approach could rather be seen as an alternative to the first phases of the classical design flow, to build a correct-by-construction view of the SoC platform, from an abstract system specification. Correctness by construction means that Boolean invariants are preserved. In contrast, the solution proposed here addresses the refinement and verification of temporal properties from a SoC platform model to its RTL implementation.

Conclusion

We have proposed a set of transformation rules for the automatic refinement of PSL assertions from the system level (TLM) to the signal level (RTL). The refined assertions preserve a PSL "simple subset", thus enabling dynamic verification. They also avoid the use of SEREs, which is useful if the refined assertions have to be used both for pure RTL designs and for hybrid TLM/RTL descriptions. Indeed, SEREs are relevant for RTL designs that have a synchronization clock but, for transactional descriptions, assertions rather express causality and/or precedence between actions, using temporal operators such as until!, before!, next event!.

We have considered two widespread categories of temporal refinements: a transfer considered as atomic at the transactional level (method call) is transformed into a given sequence of actions (on successive clock ticks), and a specific delay is induced by an action.

This set of rules should definitely be extended to support more sophisticated communication schemes, in particular burst transfers. For example, an additional assertion for the use case of section 3.2 states that "each incoming data packet (read from the IO module) must have a corresponding output packet (written by DMA b to the IO module) before 3 new incoming data packets are processed" [START_REF] Pierre | Automatic Refinement of Requirements for Verification throughout the SoC Design Flow[END_REF]. Data considered in this assertion are more than a few bytes long, they are large data (images, or parts of images) that necessitate burst transfers. Processing such a statement will require rules that, in addition to the temporal refinements considered in section 5, also take into account the occurrence of multiple transfers. Additional manipulations will probably be necessary to "reconstruct" the values of the transmitted data. We can assume that, to that goal, it will be necessary to use the PSL Modeling layer in addition to the Temporal layer, in the refined formulas.

Highlights:

-The verification process of today's systems on chip is a complex task -Assertion-Based Verification helps debugging -Verification should be consistent across abstraction levels

Figure 1 :

 1 Figure 1: Soc design flow with assertion-based verification

Figure 3 :

 3 Figure 3: UVM TestBench block diagram[START_REF]UVM Verification Guide -UVM TestBench[END_REF]

  assert ALWAYS ({not Data and En ; (Data and En)[*7]} |-> AbortFound BEFORE! StartOfFrame);

Figure 4 :

 4 Figure 4: Image processing SoC

Figure 5 :

 5 Figure 5: Examples of single transfers

Figure 6 :

 6 Figure 6: Possible evaluations of property (P I 1 )

Figure 7 :

 7 Figure 7: AHB read transfer with wait states[START_REF]AMBA 3 AHB-Lite Protocol[END_REF]

Figure 8 :

 8 Figure 8: Intuitive interpretation of the transformation rules

Figure 9 :

 9 Figure 9: Architecture of the prototype refinement tool

( 1 )

 1 Transformation of a before! (b ^c) in the case where c occurs X cycles after b

a( 2 )

 2 before! (b ^c) ((b ! next[X](¬c)) until! a) ^next event!(a)(b ! next[X](¬c)))Proof. Strong before! means that a must occur on the trace. Since we are under the constraint c occurs X cycles after b, a must hold before the clock tick in which b ^next[X]c holds (if any), which means that the expression amounts to:v |= a before! (b ^next[X]c).This formula is outside the simple subset because one of the operands of the before! operator is a temporal expression. Consequently, we transform v |= a before! (b ^next[X]c) as follows: from the definition of before!,v |= ¬(b ^next[X]c) until! (a ^¬(b ^next[X]c)) i.e., 9k < |v| s.t. v k.. |= (a ^¬(b ^next[X]c)) and 8j < k, v j.. |= ¬(b ^next[X]c) i.e., 9k < |v| s.t. v k.. |= (a ^¬(b ^next[X]c)) and v k.. |= a and 8j < k, v j.. |= (¬a) _ (b ^next[X]c) and 8j < k, v j.. |= ¬(b next[X]c) i.e.,9k < |v| s.t. v k.. |= (a ^¬(b ^next[X]c)) and v k.. |= a and 8j < k, v j.. |= ¬a and 8j < k, v j.. |= ¬(b ^next[X]c) i.e., 9k < |v| s.t. v k.. |= a and 8j < k, v j.. |= ¬(b ^next[X]c) and v k.. |= (a ^¬(b ^next[X]c)) and 8j < k, v j.. |= ¬a i.e., from the definition of until!, v |= (¬(b ^next[X]c) until! a) ^(¬a until! (a ^¬(b ^next[X]c))) i.e., from the definition next event!(b)(') = ¬b until! (b ^'), v |= (¬(b ^next[X]c) until! a) ^next event!(a)(¬(b ^next[X]c)) i.e., v |= ((b ! next[X](¬c)) until! a) ^next event!(a)(b ! next[X](¬c))) that avoids having a temporal operator under a negation. Transformation of a before! (b ^c) in the case where c occurs any number of cycles after b The transformation of the same expression a before! (b ^c) is considered here, but in the more general case where c occurs any number of clock cycles after b in the actual implementation of the communication protocol. a before! (b ^c) (¬b ^¬c ^¬a) until! (¬b ^¬c ^a ^next!((¬c ^¬b) until b)) Proof. Since we are under the constraint c occurs any number of cycles after b, a must hold before the clock tick in which b holds without any occurrence of c prior to that instant, which is expressed by the following SERE: v |= {(¬b ^¬c ^¬a)[⇤]; ¬b ^¬c ^a; {{(¬c ^¬b)[⇤]} | {(¬c ^¬b)[⇤]; b;

  v 0..k |= {(¬b ^¬c ^¬a)[⇤]} and v k+1 |= (¬b ^¬c ^a) and v k+2.. |= {{(¬c ¬b)[⇤]} | {(¬c ^¬b)[⇤]; b; [⇤]}} i.e., 9k < |v| s.t. v 0..k |= {(¬b^¬c^¬a)[⇤]} and v k+1 |= (¬b^¬c^a) and (v k+2.. |= {(¬c^¬b)[⇤]} or v k+2.. |= {(¬c ^¬b)[⇤]; b; [⇤]}) i.e., 9k < |v| s.t. v 0..k |= {(¬b^¬c^¬a)[⇤]} and v k+1 |= (¬b^¬c^a) and (v k+2.. |= {(¬c^¬b)[⇤]} or (9j, k + 1  j < |v|, s.t. v k+2..j |= {(¬c ^¬b)[⇤]} and v j+1 |= b) i.e., 9k < |v| s.t. v 0..k |= {(¬b^¬c^¬a)[⇤]} and v k+1 |= (¬b^¬c^a) and (v k+2.. |= {(¬c^¬b)[⇤]} or (9j, k+1  j < |v|, s.t. (8m, k+2  m < j+1, v m |= (¬c^¬b)) and v j+1 |= b) i.e., from the definition of until!, 9k < |v| s.t. v 0..k |= {(¬b ^¬c ^¬a)[⇤]} and v k+1 |= (¬b ^¬c ^a) and (v k+2.. |= {(¬c ¬b)[⇤]} or (v k+2.. |= (¬c ^¬b) until! b)) i.e., 9k < |v| s.t. v 0..k |= {(¬b ^¬c ^¬a)[⇤]} and v k+1 |= (¬b ^¬c ^a) and (v k+2.. |= always(¬c ¬b) or (v k+2.. |= (¬c ^¬b) until! b)) i.e., 9k < |v| s.t. v 0..k |= {(¬b ^¬c ^¬a)[⇤]} and v k+1 |= (¬b ^¬c ^a) and (v k+2.. |= always(¬c ¬b) _ ((¬c ^¬b) until! b)) i.e., from the definition of weak until, 9k < |v| s.t. v 0..k |= {(¬b ^¬c ^¬a)[⇤]} and v k+1 |= (¬b ^¬c ^a) and v k+2.. |= ((¬c ¬b) until b) i.e., from the definition of next!, 9k < |v| s.t. v 0..k |= {(¬b ^¬c ^¬a)[⇤]} and v k+1 |= (¬b ^¬c ^a) and v k+1.. |= next!((¬c ¬b) until b) i.e., 9k < |v| s.t. v 0..k |= {(¬b ^¬c ^¬a)[⇤]} and v k+1.. |= (¬b ^¬c ^a) ^next!((¬c ^¬b) until b) i.e., 9k < |v| s.t. (8j < k + 1, v j |= (¬b ^¬c ^¬a)) and v k+1.. |= (¬b ^¬c ^a) ^next!((¬c ¬b) until b) i.e., from the definition of until!, v 0.. |= (¬b ^¬c ^¬a) until! ((¬b ^¬c ^a) ^next!((¬c ^¬b) until b)) thus we get v |= (¬a ^¬b ^¬c) until! (a ^¬b ^¬c ^next!((¬c ^¬b) until b))

( 4 )

 4 before! cProof. Since we are under the constraint b occurs X cycles after a, and both of them must hold before the occurrence of c (if any), the following SEREbased formula should be verified in this context where a, b and c are Boolean expressions:v |= {(¬c ^¬a)[⇤] ; ¬c ^a ; (¬c ^¬b)[⇤(X-1)] ; ¬c ^b ; [⇤]} i.e., 9k < |v|-X s.t. v k |= (¬c ^a) and v k+X |= (¬c ^b) and 8j  k + X, v j |= ¬c i.e., 9k < |v|-X s.t. v k |= a and v k+X |= b and 8j  k + X, v j |= ¬c i.e., 9k 0 < |v| s.t. v k 0 X |= a and v k 0 |= b and 8j  k 0 , v j |= ¬c i.e., 9k 0 < |v| s.t. v k 0 |= (prev(a, X) ^b ^¬c) and 8j < k 0 , v j |= ¬c i.e.,from the definition of until!, v |= ¬c until! (prev(a, X) ^b ^¬c) i.e., from the definition of before!, v |= (prev(a, X) ^b) before! c Transformation of (a ^b) before! c in the case where b occurs any number of cycles after a The transformation of the same expression (a ^b) before! c is considered here, but in the more general case where b occurs any number of clock cycles after a in the actual implementation of the communication protocol. until! (¬c ^a ^next!((¬c ^¬b) until (¬c ^b))) Proof. We are under the constraint b occurs any number of cycles after a, and both of them must occur prior to c, which is expressed by the following SERE: v |= {(¬c ^¬a)[⇤] ; ¬c ^a ; (¬c ^¬b)[⇤] ; ¬c ^b ; [⇤]} i.e., 9k < |v| s.t. v 0..k |= {(¬c^¬a)[⇤]} and v k+1 |= (¬c^a) and v k+2.. |= {(¬c^¬b)[⇤]; ¬c^b; [⇤]} i.e., 9k < |v| s.t. v 0..k |= {(¬c ^¬a)[⇤]} and v k+1 |= (¬c ^a) and 9j, k + 1  j < |v|, s.t. (v k+2..j |= {(¬c ^¬b)[⇤]} and v j+1 |= ¬c ^b) i.e., 9k < |v| s.t. (8m, m < k + 1, v m |= ¬c ^¬a) and v k+1 |= (¬c ^a) and 9j, k + 1  j < |v|, s.t. (v k+2..j |= {(¬c ^¬b)[⇤]} and v j+1 |= ¬c ^b) i.e., 9k < |v| s.t. (8m, m < k + 1, v m |= ¬c ^¬a) and v k+1 |= (¬c ^a) and 9j, k+1  j < |v|, s.t. ((8m, k+2 < m < j+1, v m |= ¬c^¬b) and v j+1 |= ¬c^b) i.e., from the definition of until!, 9k < |v| s.t. (8m, m < k + 1, v m |= ¬c ^¬a) and v k+1 |= (¬c ^a) and v k+2.. |= (¬c ^¬b) until! (¬c ^b) i.e., from the definition of next!, 9k < |v| s.t. (8m, m < k + 1, v m |= ¬c ^¬a) and v k+1.. |= (¬c ^a) ^next!((¬c ^¬b) until! (¬c ^b)) i.e., from the definition of until!, v |= (¬c ^¬a) until! ((¬c ^a) ^next!((¬c ^¬b) until! (¬c ^b)))

c

  ^¬ e ^ab ) ¬ ^¬ ^¬ until! (¬c^b^¬e ^next!((¬c^¬e) until! (¬c^e)))))

  i.e., from the definition of until!, v |= (¬c ^¬a) until! (¬c ^¬b ^¬e ^a ^next!((¬c ^¬e ^¬b) until! ((¬c ^b ¬e) ^next!((¬c ^¬e) until! (¬c ^e)))))

( 7 )

 7 Transformation of (a^b) ! c in the case where b occurs any number of cycles after a For the transformation of the same expression (a ^b) ! c, we now consider the case where b occurs any number of clock cycles after a in the implementation of the communication protocol. (a ^b) ! c a ! next event(b)(c)

( 9 )( 10 )

 910 i.e., v 0 |= a ! ((¬b until! (b ^c)) or (always ¬b)) i.e., v 0 |= a ! (¬b until (b ^c)) i.e., from the definition of next event, v 0 |= a ! next event(b)(c) 5.4. Specific Delay induced by an Action (8) Transformation of a until! b -Constraint: next! b We start with a simple refinement. The expression a until! b can be strengthened as follows under the constraint that b is expected 1 clock tick after the beginning of the trace on which a until! b is evaluated. As an example, b can be the answer awaited from a slave component to a request a from a master component. a until! b a ^next! b Proof. We recall the semantics of the until! operator: v |= ' until! , 9k < |v| s.t. v k.. |= and 8j < k, v j.. |= ' Since we are under the constraint next! b, we have to consider the conjunction of the formulae: v |= a until! b and v |= next! b, i.e., v |= a until! b and v 1.. |= b i.e., (9k < |v| s.t. v k.. |= b and 8j < k, v j.. |= a) and v 1.. |= b i.e., v 1.. |= b and v 0.. |= a i.e., v |= a ^next! b Transformation of a until! b -Constraint: next![X]b We consider here the refinement of the expression a until! b under the constraint that b is expected X clock ticks after the beginning of the trace on which a until! b is evaluated, X > 1. a until! b next a![0..X-1](a) ^next![X](b) Proof. Since we are under the constraint next![X]b, we have to consider the conjunction of the formulae: v |= a until! b and v |= next![X]b, i.e., v |= a until! b and v X.. |= b i.e., (9k < |v| s.t. v k.. |= b and 8j < k, v j.. |= a) and v X.. |= b i.e., v 0.. |= a and v 1.. |= a and . . . v X 1.. |= a and v X.. |= b i.e., v |= next a![0..X-1](a) ^next![X](b) Transformation of a before! b -Constraint: next![X]b We consider now the refinement of the expression a before! b under the constraint that b is expected X clock ticks after the beginning of the trace on which a before! b is evaluated, X > 1. a before! b next e![0..X-1](a) ^next a![0..X-1](¬b) ^next![X](b) Proof. Since we are under the constraint next![X]b, we have to consider the conjunction of the formulae: v |= a before! b and v |= next![X]b, i.e., v |= (¬b until! a ^¬b) and v X.. |= b i.e., 9k < |v| s.t. v k.. |= (a ^¬b) and 8j < k, v j.. |= ¬b and v X.. |= b thus k < X, and we have 9k < X s.t. v k.. |= (a ^¬b) and 8j < k < X, v j.. |= ¬b and v X.. |= b

2 )( 7 )

 27 a before! (b ^c) (¬b ^¬c ^¬a) until! (¬b ^¬c ^a ^next!((¬c ^¬b) until b)) c occurs any number of cycles after b (3) (a ^b) before! c (prev(a, X) ^b) before! c b occurs X cycles after a (4) (a ^b) before! c (¬c ^¬a) until! (¬c ^a ^next!((¬c ^¬b) until (¬c ^b))) b occurs any number of cycles after a (5) (a ^b) before! c (¬c ^¬a) until! (¬c ^¬b ^¬e ^a next!((¬c ^¬e ^¬b) until! (¬c ^b ^¬e ^b occurs before a given event e next!((¬c ^¬e) until!(¬c ^e))))) (6) (a ^b) ! c a ! (next a![0..(X 1)](¬b) _ next![X](¬b _ c)) b occurs X cycles after a (a ^b) ! c a ! next event(b)(c)b occurs any number of cycles after a Specific delay for a communication(8) a until! b a ^next! b next! b (9) a until! b next a![0..X-1](a) ^next![X](b) next![X]b(10) a before! b next e![0..X-1](a) ^next![X]b next a![0..X-1](¬b) ^next![X](b)

  assert ALWAYS ((leon_a.HREADY && leon_a.HWRITE && leon_a.HADDR == ctrl_reg) => ( (leon_a.HWDATA != start) || NEXT(leon_a.HWDATA != start || NEXT((((bus_a.HREADY && leon_a.HWRITE && leon_a.HADDR == ctrl_reg) => NEXT(leon_a.HWDATA != start)) UNTIL! dma_a.generate_irq_CALL()) && NEXT_EVENT!(dma_a.generate_irq_CALL()) ((bus_a.HREADY && leon_a.HWRITE && leon_a.HADDR == ctrl_reg) => NEXT(leon_a.HWDATA != start)))))

Figure 10 :

 10 Figure 10: Example characterization of the write block communication

Figure 11 :

 11 Figure 11: Alternative notions of refinement

  Glossary ABV = Assertion-Based Verification, runtime (simulation, emulation) verification of temporal assertions. DUT = design under test. ESL = Electronic System Level, design level focused on higher abstraction concerns. IP block = Intellectual Property core, reusable component which is the property of one party. PSL = Property Specification Language, IEEE standard 1850. RTL = Register Transfer Level, design level which models synchronous digital circuits in terms of the updatings of hardware registers and signals. SoC = System on Chip. TLM = Transaction-Level Modeling, design level which focuses on the highlevel functional description of modules and communications among modules.

  r 1 and v 2 |= r 2 Note that we will interpret it hereinafter as follows:v |= r 1 ; r 2 , 9k < |v| s.t. v 0..k |= r 1 and v k+1..|v| |= r 2

  and v k+1 |= ¬c ^¬b ^¬e ^a and v k+2..j |= (¬c ^¬e ^¬b)[⇤] and v j+1 |= ¬c ^b ^¬e and v j+2..m |= (¬c ^¬e)[⇤] and v m+1 |= ¬c ^e i.e., 9k, k < |v| s.t., 9j, k + 1  j < |v| s.t., 9m, j + 1  m < |v| s.t. (8n, n < k, v n |= (¬c ^¬a)) and v k+1 |= ¬c ^¬b ^¬e ^a and (8n, k + 2  n < j + 1, v n |= (¬c ^¬e ^¬b)) and v j+1 |= ¬c ^b ^¬e and (8n, j + 2  n < m + 1, v n |= (¬c ^¬e)) and v m+1 |= ¬c ^e i.e., from the definition of until!, 9k, k < |v| s.t., 9j, k + 1  j < |v| s.t. (8n, n < k, v n |= (¬c ^¬a)) and v k+1 |= ¬c ^¬b ^¬e ^a and (8n, k + 2  n < j + 1, v n |= (¬c ^¬e ^¬b)) and v j+1 |= ¬c ^b ^¬e and v j+2.. |= (¬c ^¬e) until! (¬c ^e) i.e., from the definition of next!, 9k, k < |v| s.t., 9j, k + 1  j < |v| s.t. (8n, n < k, v n |= (¬c ^¬a)) and v k+1 |= ¬c ^¬b ^¬e ^a and (8n, k + 2  n < j + 1, v n |= (¬c ^¬e ^¬b)) and v j+1.. |= (¬c ^b ^¬e) ^next!((¬c ^¬e) until! (¬c ^e)) i.e., from the definition of until!, 9k, k < |v| s.t.

(8n, n < k, v n |= (¬c ^¬a)) and v k+1 |= ¬c ^¬b ^¬e ^a and v k+2.. |= (¬c ^¬e ^¬b) until! ((¬c ^b ^¬e) ^next!((¬c ^¬e) until! (¬c ^e))) i.e., from the definition of next!, 9k, k < |v| s.t. (8n, n < k, v n |= (¬c ^¬a)) and v k+1.. |= ¬c ^¬b ^¬e ^a ^next!((¬c ^¬e ^¬b) until! ((¬c ^b ^¬e) ^next!((¬c ¬e) until! (¬c ^e))))

Table 1 :

 1 Summary of the Transformation Rules

  3, and we get:

	assert
	ALWAYS ((leon_b.HREADY && leon_b.HWRITE && leon_b.HADDR == read_addr)
	=> NEXT ((!(leon_b.HREADY && leon_b.HWRITE &&
	leon_b.HADDR == read_addr)
	&& !(leon_b.HREADY && !leon_b.HWRITE
	&& leon_b.HADDR == write_length))
	UNTIL! (!(leon_b.HREADY && leon_b.HWRITE
	&& leon_b.HADDR == read_addr)
	&& (leon_b.HREADY && !leon_b.HWRITE
	&& leon_b.HADDR == write_length)
	&&
	NEXT!((!(leon_b.HREADY && leon_b.HWRITE
	&& leon_b.HADDR == read_addr)
	&& leon_b.HRDATA != fft_size)
	UNTIL (!(leon_b.HREADY && leon_b.HWRITE
	&& leon_b.HADDR == read_addr)
	&& leon_b.HRDATA == fft_size)))))

Table 2 :

 2 Comparative assertions sizes

		TLM: PSL	TLM: Atomic	RTL: PSL	RTL: Atomic
		operators	expressions	operators	expressions
	(P I 1 )	4	7	11	29
	(P I 2 )	4	7	13	19
	(P I 3 )	4	4	4	10

Table 3 :

 3 Summary of some experimental results

dma_a.generate_irq_CALL() || leon_a.write_block_CALL().

Declaration of interests

☐ X The authors declare that they have no known competing financial interests or personal relationships that could have appeared to influence the work reported in this paper.

☐The authors declare the following financial interests/personal relationships which may be considered as potential competing interests:


Spondyloarthritis and sarcoidosis: related or fake friends? A systematic literature

Keywords: sarcoidosis, sacroiliitis, sacroiliac joint, spondyloarthritis, bone, granulomatous

Background: Sarcoidosis and spondyloarthritis (SpA) have been regularly associated. Bone iliac granulomas have also been described. We propose herein a systematic review of rheumatologic axial manifestations of sarcoidosis.

Methods: PubMed and the Cochrane Library were used to conduct this systematic literature review. Case reports and cross-sectional studies were reviewed according to Preferred Reporting Items for Systematic reviews and Meta-Analyses (PRISMA) guidelines.

Results: A total of 41 articles were eligible. Three cross-sectional studies on the association between SpA and sarcoidosis showed a prevalence of sacroiliitis and SpA ranging from 12.9 to 44.8% and 12.9 to 48.3% in inflammatory back pain (IBP) subgroups, respectively. However, the IBP definitions and sacroiliac joint (SIJ) imaging modalities (X-rays or magnetic resonance imaging) were heterogeneous, and X-ray was mainly used for sacroiliitis diagnosis (in 78% of cases). Thirty-one case-report articles of the sarcoidosis-sacroiliitis association were identified, representing 35 patients. ASAS criteria for SpA were met in half of cases (16/32) and 46% (12/26) had HLA B27 positivity. Sarcoidosis occurred after sacroiliac symptoms in 47% of cases. In the seven case-report articles with granulomatous sacroiliac bone involvement, unilateral involvement was significatively higher than in the sarcoidosis-sacroiliitis group (p < 0.001).

Conclusion:

Literature analysis found a good evidence of the association between SpA and sarcoidosis, and special attention should be given to patients reporting IBP. Unilateral sacroiliitis may raise suspicion of granulomatous bone involvement, distinct from sacroiliitis. Imaging modalities used to study the SIJ in patients with sarcoidosis have been heterogeneous and further investigation is needed.

Introduction

Sarcoidosis is a granulomatous disease of unknown origin [1]. Lungs with mediastinal lymph nodes are frequently involved, but granulomas can affect all organs, among which the skin, lymphoid system, eyes, and liver are the most common [1]. The musculoskeletal system is involved in 4 to 38% of patients [2], consisting of acute forms, such as Löfgren's syndrome, or chronic presentation, such as sarcoid arthropathy, with synovial sarcoid granuloma. Bone sarcoidosis is rare, reported in 3 to 13% of sarcoidosis patients [3].Sacroiliitis in sarcoidosis was initially described in 1951 by Verstraeten et al. in a case report [4]. It is characterized by sacroiliac joint (SIJ) inflammation and often inflammatory low back pain. Since the publication of this paper, links between sarcoidosis and sacroiliitis have been regularly reported in the literature. Most studies have reported radiographic sacroiliitis or bone iliac involvement but on a limited number of cases [5,6].

The aim of this systematic review was to identify the diagnostic characteristics, including radiological criteria, for sacroiliitis in patients with sarcoidosis and sacroiliac involvement. We included case reports and prospective and retrospective studies.

Methods

a. Publication search

This systemic review was performed in January 2020 using the Medline (using PubMed) and Cochrane databases. We identified articles in English and French using the Preferred Reporting Items for Systematic Reviews and MetaAnalysis (PRISMA) statement [7]. Keywords used in the search strategy were (sarcoidosis OR sarcoid OR sarcoid*) AND (sacroiliitis OR sacroiliac OR ankylosing spondylitis OR spondyloarthritis OR spondyloarthropathy). Additional relevant papers were identified through other sources, mainly from the bibliographies of previous papers.

b. Inclusion criteria

All study designs (case report, retrospective or prospective, cross-sectional) were included. After the removal of duplicates, we selected papers evaluating the SIJ in patients with sarcoidosis. Sarcoidosis had to be confirmed through histological proof of non-caseating granulomas, with exclusion of other granulomatous diseases, especially mycobacterial infections [8]. We did not include cases of granulomatous reaction following anti-tumor necrosis factor alpha (TNFα) therapy for spondyloarthritis (SpA) or other autoimmune diseases because the immunopathogenesis of sarcoidosis is not well known and because of the iatrogenic link of drug-induced sarcoidosis-like reactions (DISRs)[9] following anti-TNFα therapy. DISR due to anti-TNFα therapy is considered to be a differential diagnosis, according to the granulomatous "drug reaction" mentioned in the ATS/ERS/WASOG statement on sarcoidosis [8].

c. Collection data

We collected the following data from the case reports: sex, age at diagnosis, imaging used for the author's diagnosis of sacroiliitis, sacroiliitis according to the ASAS 2009 criteria[10], SIJ score on radiography based on the modified New York (mNY) criteria, ankylosis, HLA B27 status, presence of back pain (mechanical or inflammatory), back pain ≥ 3 months, age at onset < 45 years old, features of SpA (inflammatory back pain (IBP), arthritis, enthesitis, dactylitis, uveitis, psoriasis, inflammatory bowel disease, good response to NSAIDs, family history of SpA, elevated CRP), diagnosis of sarcoidosis (granuloma on biopsy and/or Löfgren syndrome), grading of sarcoidosis on thoracic radiography, granuloma-affected organs, and temporal relationship of sarcoidosis with SIJ symptoms (before, after, or concurrent diagnosis).

Results

In total, we identified 317 articles in PubMed, and 37 articles in the Cochrane Library. After removing duplicates and adding five articles identified in the bibliography of previously selected papers, 335 articles were screened. Based on the title and abstract, 265 articles were excluded and 70 were assessed for full-text eligibility. Twenty-nine full-text articles were excluded, mainly due to DISRs following anti-TNFα treatment. Finally, 41 papers were considered for the study. The PRISMA © -flow diagram is shown in Figure 1. Three of the 41 papers were cross-sectional studies [5,11,12] (summarized in Table 1). Among the remaining 38 case reports, two groups were identified: a sacroiliitis-sarcoidosis group [4,] and a group with granulomatous bone sacroiliac involvement mimicking sacroiliitis [6,[43][44][45][46][47][48]. The main characteristics of the sacroiliitis-sarcoidosis group are summarized in Tables 2 and3 and those of the group with sacroiliac bone involvement in Table 4.

a. Cross-sectional studies

In 2005, Erb et al.[11] published the first monocentric cross-sectional cohort study of back pain in a sarcoidosis population, in which 61 patients were analyzed. Almost all patients were Caucasian, with a sex-ratio close to one. Five patients did not meet the ATS/ERS/WASOG criteria for sarcoidosis due to the absence of compatible histology and Lofgren's syndrome, but were nevertheless considered to have sarcoidosis and included in the study. Radiographic evaluation of the SIJ was performed by double reading, but the criteria for a diagnosis of sacroiliitis was not mentioned. The authors considered four patients to have sacroiliitis with only one patient with bilateral involvement. Radiological sacroiliitis was considered independently of a SpA diagnosis in this study, but one patient had HLA B27 antigen. There was no difference between patients with or without sacroiliitis in this study. The prevalence of sacroiliitis was estimated to be 6.6% (4/61) in the sarcoidosis population, 8.2% (4/49) in the back-pain sub-group, and 12.9% (4/31) in the IBP subgroup. Kobak et al.[5] reported six cases of bilateral sacroiliitis scored according to mNY criteria based on standard pelvic radiography in a monocentric cohort of 42 patients with biopsy-proven sarcoidosis. All patients in the X-ray sacroiliitis group had IBP according to Calin criteria. The authors thus diagnosed six cases of SpA according to ASAS 2009 criteria [10]. SpA-sarcoidosis patients were more likely to be female and lacking HLA B27. Eight patients without sacroiliitis also had IBP. The prevalence of sacroiliitis and SpA in the sarcoidosis population was estimated to be 14.3% (6/42) and 43% (6/14) in the IBP subgroup. Sigaux et al.[12] recently published a prospective study of back pain with MRI exploration in a biopsyproven sarcoidosis cohort of 337 patients. Among 64 back-pain patients, 29 had IBP. The diagnosis of sacroiliitis was defined as bone-marrow edema in a compartment of the SIJ on one slice for bilateral lesions or on two consecutive slices for unilateral localization. Two blinded readers (one rheumatologist and one radiologist) analyzed MRI, and a consensus was reached in case of disagreement. Sacroiliitis was diagnosed in 13 patients with IBP (5 also had radiographic sacroiliitis according to the mNY criteria). The patient characteristics in the sacroiliitis subgroup were not reported. SpA was diagnosed in all patients with sacroiliitis; one patient with mechanical pain was diagnosed with SpA due to the association of HLA B27 positivity, psoriasis, and enthesitis and one patient had a vertebral inflammatory