Hubert Garavel

Claude Helmstetter

Olivier Ponsini

Wendelin Serwe

Verification of an Industrial SystemC/TLM Model using LOTOS and CADP

des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

Embedded systems combine on a single circuit several hardware components with embedded software. To cope with the increasing complexity and time-to-market pressure, system level descriptions are increasingly used as reference descriptions. SystemC/TLM [START_REF]SystemC v2.2.0 Language Reference Manual (IEEE Std 1666-2005[END_REF][START_REF] Ghenassia | Transaction-Level Modeling with SystemC[END_REF] is a widely used standard for describing a complex system-on-chip at system level. Due to its fast simulation engines, SystemC/TLM is particularly useful for testing the embedded software, even before the hardware architecture is completely specified.

A system level description generally consists of a set of interconnected modules executing concurrently. Dealing with concurrency is known to be complex due to the many possible interleavings. Because this also holds for a systemon-chip, verification of system level descriptions is required to detect design errors as soon as possible.

The development of a verification tool dedicated to Sys-temC/TLM is a complex task, because a SystemC/TLM description can contain arbitrary C++ code (SystemC and TLM are actually implemented as C++ libraries). Existing approaches to formal verification of SystemC/TLM translate the complete model into a language accepted by a verification tool (see section 3.2). Such a complete translation requires a significant effort and has the inconvenience that the model under verification is not exactly the same as the reference SystemC/TLM model used for design and test.

In this paper, we present an approach for the validation of a SystemC/TLM description by translation into LOTOS and use of the CADP toolbox [START_REF] Garavel | CADP 2006: A toolbox for the construction and analysis of distributed processes[END_REF]. We extend the approach of [START_REF] Ponsini | A schedulerless semantics of TLM models written in SystemC via translation into LOTOS[END_REF] by reusing as much as possible of the original C++ code. In particular, we reuse a large part of the C++ code (namely the parts corresponding to local computations of processes) to implement LOTOS operations.

We have experimented with our approach on a complex component of an industrial circuit, namely the BDisp graphical processing unit designed by STMicroelectronics (≈25,000 lines of SystemC/TLM). This led to optimizations of our approach, reducing the memory requirements for formal verification.

The remainder of this paper is organized as follows. Section 2 gives an overview of SystemC and TLM. Section 3 presents related work. Section 4 gives an overview of LO-TOS. Section 5 presents our approach to the verification of SystemC/TLM. Sections 6 and 7 present the BDisp model and its LOTOS translation. Section 8 reports on our experiments with the verification toolbox CADP. Finally, Section 9 concludes.

SystemC and TLM

SystemC [START_REF]SystemC v2.2.0 Language Reference Manual (IEEE Std 1666-2005[END_REF], a standard published by the Open SystemC Initiative (OSCI), is a C++ library providing classes to describe heterogeneous systems composed of hardware and software. The architecture of a system is defined by a set of modules connected by synchronous or asynchronous ports and channels (sc module, sc port, ...). Each module contains zero, one, or more processes (SC_THREAD) describing the behavior of the system. SystemC processes interact using shared memory or communication channels, and are synchronized using SystemC events (sc_event e, e.notify(), wait(e)) and timing annotations (sc_time t, wait(t)).

Each SystemC process is a C++ method that is executed by the SystemC scheduler, communicates with other processes using shared memory, and may explicitly suspend itself by executing a wait statement. When the process is resumed by the scheduler, its execution continues from the wait statement. Each SystemC process is eligible or running or waiting for a SystemC event. There is at most one running process at a time. If the running process notifies an event, then all processes waiting for this event move from waiting to eligible.

The Transaction Level Modeling (TLM) library [START_REF] Ghenassia | Transaction-Level Modeling with SystemC[END_REF] built upon SystemC provides a transaction mechanism that encapsulates communication protocols (data transfer and synchronization) between modules, accelerating both model design and simulation. Using a transaction, a process in an initiator module can directly call the methods exported by a target module. A process can thus read many values from a memory or set many registers of a peripheral without any costly inter-process synchronization (no context switch is required). Names and attributes of exported functions depend on the protocol. In general, a protocol provides at least read and write functions, but a protocol for a transaction modeling an interrupt might be reduced to only one function without argument. At the TLM level of abstraction, processes inside the same module communicate using Sys-temC events and shared variables. A TLM model can be timed or untimed: a timed model contains timing annotations (sc_time t, wait(t)) whereas an untimed model does not. An untimed model includes more possible behaviors than a timed model, increasing the coverage, but also the cost, of the verification.

Existing approaches to TLM verification

The OSCI provides an open-source simulator for Sys-temC/TLM and a library SCV to ease test generation. However, the OSCI does not provide tools for formal verification. Moreover, while the SystemC specification allows many schedulings for a given test case, the OSCI simulator exhibits always the same scheduling. Thus, even if an execution leads to the expected result, another execution with a different scheduling may be erroneous. This issue has been addressed by many publications. Two approaches have been investigated: stateless model checking of a SystemC/TLM program, and translation of a SystemC/TLM program to a language for which a model checker is available.

Stateless model checking

The first approach is based on the execution of the Sys-temC/TLM program using an enhanced SystemC simula-tor capable of exploring each test case with many schedulings. One solution is to implement a random scheduler; this increases error detection but the resulting coverage is uncertain. Another option is to try all valid schedulings, but this technique does not scale up to industrial examples. In contrast, stateless model checking techniques based on dynamic partial order reduction [START_REF] Helmstetter | Automatic generation of schedulings for improving the test coverage of systems-on-a-chip[END_REF][START_REF] Kundu | Partial order reduction for scalable testing of SystemC TLM designs[END_REF][START_REF] Blanc | Race analysis for Sys-temC using model checking[END_REF] select only a small subset of the valid schedulings, and so scale up to medium sized industrial examples. The generated subset of schedulings is large enough to guarantee that all local errors (i.e. assertion violations) and deadlocks are found.

A SystemC/TLM program can contain loose timing annotations (e.g., an interval of realistic values [T -d, T + d] instead of an exact duration T ) if the timing of the real system is uncertain. At runtime, a simulation engine can draw a particular value inside each interval. Again, random simulation does not ensure coverage. Dynamic partial order reduction combined with linear programming techniques can be used to generate a set of schedulings and timings that guarantee to find all local errors and deadlocks for a given test case [START_REF] Helmstetter | Test coverage for loose timing annotations[END_REF].

All the stateless model checking techniques [START_REF] Helmstetter | Automatic generation of schedulings for improving the test coverage of systems-on-a-chip[END_REF][START_REF] Helmstetter | Test coverage for loose timing annotations[END_REF][START_REF] Kundu | Partial order reduction for scalable testing of SystemC TLM designs[END_REF][START_REF] Blanc | Race analysis for Sys-temC using model checking[END_REF]] that have been implemented for SystemC/TLM programs can be applied only to bounded test scenarios.

Translation-based approaches

For programs that do not terminate, a second approach has been investigated. The idea is to translate the Sys-temC/TLM program to be verified to another language, and then verify the translated program using an existing stateful model checker. This approach has first been applied to the RTL level SystemC descriptions [START_REF] Drechsler | Reachability analysis for formal verification of systemc[END_REF][START_REF] Große | CheckSyC: an efficient property checker for RTL SystemC designs[END_REF].

Many translations and languages have been proposed for the validation of transactional models, like [START_REF] Niemann | Formalizing TLM with communicating state machines[END_REF], which translates SystemC/TLM programs into finite state machines (FSM), or like [START_REF] Kroening | Formal verification of SystemC by automatic hardware/software partitioning[END_REF], which describes abstraction techniques and a translation from SystemC/TLM to labeled Kripke structures. Like our approach, most of these translations are manually, a notable exception being the LusSy tool chain [START_REF] Moy | LusSy: an open tool for the analysis of systems-ona-chip at the transaction level[END_REF], which automatically translates TLM models into synchronous automata with variables; it provides some simple abstraction techniques (e.g., abstract address representation). The LusSy tool chain has been connected to many model checkers, including symbolic model checkers based on BDD or SAT. Some small examples have been successfully verified, but industrial examples face the state space explosion problem.

The state space explosion problem appears chiefly because TLM models are mainly asynchronous. Indeed, after each transition, there are many valid scheduling choices that should be explored. It is therefore suitable to use the model checkers for asynchronous programs, as these model check-ers have been specifically optimized to fight state space explosion arising from asynchrony. For example, the SPIN model checker uses partial orders to reduce state spaces; a translation of TLM to Promela is described in [START_REF] Traulsen | A SystemC/TLM semantics in Promela and its possible applications[END_REF], allowing the use of SPIN to verify TLM models. Also, we recently proposed a translation of TLM to LOTOS [START_REF] Helmstetter | A comparison of two SystemC/TLM semantics for formal verification[END_REF] that enables verification of the benchmark of [START_REF] Traulsen | A SystemC/TLM semantics in Promela and its possible applications[END_REF] for a slightly greater number of processes than using SPIN; we pursue this line of work in the present paper.

All the translations we have presented in this subsection have given successful verification results only on small examples (a few hundred lines of code). This paper tries to go beyond this limit by addressing larger problems, namely an industrial example of about 25,000 lines of SystemC/TLM code.

LOTOS

The ISO standard LOTOS [START_REF] Iso/Iec | LOTOS -a formal description technique based on the temporal ordering of observational behaviour[END_REF] (Language Of Temporal Ordering Specification) is a process algebra used to describe asynchronous concurrent processes communicating and synchronizing by rendezvous on gates. In the following we briefly introduce the main concepts of LOTOS occurring in the examples of this paper; for a complete description of LOTOS, we refer the reader to existing tutorials, such as [START_REF] Bolognesi | Introduction to the ISO specification language LOTOS[END_REF].

LOTOS specifications are composed of a data part and a behavior part. Data values and operations are described by algebraic specifications in the style of ACTONE [START_REF] Ehrig | Fundamentals of Algebraic Specification 1 -Equations and Initial Semantics[END_REF]. Types define a collection of sorts, operations on sorts, and equations describing the meaning of operations.

Behaviors are expressed by terms combining processes with algebraic operators. Figure 1 gives a simplified grammar of LOTOS behaviors; lower case identifiers stand for terminals and upper case identifiers for non terminals (P is a process name, G a gate name, X a variable name, S a sort name, and V a value expression).

As usual in process algebras, the semantics of a LO-TOS specification is defined operationally by a translation of LOTOS into a Labeled Transition System (LTS). Here, we only sketch the meaning of behavioral operators. A communication "G O 1 .... O n ; B" on a gate G allows to communicate several values O i , called offers, either for emission (!) or reception (?); then behavior B is executed.

"B 1 []B 2 " specifies a nondeterministic choice between be- haviors B 1 and B 2 . "B 1 |[G 1 , ..., G n ]|B 2 "
specifies the parallel composition of B 1 and B 2 synchronizing on the gates G. Synchronization on gates with offers only occurs if the offers are compatible (same number of offers, same types, and same or compatible values). A behavior B can be guarded by a Boolean expression V : "[V ]-> B" specifies that B will only be executed if V is true. "let X:S=V in B" allows to define a variable X of sort S that is initial-

B ::= G O 1 ... O n ; B (communication) | B 1 []B 2 (choice) | B 1 |[G 1 , ..., G n ]|B 2 (parallel) | exit(V 1 , ..., V n ) (termination) | [V ]->B (guard) | let X : S = V in B (variable definition) | P [G 1 , ..., G m ](V 1 , ..., V n ) (process call) O ::= !V | ?X : S (offer) Figure 1. Grammar of LOTOS (excerpt)
ized to value V and used in B. Finally, a behavior B can be given a name by declaring a process P parameterized by sets of gates (G i ) and of variables (X i of sort S i ) as follows:

"process P [G 1 , ..., G m ](X 1 :S 1 , ..., X n :S n ): exit := B endproc".

Translating a TLM model into LOTOS

To translate an untimed SystemC/TLM model into a LO-TOS specification, we extend the translation approach described in [START_REF] Ponsini | A schedulerless semantics of TLM models written in SystemC via translation into LOTOS[END_REF]. This approach splits a SystemC/TLM model in two parts that are handled differently:

1. communications and synchronizations between Sys-temC/TLM processes, i.e., the SystemC/TLM specific code; the translation of this code into LOTOS behaviors is described in [START_REF] Ponsini | A schedulerless semantics of TLM models written in SystemC via translation into LOTOS[END_REF].

2. local computations within a single module, e.g., classes, methods, sequential control, data manipulation; the translation of this code into LOTOS data types is not detailed in [START_REF] Ponsini | A schedulerless semantics of TLM models written in SystemC via translation into LOTOS[END_REF].

The present paper reduces this translation effort by reusing most of the non SystemC/TLM specific C++ code of the original model. Our approach takes advantage of a particular capability of CAESAR (the LOTOS to C compiler included in the CADP verification toolbox [START_REF] Garavel | CADP 2006: A toolbox for the construction and analysis of distributed processes[END_REF]), which allows the possibility to implement LOTOS sorts (respectively, LOTOS operations) by external C data types (respectively, C functions).

For each SystemC/TLM module described by a C++ class M , we create a corresponding LOTOS model importing C/C++ code, as follows:

1. We define, in C, a compact representation M C of the class M . A value of type M C is called module state. This type will be used by the model checker to store and compare the explored states.

2. We define a LOTOS sort M LOTOS corresponding to M C , and we declare a set of LOTOS operations allowing to access or modify a module state (i.e., an element of M C ). 3. We translate each SystemC/TLM process of M into a LOTOS process, using the aforementioned LOTOS operations for the local computations, and applying the translation rules of [START_REF] Ponsini | A schedulerless semantics of TLM models written in SystemC via translation into LOTOS[END_REF] for the communications.

4. We extract from the original SystemC/TLM module the C++ code needed to implement the LOTOS operations.

5.

We implement an interface between this C++ code extracted in the previous step, and the LOTOS code (compiled to C using the LOTOS to C compiler CAESAR).

The following subsections detail these five steps, using the following SystemC/TLM module M as a running example.

class M : public sc module { sc port<...> tlm port; data t data; ... void compute() { / * SC THREAD * / while(!stream.full()) { addr+=4; data=tlm port.read(addr); stream<<data; wait();}} };

Definition of the C type M C

The first step is to define a compact representation M C of the SystemC/TLM module described by the class M . M C is a C structure (struct type) M C that contains all the members of M the values of which are not constant. Notice that the C++ class M is aimed at fast simulation, whereas M C is aimed at state space exploration and verification. Therefore, reducing the memory footprint of M C is more important than reducing the access time to each of its fields. Hence, each field of M C should be represented with the minimum number of bits (e.g., no more than one bit for a boolean value) and padding bits should be avoided as far as possible. Furthermore, each value of M C should have a unique memory representation to ease comparing and storing.

In addition to the C structure M C , CAESAR also requires the user to provide the following C functions:

• a comparison function taking two module states of type M C as argument, used during state space exploration to decide whether a state has already been encountered (e.g., memcmp(), if the structure M C contains no padding)

• a printing function for states of type M C .

Definition of the LOTOS sort M LOTOS

According to the different ways processes operate on the state of a module M , the LOTOS operations to manipulate values of sort M LOTOS have one of the following three profiles, where each T i is a type used both in LOTOS and C++, such as addr t, data t, or Bool :

• M LOTOS → T r : an operation of this profile corresponds to an access to the state without side-effect.

The case where T r = Bool corresponds to the evaluation of a condition.

• M LOTOS × T 1 × • • • × T n≥0 → M LOTOS :
an operation of this profile corresponds to a modification of the state of the module as a "side-effect" of executing an instruction, as for instance an assignment. Notice that as in any pure functional language, side effects can only be represented by passing the current state before the call as an additional first parameter and return the state after the call as return value.

• M LOTOS × T 1 × • • • × T n≥0 → M LOTOS × T r :
an operation of this profile corresponds to a modification of the state that also returns a value. As a LOTOS operation can return only one single value, it is necessary to define an additional LOTOS sort for each pair M LOTOS , T r , together with operations to access the elements of this pair.

At this stage, we just have to declare these operations in LOTOS; they will be implemented in C++ as described in 5.4 and 5.5.

In the running example, we have to declare the four LOTOS sorts M LOTOS , data t, addr t, and M LOTOS , addr t . The implementations of data t and addr t of the original SystemC/TLM model can be reused directly. The sort M LOTOS , addr t is implemented as a C structure with two fields (named state and addr).

We also have to declare the following operations:

• M stream full : M LOTOS → Bool evaluates the C++ condition stream.full().

• M compute 1 : M LOTOS → M LOTOS , addr t simulates the process compute up to the transaction.

• M compute 2 : M LOTOS , data t → M LOTOS simulates the process compute from the transaction to the wait() statement.

Translation of the processes of M

Using the operations of M LOTOS , the SystemC/TLM processes can be translated into LOTOS processes according to the rules described in [START_REF] Ponsini | A schedulerless semantics of TLM models written in SystemC via translation into LOTOS[END_REF]: each SystemC/TLM process is translated to a LOTOS process; the shared variables and the SystemC events are modeled using additional LO-TOS processes; finally, all these LOTOS processes are interconnected using LOTOS parallel composition operators.

In the running example, the process M ::compute() is translated into the following LOTOS process:

process

Split of the methods of M

To reuse the code of M , one must first make a copy of class M by removing all occurrences of SystemC/TLM specific types (such as inheritance from sc_module and the port tlm port); we still note M this modified class. Then, to reuse the methods of M when implementing the operations of M LOTOS , we extract corresponding fragment methods from each method of M . Note that the code reused does not contain any SystemC/TLM specific statement.

The modified class M is:

class M /*

Implementation of the LOTOS operations as C++ functions

The operations of M LOTOS are implemented by C++ functions (declared as C functions to enable linking with the C code generated by CAESAR), which initialize an object of type M according to the module state M C , call the corresponding fragment method of M , and copy the resulting state of M back into a new value of type M C . Therefore, the user must also provide two functions M C to M () and M to M C (), which convert between a module state (a value of the structure M C ) and a state of the module M .

In the running example, M compute 1() is implemented as follows:

extern M module; M C , addr t M compute 1 (M C mc) { M C ,

The BDisp and its SystemC/TLM model

In the rest of this paper, we illustrate our verification approach on the SystemC/TLM model of a graphical processing unit that is used in real circuits.

The BDisp

The BDisp is an IP (Intellectual Property) designed by STMicroelectronics. It is a 2D-graphics co-processor implementing Blit (Block Image Transfer) and numerous graphical operators, e.g., rotations, alpha blending, or Blue Ray disc decoding. A job is a sequence of operations that the BDisp must perform to generate a video stream. Both real-time jobs and non-real-time jobs are supported.

The BDisp is software-controlled by memory-mapped registers and instruction queues stored in memory. In order to program a job, the embedded software fills an instruction queue describing the graphical operations to be applied. Next, the embedded software starts the job execution by writing into the BDisp registers; then, it can check the status of a queue by reading the BDisp registers.

There are two kinds of queues: composition queues (CQ) for real-time jobs, and application queues (AQ) for nonreal-time jobs. The BDisp processes one queue at a time, scheduling the queues according to their priorities. The BDisp receives interruptions generated by the Video Timing Generator (VTG). These interruptions, together with the information contained in instruction queues, controls the execution pace of the composition queues in order to satisfy real-time constraints. Additionally, the CPU can suspend a queue or change its priority by writing to BDisp registers.

The BDisp provides many types of interruption to manage all situations, but the interruptions generated by the BDisp are not relevant for the properties addressed in this paper.

The BDisp SystemC/TLM model

STMicroelectronics provided us with a SystemC/TLM model of the BDisp. This model is large: it consists of 22 files, totaling to about 25,000 lines of code.

The BDisp SystemC/TLM model is designed at a level of abstraction tailored to functional validation. The code contains a few wait instructions with a duration. These timed wait instructions are used to allow the other processes to be executed. However, the durations are not precise enough to allow performance evaluation.

Simulating the BDisp requires several additional models: a model of the CPU, a model of the VTG, a model of the memory, and a model of the bus. The CPU model is a socalled "native wrapper": the embedded code, written in C, is included in the SystemC/TLM code, and the accesses to the BDisp registers are instrumented in such a way that each register access generates a transaction. All these models are quite simple compared to the BDisp model.

The SystemC/TLM module describing the BDisp implements several sorts of connections. Communication between the bus and other components (BDisp, CPU, and memory) is modeled using the TAC TLM protocol designed by STMicroelectronics [START_REF]TAC Package[END_REF]. Communication between the BDisp and the VTG uses interrupts and is modeled by another TLM protocol (the BDisp module exports one method that is called by the VTG process to notify an interruption).

Internally, the BDisp module contains only one Sys-temC/TLM process, which is an SC_THREAD. That does not mean an absence of concurrency inside the BDisp. Indeed, two external processes, the CPU and the VTG, can simultaneously execute code inside the BDisp module by calling its exported methods.

STMicroelectronics provided us with some test scenarios to validate the BDisp. Each test scenario is composed of a piece of C code to program the BDisp, a memory dump containing the instruction queues, and the expected outputs.

All the tests run well and reveal no error. However, as the OSCI simulator is used, each test is executed with only one single scheduling. Moreover, the simulations are driven by particular timing annotations, which may differ from the real system. Modeling the BDisp in LOTOS will allow us to explore more situations and, possibly, detect more synchronization errors than by using the test scenarios.

The BDisp LOTOS model

Overview

Primarily, our goal was to validate the control part of the BDisp, e.g., all issues related to interprocess synchronization. We were interested neither in validating the sequential graphical operators (CADP is primarily aimed at validating concurrent algorithms) nor the embedded software that controls the BDisp (we have no access to it). Consequently, our LOTOS model describes only the features and the external components that are relevant to the control part of the BDisp.

Following the method presented in section 5, we define the C structure type BDisp C and the LOTOS sort BDisp LOTOS , and we implement the operations on BDisp LOTOS using C++ functions extracted from the original SystemC/TLM model. To minimize the size of the type BDisp C , we store only the registers that are meaningful to the control. For some registers, we do not need to store all the bits. For example, in the SystemC/TLM state, the register BLT CTL uses 32 bits, but we are only interested in the 31th bit. Thus, the type BDisp C is implemented using bit fields: struct {int BLT_CTL_31:1; ...} BDisp C ; and the conversion from the LOTOS state to the Sys-temC/TLM state uses bitwise operations: sc_state.registers [BLT_CTL_ID].value = lotos_state.BLT_CTL_31<<31; After these optimizations, the C structure BDisp C occupies only 52 bytes to store the state of a BDisp with 2 composition queues, 4 application queues, and a maximum number of screen lines reduced to 4; instead, the C++ class BDisp uses about 40 kilobytes.

Once the LOTOS sorts are defined, we translate the three SystemC/TLM processes (BDisp, VTG, and CPU) in three concurrent LOTOS processes, called BDisp process, CPU, and VTG. These three LOTOS processes can read and modify the contents of the BDisp module, which we model as a shared variable of type BDisp LOTOS . In our LO-TOS model, this shared variable is encapsulated in a process called BDisp state.

Next, we inline the code of the exported functions in the corresponding initiator process, because we have shown in [START_REF] Helmstetter | A comparison of two SystemC/TLM semantics for formal verification[END_REF] that transaction inlining reduces the number of states. This means that:

• the code of the BDisp module used to set or get the value of each register is inlined in the CPU LOTOS process;

• the code of the BDisp module used to simulate the effect of a video synchronization is inlined in the VTG LOTOS process.

The BDisp module contains two SystemC events, which we model using a dedicated LOTOS process called event handler, as described in [START_REF] Ponsini | A schedulerless semantics of TLM models written in SystemC via translation into LOTOS[END_REF].

The architecture of the LOTOS model is shown on Figure 3. There are five LOTOS processes, three of which correspond to the three SystemC/TLM processes Our approach allowed us to reuse about 5500 lines of the original SystemC/TLM code (which is, in fact, C++ code), the remaining lines being not related to control. We have written 1000 lines of LOTOS code, and about 2500 lines of C/C++ code for the interface. A complete SystemC/TLM to LOTOS translation, as described in [START_REF] Ponsini | A schedulerless semantics of TLM models written in SystemC via translation into LOTOS[END_REF], would have required far more work.

Abstractions and simplifications

The original SystemC/TLM model contains a lot of details that are not relevant for verifying the control part of the BDisp. We present in this section the abstractions and simplifications we applied, still preserving the potential issues.

CPU commands. In the original SystemC/TLM model, sending a command from the CPU to the BDisp is achieved by a TLM write transaction T r. The address of T r is obtained by adding the register offset to the base address of the BDisp. The command arguments are encoded in the 32-bit data field of T r. As we are not interested in this encoding mechanism, we represent all possible BDisp commands by a new LOTOS type CPU command. This brings three benefits:

• this new type requires fewer bits than a numeric offset;

• we can iterate efficiently over the registers (this is used in the CPU to generate a command nondeterministically);

• no model of the bus is required.

Instruction nodes. Each instruction node is significantly reduced by removing anything unrelated to control. For an instruction node of a composition queue CQn, we keep only two Booleans and one screen line number (reduced to the range 0 . . . 3). For an instruction node of an application queue AQn, we need only two Booleans. Thus, the instruction nodes are small enough to be enumerated efficiently.

Instruction queues. Once an instruction queue is triggered, the BDisp reads an instruction node from the memory. Since we focus on the verification of the BDisp, we assume that the embedded software controlling the BDisp has correctly written the instructions to the memory before triggering the queue. Thus, we can use lazy evaluation to model the instruction queues. Instead of generating the contents of an instruction queue when it is filled in by the CPU, we wait until the BDisp reads it. Each time a new instruction node is read by the BDisp, we generate its contents nondeterministically. The benefits are twofold:

• we can remove the code that writes instruction nodes to the memory;

• we store at most one node per instruction queue, reducing the memory size of a state.

This abstraction may prevent detection of bugs due to concurrent accesses to a node, but such bugs are possible only with erroneous embedded software, and, as said above, we assume that this software is correct.

Boolean abstraction of counters. After a few experiments, we noticed that two integer variables could increase infinitely, leading to an infinite state space. After examining the code and the test scenarios provided by STMicroelectronics, we concluded that we could safely assume that these variables take only two values, and thus be abstracted by booleans. To check the correctness of this abstraction, we applied the same modification to the original SystemC/TLM model, and we ran the test scenarios provided by STMicroelectronics again. The simulation results are identical, which confirms the correctness of our abstraction.

Accessing the BDisp state

The contents of the BDisp module are stored in the variable state of the process BDisp state. The variable state is of sort BDisp LOTOS , which is implemented using the C type BDisp C . Many functions access or modify this variable. For example, the function ExeSetCommand_CIF simulates the effect of a CPU command (i.e., a write to a BDisp register); this function takes a BDisp state and a CPU command as arguments, and returns the updated BDisp state.

To model a variable such as state, which is shared between several processes, the usual solution in process algebra is based on a READ/WRITE mechanism: the LOTOS process BDisp state storing the variable value has two gates READ and WRITE, used to send the current value and get the new value.

Here is how the CPU can write to a BDisp register using the READ/WRITE mechanism: First, the BDisp state process sends its current state to the CPU process. Next, the CPU process executes the command. Finally, the CPU process sends back the new state to the BDisp state process.

When using the READ/WRITE mechanism, the code of the BDisp state process is quite simple. Moreover, it is easy to implement a lock to prevent concurrent accesses to the BDisp state: a READ rendezvous locks the state, a WRITE rendezvous unlocks it.

However, the BDisp case study revealed a drawback of the READ/WRITE mechanism. The BDisp state is sent to three processes (CPU, VTG, and BDisp process). Eventually, many processes contain one or several local variables of sort BDisp LOTOS . In a first version of the BDisp LO-TOS model, there were 17 such variables, using 52 bytes of memory each, leading to excessive memory consumption for states of the LOTOS model (about 1 kilobyte per state).

We therefore designed a different mechanism, named EXECUTE/RETURN, to avoid this duplication of BDisp state local copies. In this approach, the gates WRITE and READ are replaced by the gates EXECUTE and RETURN. The initiator process (e.g., the CPU) sends an opcode to the BDisp state process using the EXECUTE gate. The BDisp state process decodes the opcode and executes the corresponding function. If the function returns some values (in addition of the new BDisp state), these values are send back to the initiator process using the RETURN gate. The lock mechanism is implemented by adding two boolean offers to each EXECUTE or RETURN communication: the first boolean specifies whether to take the lock or not, the second whether to release it or not.

This EXECUTE/RETURN mechanism requires more LOTOS code than the usual READ/WRITE mechanism, because a new type has to be implemented to store the opcodes, and because the BDisp state process contains specific code for each function of the BDisp LOTOS sort. But the EXECUTE/RETURN mechanism is very profitable in presence of large shared variables. Indeed, we reduced the state size for the whole LOTOS model from one kilobyte down to 104 bytes, i.e., by an order of magnitude.

However, the EXECUTE/RETURN mechanism might increase the number of transitions in the LTS. Suppose that a process wants to execute an atomic sequence of operations o 1 , . . . , o n on the BDisp state. Using the classic mechanism, a single READ and a single WRITE transitions are enough. Instead, the EXECUTE/RETURN mechanism requires, for each operation o i , one EXECUTE transition and possibly one RETURN transition. To avoid this increase of the LTS size, it is possible to aggregate the atomic se-quence o 1 , . . . , o n in a single new operation o . Thus, only one EXECUTE transition is required, and one RETURN transition if the sequence o returns some values. Aggregation works as long as the operations of an atomic sequence are not separated by other LOTOS transitions; in particular, this approach worked well on the BDisp case study.

Experiments and results

Interactive and random simulation

The LOTOS model of the BDisp were simulated using the Open/Caesar Interactive Simulator (OCIS). Compared to simulating the SystemC/TLM model with the simulator provided by the OSCI, using OCIS offers two benefits:

• the simulation is interactive: the user can choose the CPU commands, the contents of the instruction nodes, and how the processes are scheduled

• the user can freely backtrack to any previous state, because OCIS stores the tree of explored states.

Another possibility to simulate the LOTOS model would be to use the random simulator tool Executor of CADP. Contrary to the OSCI SystemC simulator, Executor chooses the scheduling nondeterministically.

Generation of the full LTS

Beyond simulation, we aimed at formal verification by generating the labeled transition system (LTS) corresponding to our LOTOS model of the BDisp.

Early attempts indicated that the LTS of this LOTOS model is too large to be generated. On a 64 bit Linux machine (2 GHz Opteron), we interrupted the generation after 3 hours and 20 minutes (at this point, the generation required 15.7 gigabytes of memory). The graph obtained contained 155,377,179 states and 371,146,000 transitions. It is likely that the full graph is many times bigger.

To fight the state explosion, we applied the compositional verification techniques offered by CADP. We could generate the LTS of the CPU (45 states after reduction), the LTS of the VTG (21 states), and the LTS of the BDisp process (124 states). However, we could not generate the LTS of the BDisp state process, which may be as big as the LTS of the full system. Consequently we could not use compositional verification.

Model checking of verification scenarios

Because we could not generate the full LTS, we decided to concentrate on verification scenarios, that restrict the inputs to some of their most realistic values. • scenarios "AQn", with n ∈ [1.

.4]: we trigger n application queues (n × 3 CPU commands), the VTG is disabled since it has no effect on the application queues;

• scenarios "CQ1AQn", with n ∈ [0..4]: we trigger 1 composition queue and n application queues (n×3+3 CPU commands), the VTG is enabled;

• scenario "CQ1AQ1+RESET": we add a soft reset to the scenario CQ1AQ1 (6+1 CPU commands).

For each of these ten scenarios, we generated the LTS (see Table 1) and minimized for branching bisimulation (using the bcg min tool of CADP). We expressed five properties using regular alternationfree mu-calculus formulas [START_REF] Mateescu | A model checking language for concurrent value-passing systems[END_REF], and evaluated them on the minimized LTS corresponding to the verification scenarios, using the Evaluator 3.5 model checker of CADP.

• P1: if a composition queue is triggered before any application queue, and if the composition queue is not suspended, then no application queue can be executed.

• P2: if a composition queue is triggered but not disabled, then there exists always a path to execute it.

• P3: if an application queue is triggered but not disabled, then there exists always a path to execute it.

• P4: if the CPU sends a RESET command to the BDisp, then the BDisp can still read one node but not two.

• P5: property expressing the absence of deadlock.

The property evaluation results are given in Table 1. The evaluation of all the properties for all the reduced LTS took about 45 seconds. Most of the results were as expected, in particular:

• The scenarios AQn do not satisfy property P5 (no deadlock), because the BDisp stops normally when all application queues are completely executed, and the VTG is disabled.

• The property P1 is false when a reset is possible. Indeed, if the reset occurs after CQ1 triggering but before AQ1 triggering, then AQ1 is executed first.

However, one would have expected properties P2 and P3 to be satisfied by all scenarios AQn and CQ1AQn, but for instance P2 does not hold for scenario CQ1AQ1. The diagnostic generated by Evaluator exhibited a scheduling leading to a wrong behavior of the BDisp. Indeed, if the CPU is scheduled too often before the BDisp, the latter may miss an event notification, and thus not execute properly. Using an interactive SystemC scheduler, we noticed that this scheduling is reproducible on the untimed version of the SystemC/TLM model (i.e., replacing delayed notifications by immediate notifications), but not on the timed version (nor on the actual circuit itself). We proposed a modification of the SystemC/TLM model so that the property holds also in an untimed context.

Conclusion and future work

We presented an approach to apply model checking to SystemC/TLM models. In our approach a large part of the C++ code present in these models is reused, while the remaining part of the SystemC/TLM code is translated into LOTOS according to the systematic rules of [START_REF] Ponsini | A schedulerless semantics of TLM models written in SystemC via translation into LOTOS[END_REF]. Contrary to other approaches, our approach avoids the complete translation of the SystemC/TLM model into the particular input language of the model checker considered. Thus, formal verification is better integrated in the design flow, the translation effort is reduced, and the confidence in the results is increased.

We applied this approach to a large industrial case study, namely the BDisp designed by STMicroelectronics. Although we were not able to explore the entire state space of the whole system, we managed to analyze large subsets of it and to prove several correctness properties on realistic verification scenarios. Using the verification tools of CADP [START_REF] Garavel | CADP 2006: A toolbox for the construction and analysis of distributed processes[END_REF], we discovered an issue that makes the original timed SystemC/TLM model incompatible with a semantics for untimed TLM models (e.g., the one of [START_REF] Ponsini | A schedulerless semantics of TLM models written in SystemC via translation into LOTOS[END_REF]).

As regards future work, a first line of research would be to elaborate guidelines to write SystemC/TLM models so as to reduce the amount of work required to obtain a verifiable LOTOS model. For instance, to enable partial order reductions and compositional verification of the LOTOS model, it seems that the SystemC/TLM models should be split into many small processes rather than a big monolithic one.

As a second line of research, we are currently developing a LOTOS/SystemC library that helps reusing even more of the original C++ code, including SystemC/TLM specific code.

Figure 2 .

 2 Figure 2. LOTOS model reusing C++ code

Figure 3 .

 3 Figure 3. Architecture of the LOTOS model

Table 1 .

 1 Results of the experimentscase study, a verification scenario is mainly a sequence of CPU commands that do something useful, like triggering the queues, whereas the control information of the instruction nodes is chosen nondeterministically.

	For the BDisp

Acknowledgments.

We are grateful to L. Ducousso, D. Hermitte, and R. Hersemeule (STMicroelectronics) for providing us with the BDisp case study and for their help with this work.

* This work has been partially funded by the French government and by Conseil Général de l'Isère as part of the Multival project (pôle de compétitivité Minalogic).


Antonio Mandarino

Karl Joulain

Melisa Domínguez Gómez

Bruno Bellomo

Thermal transistor effect in quantum systems

We study a quantum system composed of three interacting qubits, each coupled to a different thermal reservoir. We show how to engineer it in order to build a quantum device that is analogous to an electronic bipolar transistor. We outline how the interaction among the qubits plays a crucial role for the appearance of the effect, also linking it to the characteristics of system-bath interactions that govern the decoherence and dissipation mechanism of the system. By comparing with previous proposals, the model considered here extends the regime of parameters where the transistor effect shows up and its robustness with respect to small variations of the coupling parameters. Moreover, our model appears to be more realistic and directly connected in terms of potential implementations to feasible setups in the domain of quantum spin chains and molecular nanomagnets.

I. INTRODUCTION

The exploitation of classical thermodynamics has conducted to the technological revolution that shaped our world since the Nineteenth century [START_REF] Carnot | Reflexions sur la Puissance Motrice du Feu[END_REF]. In recent years the exploration of the thermodynamics of quantum systems has given birth to quantum thermodynamics: a high impact research field either on the fundamental level and the applicative one [START_REF] Gemma | Quantum Thermodynamics[END_REF]. In analogy to classical models, quantum heat engines have been proposed and realized [START_REF] Quan | [END_REF][4][5]. In particular, the properties of non-equilibrium open quantum systems has been employed to study how to obtain many-body entanglement [6] or efficient flux management [7]. Moreover, the implementation of nonequilibrium quantum heat machines has been discussed in solid state set-ups [8] or in more complex scenarios [9].

The ability to manipulate quantum resources is a demanding but fruitful task that has to be pursued in order to build novel devices. A potential high impact apparatus will be the one aiming at the control of thermal energy transport in quantum systems, and at the amplification of heat fluxes among the different parts constituting a composite system. A promising approach in the aforementioned task is to pursue the flourishing path followed in electronics after the realization of rectifiers and transistors with semi-conducting materials [10] that paved the way to build logic gates and to the information and computational technology [START_REF] Millman | Microelectronics[END_REF].

Typically, thermal and electric currents phenomena are empirically well described by the Fourier's and Ohm's laws, respectively. In fact, the functional dependence upon the two respective control variables, temperature and voltage, is of the same type. Recently, evidences of the emergence of the Fourier's law has been pointed out also in the quantum realm [START_REF] Michel | [END_REF]13].

The proposal of such thermal analogues of the electronic rectifier and transistor is based on the assumption that in a thermal set-up the role played by batteries could be played by thermostats. This analogy allowed to come forward with various proposals of mesoscopic thermal de-vices such as rectifiers and diodes [14,15] and transistors [16], the latter operating either in near field [17] or in far field [18] regime of thermal radiation, and also thermal logic gates [19,20].

The theoretical efforts are bolstered by the experimental ingenuity involving a wide range of experimental platforms ranging from carbon and boron nitride nanotube structures [21] and bulk oxide materials [22] to semiconductors quantum dots [23], magnonic systems [24] and phase changing materials, such as vanadium dioxide VO 2 [25,26], and ceramics materials that below a critical temperature behave like high temperature superconductors and above it as dielectrics [27,28].

In the same time, the quest of atomic-scale devices for quantum computational purposes is increasingly pushing the necessity to control and manipulate single or few atoms systems. In particular, the isolation and coherent manipulation of single spins, that are one of the best candidates for a non-optical implementation of a single qubit, is achieved using optical traps and electrical techniques [29]. Recently, several novel quantum technology devices have been proposed, including isolators based on photonic transitions [30], rectifiers [31,32], transistors in an electromagnetic controlled environment [33,34], and also phonon-thermoelectric transistors [35].

Moreover, quantum systems suffer of an unavoidable coupling to their environment, typically modeled as a thermal reservoir of much bigger dimensions of those of the system [START_REF] Breuer | The Theory of Open Quantum Systems[END_REF][START_REF] Schaller | Open Quantum Systems Far from Equilibrium[END_REF]. Despite some detrimental phenomena related to decoherence and dissipation, control and engineering of interacting quantum systems coupled with different thermal baths have led to several studies pointing out how to build the smallest thermal refrigerator [START_REF] Linden | [END_REF]39], how to rectify a thermal current at the very quantum level [40][41][42] and recently the building blocks of a quantum thermal transistor have been discussed considering an integrable spin-chain model [43] and in a qubitqutrit system [44] .

In this paper we analyze the ability to design a quantum thermal transistor employing a spin ring that can, in principle, be implemented on a molecular nanomagnet [START_REF] Bartolomè | Molecular Magnets: Physics and Applications[END_REF]. In comparison to a previous model [43], we consider a more complex scenario where the collective quantum behavior of few spins is expected to play a crucial role in the functioning of the device.

The paper is structured as follows. In Section II, we examine the spin-ring model outlining the frameworks where the theoretical model finds a direct implementability. This section is also devoted to the quantum dissipative process that allows the system to exchange heat fluxes. In Section III, we discuss how the proposed systems can be adopted to build a quantum thermal transistor and some limits of their applicability. Having in mind a direct experimental implementation, in Section IV the robustness of the transistor effect against unavoidable fluctuations and perturbations is addressed. Section V concludes the paper with some final remarks and prospects. Some details can be found in the Appendix.

II. THE SPIN-RING MODEL

Quantum critical spin chains have longly been considered as one of the best substrates to test and implement the future quantum computing and the novel quantum devices. Their main characteristic is to show wide versatility [START_REF] Amico | [END_REF]. In fact, considering the most general model for quantum magnetism, described by the Heisenberg Hamiltonian, one can explore a great variety of universality class by an appropriate tuning of the interaction strengths. Moreover, recent modern developments allow to realize spin chains of few atoms having net spin s = 1/2, opening the road to the exploitation of the physics of some well known models, viz., Ising, XY and XXZ ones [47][48][49][50][51].

In parallel, molecular nanomagnets [START_REF] Bartolomè | Molecular Magnets: Physics and Applications[END_REF] are also attracting more interest as a feasible platform for quantum technological purposes [52]. Specifically, molecular nanomagnets, composed by N = 3 main units, have been proved to be useful for quantum thermometry [53] and for coherent-manipulation of three-qubit states [54].

Spin chains and nanomagnets are theoretically well described by the same effective Hamiltonian upon fixing the configuration geometry. Here, we consider a system of three two-level systems (qubits) of frequency ω p (p = L, M, R), embedded in a magnetic field, and we introduce the vector of the effective spin operators of any qubit Ŝp = (σ x p , σ y p , σ z p ) T and the 3-by-3 matrix λ governing the coupling between spins along different polarization axis, where σ i p (i = x, y, z) is the i-th Pauli matrix of the p-th qubit. A realistic description of a triangular spin chain with a qubit in each vertex labeled L, M and R, as depicted in Fig. 1, is given by the following Hamiltonian (hereafter the reduced Plank constant and the Boltzmann constant are set equal to one, = k B = 1):

H S = 1 2 p=L,M,R ω p σ z p + p =q ŜT p λ Ŝq . ( 1
)
T M T L T R
FIG. 1: (Color online) Schematic picture of a system composed by three qubits interacting each one with any other according to the model in Eq. ( 2). Each of them is dissipating into a different thermal environment as described in Eq. ( 3).

The first term is the sum of single particle free Hamiltonians of three qubits immersed in a magnetic field pointing along the direction of the z-axis and it is responsible of the non-zero field splitting of each qubit, while the second term is the intra-chain spin-spin exchange coupling. Such an Hamiltonian takes into account symmetric and antisymmetric exchange interactions. A proper tuning of λ can give a situation where only the former type of interactions occurs, like in the standard Heisenberg Hamiltonian, or can introduce a coupling between nonhomologous components of the spin operators, as in the Dzyaloshinskii-Moriya interaction [55,56]. We omit here the overcomplexity introduced by an antisymmetric exchange, hence we assume that the tensor λ contains only symmetric terms.

This allows us to consider spins interacting among them through an Heisenberg type Hamiltonian. Therefore, specifying their couplings η pq with p, q = L, M, R and p = q, and the strengths along different polarization axis λ i , the Hamiltonian of the system reads:

H S = 1 2 p=L,M,R ω p σ z p + 1 2 p =q η pq i=x,y,z λ i σ i p σ i q , (2)
where we have chosen equal λ i for the three qubits. This Hamiltonian describes the simplest non-trivial example of spin ring whose properties can be observed with good approximation in a {Cu 3 }-Type nanomagnet, a complex having an almost equilateral triangular shape with a Cu 2+ ion of spin-1/2 at each vertex [57].

A. Comparison between two Ising-type rings

Joulain et al. in their seminal paper [43] have addressed how a thermal transistor can be realized with a quantum system of three interacting qubits, coupled to a thermal reservoir each, and showed how it is analogous to an electronic bipolar one. Their discussion is based on a peculiar choice of a very simple model, that implies a lot of strong assumptions on the underlying physics.

Let us refer to the model adopted in [43] as the z-axis. In fact, there the magnetic field applied on the three qubits is longitudinal to the direction of the spin-spin interactions. Being more specific, the exchange interaction in H S of Eq. ( 2) is non-zero only along the same direction of the magnetic field, i.e. only λ z = 0. Among the other assumptions, this is the one that, in our opinion, requires now a detailed discussion. In fact, this premise, along with some other minor approximations, has the advantage to let the model and the dissipative dynamics be solvable with analytical techniques, since the operators σ z p σ z q commute with the free Hamiltonian. Essentially, the only effect of the zero field splitting terms σ z p σ z q is to modify the eigenenergies of the system, but the collective eigenfunctions remain the same and can be still expressed as a tensor product of single-particle eigenstates. We note that this kind of spin ring, even if considered in a quantum context, is a semi-classical model. In fact, the spin-1/2 operators σ z p can be alternatively viewed as a classical magnetic moment pointing only along two opposite directions. The z-axis Ising model, hence, takes correctly into account a quantization of the magnetic moment, but it does not consider quantum fluctuations due to other spatial components of the same spin operator Ŝp and any possible critical behavior is disregarded.

It is worth noting that in order to propose a truly quantum model a more complex interaction should be taken into account. The reason why we discuss the class of Hamiltonians defined in Eq. ( 2), where, in general, the sum of the single particle contributions does not commute with the interaction term is twofold: (i) from a purely theoretical point of view, these systems may exhibit strongly correlated and nonlocal eigenstates, opening the door to phenomena with an enhancement due to quantum correlations or criticality [START_REF] Amico | [END_REF]; (ii) from an experimentally inspired perspective, nowadays, the control of nanomagnets, spin chains or even quantum dot molecules, has been well established for quantum critical systems [49][50][51].

For the aforementioned reasons our aim is then to propose a well established quantum setting, richer than the one considered in [43], where the thermal transistor effect displays and to study its robustness with respect to the operating temperature and against spurious fluctuations of the exchange interactions.

In particular, we will mainly focus on the case of magnetic systems that belong to the universality class of the quantum critical Ising model in a transverse field and we will refer shorthand to it as the x-axis Ising model. It can be realized considering in Eq. ( 2) that the coupling among the qubits acts only along a direction (that we name x) transverse to the applied magnetic field, i.e. only λ x = 0. We remark that once the coupling with the environment is added (see next sub-section), the different directions transverse to the applied magnetic field are not equivalent anymore. We address in Section IV the presence of perturbations on both the x and z configurations.

The x-axis Ising model introduced as the exemplary model to study quantum phase transitions in magnetic systems and their critical behaviors has been employed in a wide range of protocols to characterize and fulfill quantum computational tasks [START_REF] Amico | [END_REF]. The main feature of such a model resides in the fact that its collective states are no longer a tensor product of the single particles states, but are non-separable. Its pivotal role for the comprehension of magnetism at the quantum scale has fostered the research of a model magnet where its properties can be experimentally measured with different techniques. Nowadays, the most germane realization has been achieved in the low-energy magnetic excitation of the insulator LiHoF 4 [49] or with crystals of the ferromagnetic CoNb 2 O 6 where the spin resides on the Co 2+ ion [50]. A detailed presentation of the spectrum of the x-axis Ising model for the purposes of this paper is shown in Appendix , while a complete discussion of the spectrum of z-axis one can be found in [43].

B. Dissipative dynamics

Each qubit composing the spin ring described above suffers of an unavoidable coupling with its surrounding environment, that is modeled as a thermal bosonic reservoir. The temperatures of the three reservoirs are, in general, different, giving rise to an out of thermal equilibrium scenario where the temperatures are meant to be tunable at will. The total Hamiltonian is then H = H S +H B +H I , where the bath and the system-bath Hamiltonians, respectively, read:

H B = p=L,M,R k ω k a p † k a p k H I = p=L,M,R σ x p ⊗ k g p k a p † k + a p k , (3)
where a p k and a p † k are the bosonic operators of bath p and g p k are the coupling strengths. A schematic representation of the global system is sketched in Fig. 1. As spin ring Hamiltonian H S , we consider the one of Eq. ( 2).

The dynamics of the 3-qubit system is dissipative and, under the Born-Markov and secular approximations [START_REF] Breuer | The Theory of Open Quantum Systems[END_REF], the evolution of the density matrix is described by a master equation of the following form:

ρ = -i[H S + H LS , ρ] + 3 p=1 L p [ρ], (4)
where

H LS = p, ω s p (ω)A † p (ω)A p (ω) is the Lamb shift Hamiltonian, A p (ω) = ω= i-j | j \ / j |σ x p | i \ / i |, | i with i = 1, .
.., 8 are the dressed states of the Hamiltonian H S , as described in the Appendix , and the Lindblad operators are given by [START_REF] Breuer | The Theory of Open Quantum Systems[END_REF] L

p [ρ] = ω γ(ω) A p (ω)ρA † p (ω) - 1 2 {ρ, A † p (ω)A p (ω)} , (5)
where γ p (ω) = J p (ω)[1 + n p (ω)] for ω > 0 and γ p (ω) = J p (|ω|)n p (|ω|) for ω < 0. The average number of excitations and the spectral density of the p-th reservoir are respectively n p (ω) = [exp ω Tp -1] -1 and J p (ω). In all the numerical computations, we will choose Ohmic reservoirs characterized by a linear spectral density J p (ω) = κ p ω (at least in the range of working frequencies), using values of κ p different for the three baths in order to suitably engineer the effect of the environments on the three qubits. It follows that γ p (0) = lim ω→0 + J p (ω)n p (ω) = κ p T p . In the Appendix , a scheme of the transitions induced by the three thermal baths is also reported.

We remark that as we will consider a strong coupling between the three qubits (comparable or higher than the bare frequencies ω p ), we need the above microscopic approach to derive the Lindblad operators responsible of the non-unitary evolution of the density matrix, avoiding any extra simplification that can be somehow justified when the spin-spin interaction is much smaller than the bare frequencies of the qubits [START_REF] Breuer | The Theory of Open Quantum Systems[END_REF]40]. In this limit, we cannot consider phenomenological master equations where the operators A(ω) are built starting from the eigenstates of the bare system Hamiltonian. For the z-axis Ising model, these coincide with the dressed eigenstates, while for the x-type this is not the case.

We also note that since H LS commutes with H S , it only leads to a renormalization of the unperturbed energy levels of H S induced by the coupling with the reservoirs and that the steady state is independent on it.

The three temperatures of the environment will be in general chosen to be different, leading to out of thermal equilibrium steady states, which are not expected to be three-qubit thermal states. At the same time, we expect that each qubit will not thermalize (its own reduced state) to the temperature of its own reservoir because of the collective nature of the quantum dynamics.

III. QUANTUM THERMAL TRANSISTOR

The particular operating principle of an electronic transistor makes possible to regulate the currents at two of its terminals, that could take also very high values, regulating a much smaller current injected through a third terminal. This peculiarity made the transistor particularly suitable to build logic gates commonly used in nowadays electronic. We propose here a thermal analogue of this device able to amplify some of the heat currents circulating in a system as in Fig. 1. The control parameter that will play the role of the gate potential in an electronic transistor is the temperature T M of the reservoir coupled to the middle qubit of frequency ω M .

A. Heat currents in a thermal transistor A straightforward way to take into account the heat flow in and out a quantum system [58], is to link the variation of its mean energy H s to the sum of the heat currents J p exchanged between the quantum system and each bath (no power comes from other external sources in our model):

p J p = ∂ H S ∂t . (6)
By substituting Eq. ( 4) in the previous expression, one can compute the current J p that each thermostat exchanges with the system as

J p = Tr (L p [ρ]H S ) . (7)
We note that at the steady state ρ ss , it holds ρss = 0, so that the total energy is conserved in time. This implies that p J p = 0. A minor remark concerns the fact that the Lamb shift term appearing in Eq. ( 4) does not contribute neither to the final expression of J p neither to the steady state, so that the steady currents are independent on it. In the following, we always address steady configurations and we use J p to indicate steady currents. Following the geometry of the configuration of Fig. 1, we will refer to left, middle and right currents (J L , J M and J R ) to those exchanged, collectively, between the spin ring and, respectively, the left, the middle and the right thermostat. From now on, we assume that the hot reservoir, providing the energy to the system, is the left one, whereas the cold one, that adsorbs the heat flux, is the one placed to the right, and finally the bath in the middle acts as a control. Borrowing the familiar terminology of the bipolar transistor, the right qubit is playing the role of the emitter, while the left one of the collector and the middle one is indeed the analogue of the base.

The thermal transistor effect happens when a small change in the the control temperature T M produce a significant variation of the two lateral currents in contrast with a tiny variation of J M . To study the occurrence of this effect we define the differential thermal resistances

χ s = ∂J s ∂T M -1 Ts=const , s = L, R, (8)
and, as in the spirit of the electronic transistor [10], we introduce a dynamical amplification factor α s , function of the control temperature T M , defined as

α s = ∂J s ∂J M = - χ s χ L + χ R . (9)
The adimensional parameters in Eq. ( 9) are the figures of merit used to have a quantitative benchmark of the presence of the thermal transistor effect and they satisfy the relation α L + α R = -1. In particular, for regions where |α s | 1 one can infer that we are in presence of a strong amplification of the lateral currents in comparison to that controlled by the heat bath in central position. Therefore, it is evident that to amplify the thermal currents one of the two differential thermal resistances should be negative. We underline that this condition was already discussed in the context of non-linear lattices [16], three-terminal graphene devices [59] and band structured engineered silicene superlattices [60].

B. Thermal transistor in an x-axis Ising model

As said in Sec. II A the main case we want to discuss is when the three qubits are described by an x-axis Ising model. In particular, we choose open boundary condition, i.e. η LR = 0.

In Fig. 2 we show the behavior of each current. In order to deal with adimensional quantities we plot the currents J p in units of κ∆ 2 , where κ = κ L is the parameter characterizing the strength of the dissipation of the left qubit and ∆ = ω L , ω L being assumed as the reference frequency. The currents are function of the temperature T M , given in units of ∆. We observe that once expressed also κ M and κ R in units of κ, the steady state of Eq. ( 4) is invariant with respect to κ, while the currents are just proportional to it. Its value must just be small enough to guarantee the validity of the approximations used to derive the master equation of Eq. ( 4). In the following, all the values of temperatures are given in units of ∆, while for currents they are in units of κ ∆ 2 . It is possible to appreciate in Fig. 2 how the thermal transistor effect manifests itself and how the amplification of J L and J R is continuously achieved.

We stress here the crucial role played by the non- equilibrium steady state. In fact, the presence of three environments at different temperatures plugged to distant sites of a magnetic system is the responsible of the three heat flows circulating into it. In particular, it is not surprising observing that even at T M = 0 each of the currents has a non zero value.

In order to better describe the emergence of the thermal transistor effect, the amplification factors α s are plotted in Fig. 3, where it is possible to see how the two lateral currents are amplified. Notably, around T M 0.600, the amplification factor diverges, due to a local minimum of J M -2.90 × 10 -3 . To this extent, we can circumscribe the best working region of this quantum thermal transistor to an interval of the control quantity centered around this value. However, a plateau is present where the amplification factors have values still significantly high. In particular, at T M 4.17, where J M = 0, α L 18.3. As a commentary, we notice that for this value of T M , the reservoir M does not need to inject or absorb energy to maintain the system in the steady state, or in other words we can say that the central reservoir is in a situation of dynamical thermal equilibrium between the hot and the cold heat baths.

We also remark that it is easy to see that the right qubit is the one showing χ R < 0. We have thus shown how a purely quantum scenario can be used to implement a negative differential resistance device. Other choices of the values of the parameters entering either in H S and in the dissipator of Eq. ( 4) give a behavior of the currents and of the amplifications analogous to the ones in Figs. 2 and3. This has been observed in the case of asymmetric configurations.

C. Thermal transistor in a z-axis Ising model

In order to better assess the value of the model here proposed, we compare it with the model previously stud- 7) exchanged by the environments with the system as a function of the control parameter TM , when the system is described by a z-axis Ising model. The solid red line refers to JL, the dashed green line to JM and the blue dotted one to JR. The parameters have the same values of Fig. 2. In the inset, a zoom including the working region of this setting.

ied in [43]. There, the thermal transistor effect had been observed in a range of temperatures much narrower than in our case. We put ourself in the same zone of parameters identified in Fig. 2 and we look if it is possible to extend the working region to larger zones of temperatures as in the x-axis case. In Fig. 4, we show that in the case of the z-axis Ising model the thermal transistor effect works only in a narrow interval of the control temperature, namely T M ∈ [0, 0.2]. When moving to higher values of temperature, the effect completely vanishes, no matter how large the thermal gradient between the hot and cold heat baths is. In fact, in our analysis we have also increased the difference T R -T L in comparison to what has been shown in [43] and observed that the current amplification is always achieved in the same narrow working region.

Recently, the appearance of current amplification has been discussed in a model based on a qubit-qutrit system. Also in this case, the thermal transistor works in a narrow interval of the control temperature in comparison to the x-type Ising model analyzed in Sec. III B, [44].

D. Local behavior

Here, we discuss the possibility to interpret the results of Fig. 2 on the basis of considerations involving only the local behavior of the qubits composing the spin ring. Firstly, we can have access to some local features introducing the reduced density matrix of any qubit, ρ p = Tr q,r =p (ρ ss ), where ρ ss is the global steady state. We indicate with ρ 1 p and ρ 0 p , respectively, the populations of the excited and ground state of the p-th qubit. Each ρ p is a mixed state in the local energy basis and such that we can define a local temperature for each qubit (ρ 0 p ≥ ρ 1 p ), with respect to their free Hamiltonianan, as:

T loc p = ω p ln(ρ 0 p /ρ 1 p ) . ( 10
)
We plot in Fig. 5 the local temperatures of the qubits as a function of the control temperature T M . It is clear that by increasing T M , the temperature gradient between the L and M qubits decreases, in contrast to what happens between the pair of qubits M and R. In addition, the external qubits are never in thermal equilibrium with their respective environments, only the middle one reaches the equilibrium with the control thermostat M at T M 4.17. For this value it holds J M = 0 and J L = -J R 0.179. This means that all the heat injected by the hot reservoir into the system is transferred directly to the cold bath without any participation of the control bath.

Once analyzed the behavior of the local temperatures, we examine if we can qualitatively reproduce the behavior of the heat currents with the following local model. The three qubits are in contact with their local thermostats exactly as in our model, but the qubits do not interact between themselves. Instead, each qubit is also strongly coupled to another local thermal environment whose temperature is equal to (for any value of T M ) the temperature T loc p (T M ) depicted in Fig. 5. The steady state of each qubit can be made close at will to the thermal state of temperature T loc p (T M ) by suitably tuning the coupling between qubits and their own two local reservoirs. In this local model, the reduced state of each qubit is thus equal to the one obtained in our model, while the way each qubit dissipates is strongly different. In the local model the dissipation is governed by local Lindblad operators while in our model by collective ones, computed using the dressed states of H S .

In Fig. 6 we compare the local currents with the exact ones of Fig. 2. We notice that in some cases, local currents well approximate the exact ones, like J L , while in

◆ ◆ ◆ ◆ ◆ ◆ ◆ ◆ ◆ ◆ ◆ ◆ ◆ ◆ ◆ ◆ ◆ ◆ ◆ ◆ ◆ ◆ ◆ ◆ ◆ ◆ 3 6 9 T M 0.1 0.2 J L (a) 3 6 9 T M -4 -2 2 4 J M x10 -3 (b) 3 6 9 T M -1.5 -1 -0.5 J R (c)
FIG. 6: (Color online) Comparison between the exact currents computed for the x-axis Ising model (red lines), the same ones of Fig. 2, and the currents obtained with the local model (dotted blue lines).

other they do not, like J R . This is a clear indication of the relevant role played by the collective behavior of the spin ring when it exchanges heat with the local thermostats. The local temperatures induced by the collective dynamics are thus, in general, not enough by themselves to catch all the physics of this collective exchange and of the occurrence of the thermal transistor effect. In particular, we stress the absence of a local minimum for J M , around which we observed the best performance of the device.

IV. ROBUSTNESS AGAINST PERTURBATIONS

The results reported in the previous sections show how to build a quantum thermal transistor operating on a wide range of temperatures and starting from a microscopic derivation, with a potential implementation over some feasible physical settings. However, in any real physical implementation of an Ising Hamiltonian, spurious and undesired couplings pointing along different directions of the desired axis for the interaction could occur. This could entail a lost of the thermal transistor effect. Obviously, in any controlled setup, those interactions can be considered as small fluctuations and treated by means of perturbative corrections to the system Hamiltonian H S . Nevertheless, in order to pursue our microscopical description of the effect and be precise, we use the full model for the three qubits as in Eq. (2), introducing time by time more complex interactions and studying to which extent they alter the amplification performances.

In order to substantiate the process illustrated so far, we consider a physical implementation where the real axis of the interaction term of the model can differ from the expected one (indicated with k in the following) [49], and we compute the amplification factors, α s (λ i , λ j ), that are now functions of the couplings, λ i and λ j , along the other two possible polarization directions i and j, and they may assume a different value from the unperturbed one. Only the coupling between the qubits L and M and between the qubits R and M are perturbed, while the coupling between the qubits L and R is maintained equal to zero as before.

To obtain a statistical detailed analysis we assume that the values of the perturbations are normally distributed and we evaluate the averaged amplification factors α i,j s = dλ i dλ j α s (λ i , λ j )N (λ i,j , Σ i,j ), [START_REF] Millman | Microelectronics[END_REF] where s = L, R, and N (λ i,j , Σ i,j ) is the bivariate Gaussian distribution of the perturbations. It is centered around their mean values λ i,j = (λ i , λ j ), with covariance matrix given by Σ i,j = diag(Σ i , Σ j ). In particular, we choose that the spurious interactions can deviate of around 10% from their mean value, i.e. Σ i = 0.1λ i .

As a tool to investigate the effect of small perturbations, we define the ratio

ζ i,j = α i,j L α unp L , (12)
where α unp L represents the value of the left amplification factor obtained in the absence of perturbation. If only one additional coupling of the type σ i p σ i q perturbs the main interaction term σ k p σ k q , the above ratio is indicated with ζ i . For the sake of clarity, we point out that another quantity analogue to ζ i,j can be in principle defined using the amplification factor of the right current α R . Nevertheless, its value depends on α L in a simple way, such that for any T M this choice would lead to analogues dampings of ζ i,j as function of the strength of the perturbation, λ i,j .

In Fig. 7 we show the quantity ζ as a function of the average strength of 3 types of typical perturbations that can occur in both settings discussed in Section III. Since α unp L can diverge for a certain value of the control temperature T M , we fix it equal to T M = 0.650, close enough the one where the divergence appears in order to have α unp L 1 but where it is still finite, being α unp L 1.42 × 10 3 . We stress here that the value of T M in the presence of perturbations is kept the same of the unperturbed case. The quantity ζ is close to unity when the system still operates as a quantum transistor close to its unperturbed value α unp L but it vanishes as soon as the perpendicular couplings become more intense.

As it is apparent from the plot, the x-axis and z-axis Ising models show a completely opposite behavior in the presence of perturbations. Indeed, despite the fact that both the models have been perturbed around a quite optimal configuration, the x-axis model still shows the thermal transistor effect for extra couplings small enough. In contrast, the possibility to achieve a current amplification with the z-axis Ising model is completely lost in the presence of infinitesimal couplings among the spin in any direction perpendicular to the wanted interaction axis. Our numerical evidences only allow us to see that ζ is extremely low for values of the extra couplings larger than ten millionths of the one along the z-axis, but we cannot surmise how the unperturbed value is restored for smaller values of the spurious coupling λ i,j .

We also provide a qualitative mathematical explanation of this phenomenon which resides on the structure of the couplings between the qubits. In fact, as pointed out when discussing the two possible configurations, a coupling commuting with the bare Hamiltonian affects only the eigenfrequencies of the systems and it leaves unchanged the eigenstates entering in the definition of the operators A(ω), that are essential to derive the dissipative dynamics of Eq. ( 4). Adding a perpendicular coupling, not commuting with the bare part of H S completely alters their structure and it imposes to consider the dressed-state basis to write the A(ω), that typically differs from the bare-state basis one.

V. CONCLUSIONS

In this paper, we have addressed the design and the possible physical implementation of a quantum thermal transistor. This novel device acts on thermal currents as a bipolar electronic transistor does with electric currents, providing an amplification of the collector's and emitter's currents by a proper tuning of the gate potential, while the corresponding gate current is order of magnitude lower than the other two and practically constant.

Our model proposes a system of three qubits strongly interacting among them and each of them in contact with a different thermal reservoir. This setting imposes nonequilibrium dissipative dynamics that entail the presence of non-vanishing steady state currents flowing into the system via bath induced transitions. We have focused our attentions on a particular system that can lead to a feasible realization on several experimental platforms, such as molecular nanomagnets and few-body spin chains, and we have referred to this model as the spin-ring model.

In particular, we have devoted our efforts to describe how a quantum thermal transistor works in a scenario where a more complex spin-spin coupling is present, in comparison to a previous model recently presented in [43]. Throughout the paper, we have referred to these two models as the x-type Ising model and the z-type Ising model. The former is characterized by an interaction Hamiltonian not commuting with the bare one, or in other words the magnetic field acting on the three spins is perpendicular to the direction along which the spins interact; the latter, instead, is a model where magnetic fields and interaction are longitudinal, so that the two contributions of the system Hamiltonian commute.

Choosing as control parameter the temperature of the heat bath directly coupled to the middle qubit, we have shown that the x-type spin ring operates as a thermal transistor over a wider range of temperatures in comparison to the z-type one. The significant amplification of the lateral currents has been justified in the context of devices characterized by negative differential thermal resistance [16,59,60] and by means of the collective dynamics. In fact, considering a naive local model for the system, that partially takes into account collective phenomena, cannot explain the whole behavior exhibited by our model. Finally, we have discussed the robustness of both the possible implementations against spurious and uncontrollable couplings stemming from the magnetic interaction between the different pairs of the effective spins of the magnetic ring. The results of exact numerical computations suggest that, for reasonably small perturbations, the x-type molecule can be steered acting on the control temperature to behave still as a thermal transistor around its unperturbed configuration. In contrast, our computations show that the z-type molecule is really fragile in presence of those kinds of perturbations.

As final remarks, we would like to point out that even if we have performed a microscopic derivation of master equation describing the dynamics of the system, overriding any phenomenological simplification, a deeper comprehension of the very quantum effects conducting to such current amplification is still lacking. It could be matter of future investigation the role of system criticality and of the dissipation mechanism and how they contribute and compete in order to state a general scheme to build a quantum thermal transistor. where the 16 real coefficients a i , b i , c i , d i with i = 1, 2, 3, 4 in the above expressions are functions of the parameters entering in the Hamiltonian. In all the numerical trials, we have found the same above structure for the eigenvectors, all the coefficients being real.

It is worth noting that the above states have well-defined parity and that the states with opposite energy have different parity. In fact, it is easy to check it by measuring the parity operator P = σ z L ⊗ σ z M ⊗ σ z R on any term appearing in | i .

Finally, we report in Table I the transitions mediated by any thermal reservoir. It is worth noting that we write here only the transitions that can be interpreted as the emission of a photon in the usual context of quantum optics, since they involve states with a positive energy difference between the initial and the final value.

TABLE I:

The possible transitions of positive frequency mediated by any of the three thermal baths by means of the interaction operator σ x p for the case of Sec. III B. The first column gives the initial states, starting from the one with highest energy, whilst the other columns specify the qubit operator coupled to the corresponding thermal reservoir as prescribed by Eq. ( 3), and the final states connected to the initial ones.

σ x L σ x M σ x R | 1 | 2 , | 3 , | 5 | 2 ,

2 JFIG. 2 :

 22 FIG.2:(Color online) The three thermal currents defined in Eq. (7) (in units of κ ∆ 2 ) exchanged by the environments with the system as a function of the control parameter TM (in units of ∆), when the system is described by an x-axis Ising model. The solid red line refers to JL, the dashed green line to JM and the blue dotted one to JR. The parameters are ωL = ∆, ωM = 0.1 ∆, ωR = 0.2 ∆, ηLM = ηMR = ∆, ηLR = 0, κL = κM = κ, κR = 100 κ, TL = 10 ∆ and TR = 0.01 ∆. In the following figures, currents and temperatures are always meant, respectively, in units of κ ∆ 2 and ∆.

2 JM x10 - 3 FIG. 3 :

 233 FIG. 3: (Color online) The amplification factors defined in Eq. (9) as a function of the control parameter TM . The solid red line refers to αL and the blue dotted one to αR. In the inset, a zoom of JM including its local minimum responsible of the divergence of the amplification factors. The parameters have the same values of Fig. 2.

1 JMFIG. 4 :

 14 FIG.4: (Color online) The three thermal currents defined in Eq. (7) exchanged by the environments with the system as a function of the control parameter TM , when the system is described by a z-axis Ising model. The solid red line refers to JL, the dashed green line to JM and the blue dotted one to JR. The parameters have the same values of Fig.2. In the inset, a zoom including the working region of this setting.

FIG. 5 :

 5 FIG. 5: (Color online) Local temperatures of the three qubits as defined in Eq. (10), as a function of the control parameter TM . Plots (a), (b) and (c) refer, respectively, to the local temperature of the left, middle and right qubit. The parameters have the same values of Fig. 2.

FIG. 7 :

 7 FIG. 7: (Color online)The ratio ζ defined in Eq. (12) for the x-type Ising model, as a function of the mean value of the spurious couplings λ i,j . The dashed green line refers to ζ z , the blue dotted one to ζ y and the red solid line takes into account perturbations with both λ y and λ z = 0 but with the same mean value, namely ζ y,z . In the inset, the ratio ζ for the z-type Ising model. Here, the dashed green line refers to ζ x , coinciding with ζ y (red diamonds). The blue dotted one refers to ζ x,y and is obtained imposing λ y and λ z = 0 with the same mean value. The parameters of the unperturbed configuration are the same as in Fig.2.

| 1 =

 1 -a 1 |111 -a 2 |100 -a 3 |010 -a 4 |001 | 8 = +a 1 |000 -a 2 |011 + a 3 |101 -a 4 |110 | 2 = +b 1 |000 + b 2 |011 + b 3 |101 + b 4 |110 | 7 = +b 1 |111 -b 2 |100 + b 3 |010 -b 4 |001 | 3 = +c 1 |000 -c 2 |011 -c 3 |101 + c 4 |110 | 6 = -c 1 |111 -c 2 |100 + c 3 |010 + c 4 |001 | 4 = +d 1 |111 -d 2 |100 -d 3 |010 + d 4 |001 | 5 = -d 1 |000 -d 2 |011 + d 3 |101 + d 4 |110 , (A.2)

  | 3 , | 5 , | 8 | 2 , | 3 , | 5 | 2 | 4 , | 6 | 4 , | 6 , | 7 | 4 , | 6 | 3 | 4 , | 7 | 4 , | 6 , | 7 | 4 , | 7

	| 4	| 8	| 5 , | 8	| 8
	| 5	| 6 , | 7	| 6 , | 7	| 6 , | 7
	| 6	| 8	| 8	| 8
	| 7	| 8	| 8	| 8

Acknowledgments A.M. acknowledges the "Région Bourgogne-Franche-Comté" for financial support throughout the mobility grant N. 2017Y-06400. B.B. acknowledges the support by the French "Investissements d'Avenir" program, project ISITE-BFC (contract ANR-15-IDEX-03). A.M. thanks Heinz-Peter Breuer for useful comments and Elena Servida for discussions about semiconductor electronics. B.B. thanks Benedetto Militello and David Viennot for helpful comments.

Appendix: Spectrum of the system Hamiltonian in the x-type Ising model.

In this appendix we give a sketch of the diagonalization of the system Hamiltonian introduced in Eq. ( 2) and used to obtain the thermal transistor effect discussed throughout the paper. In particular, we focus on the case of the x-type Ising model with the left and right qubits not interacting, i.e. η LR = 0. The matrix of a system composed by three qubits with different splitting in a magnetic field with a transverse Ising interaction reads:

where we have assumed η qp = η pq and for shorthand we have introduced Ω pq = ω p + ω q and Λ x pq = η pq λ x with p, q = L, M, R.

The secular equation of Eq. (A.1) can be reduced to a quartic equation, leading to four pairs of energy eigenvalues equal in modulus. We can, therefore, decompose H S in the base where it is diagonal,

where we have ordered the energy eigenvalues using the following notation 8 ≤ 7 ≤ ... ≤ 1 and 9-i =i , ∀i.

Introducing the computational basis, defined as the tensor product |l L l M l R , of all the dispositions of the eigenvectors of the three σ z p , i.e. σ z p |l p = (-1) (lp+1) |l p , with l p = 0, 1 and p = L, M, R, the eigenvectors of H S , found for the main case discussed in the paper (Sec. III B), are: