Yasushi Umezawa
email: yasushi.umezawa@us.fujitsu.com

Takeshi Shimizu
email: takeshi.shimizu@us.fujitsu.com

A Formal Verification Methodology for Checking Data Integrity

Formal verification techniques have been playing an important role in pre-silicon validation processes. One of the most important points considered in performing formal verification is to define good verification scopes; we should define clearly what to be verified formally upon designs under tests. We considered the following three practical requirements when we defined the scope of formal verification. They are (a) hard to verify (b) small to handle, and (c) easy to understand.

Our novel approach is to break down generic properties for system into stereotype properties in block level and to define requirements for Verifiable RTL.

Consequently, each designer instead of verification experts can describe properties of the design easily, and formal model checking can be applied systematically and thoroughly to all the leaf modules.

During the development of a component chip for server platforms, we focused on RAS (Reliability, Availability, and Serviceability) features and described more than 2000 properties in PSL. As a result of the formal verification, we found several critical logic bugs in a short time with limited resources, and successfully verified all of them. This paper presents a study of the functional verification methodology.

Introduction

Logic verification has become more important but difficult to complete with increasing size and complexity of system on chip (SoC) designs. Powerful formal verification methods have been playing an important role in pre-silicon validation processes. On the other hand, it is still not realistic to verify all the functions of a SoC designs by formal verification methods because it requires lots of effort to describe design properties strictly in formal language. Even if such models are successfully developed, model checking for complex designs may be beyond the power of available tools and computing resource, resulting in fail. Therefore, hybrid verification methodologies using both formal verification and logic simulation have been discussed and proposed [START_REF] Mcmillan | Fitting Formal Methods into the Design Cycle[END_REF][2] [START_REF] Dill | What's Between Simulation and Formal Verification[END_REF][4] [START_REF] Ho | Smart Simulation Using Collaborative Formal and Simulation Engines[END_REF][6] [START_REF] Maher Mneimneh | Scalable Hybrid Verification of Complex Microprocessors[END_REF] [START_REF] Chen | Utilizing Formal Assertions for System Design of Network Processors[END_REF].

One of the most important and difficult points considered in hybrid verification methodology is to define a good verification scope of formal verification; i.e. what to be verified with formal verification techniques and what to be left for conventional validation with logic simulation. Needless to say, the goal of the project is to verify the design and minimize the verification effort, but not to apply formal verification methodology. Thus, the following three practical requirements should be considered when the formal verification criteria are defined.

• Properties defined in the formal verification scope are hard to validate thoroughly in conventional logic simulation. If such properties are solved formally, it significantly increases the validation coverage. • The problem size of the properties is suitable for available formal verification tools. Description of the properties in formal language should be simple, and it should not take much time in model checking, so that we could insist superiority and efficiency against conventional logic simulation methods. • The purpose and the methodology of formal verification should be well documented and shared by the design and verification team. It is important to deploy the formal verification systematically in the design flow.

In a development project of a component chip for server platforms, we considered to apply formal verification techniques from the viewpoint described above. The component chip has strong requirements for RAS features and they should be verified thoroughly before tape out.

In the following sections, the requirements and the overview of the target design are mentioned. In section three, design properties that are derived from the requirements are described in detail. In section four the design flow for verification is shown. Section five contains the result and analysis of the formal verification activity. Section six is our conclusions.

Target Design Overview

We have been developing a component chip for servers. Table 1 shows the overview of the chip implementation.

The chip requires so-called 'main-frame class' reliability so that it supports enhanced RAS features to detect soft errors in the chip and permanent failures of a component. All the internal data paths, registers, state machines, and counters are protected by parity bits. When a parity error is detected, the error must be logged and reported according to the severity of the error. The requirements in implementation level are summarized as follows.

• Parity protection in data paths.

• Parity protection in key control structures, such as FSM and counters. • Illegal state detection for FSM and counters.

As a result of initial investigation, we found more than 1300 checkpoints for data integrity derived from the chip specification. It is not realistic to verify this huge number of checkpoints exhaustively and efficiently by logic simulation, simply because it will consume too much time. This is the initial motivation for us to set the scope of formal verification as data integrity checking. The advantages are summarized as the following. First, the description of the properties for integrity check is easy and simple because the properties are broken down into module level. Thus, each designer can easily describe the properties, and model checking can be applied locally at each leaf module, as described in the later section. Second, the properties are data-centric and exhaustive search is needed. Formal model checking is right to use for the purpose. Also, it is possible to model the property in a simple and comprehensive description.

For the above two reasons, we could expect significant increase in productivity with formal model checking.

Properties in Leaf Module Level

We reached the following three properties for data integrity verification in leaf module level after breaking down the system level properties in the previous section.

Note that we used user-written properties, and automatic assertion extraction was not performed.

• Ability of error detection.

• Soundness of internal states.

• Output data integrity.

Figure 1 shows abstraction of each module. In the following sections, each property above is explained based on the abstraction. The state A in the figure is for internal FSM and protected by odd parity. EC/ED can inject errors arbitrary into the state A. The state B is for data path and protected by odd parity.

Three properties should be described and verified against all non-structured modules or leaf modules. A leaf module should be small enough for formal verification tools so that Divide-and-Conquer approach is the key to success for verification goals. A leaf module can be excluded if it has no internal state and no data paths with parity protection. Other important properties can be verified with formal verification as well, but that is not mandatory criteria.

Note that we picked up Property Specification Language (PSL) [START_REF][END_REF] for property description because it is in widespread use as an industry standard and supported by several formal verification tools.

Ability of Error Detection

The first property is for error detection. The design property is to check if all the illegal values are detected and reported at each integrity check point. Figure 2 shows a PSL code for this property, referring to the typical leaf module in Figure 1 • Check1: HE (Hardware Error Report) is true in the next cycle when EC/ED is driven and the injected value through ED is illegal. EC should be defined for each FSM and counter, but ED can be shared between FSM and counters. • Check2: HE is true in the next cycle when I is illegal.

This property means that Check1 and Check2 in Figure 1 should fire when an error is injected.

Soundness of Internal States

The second property is for soundness of internal states. The design property is to check if the integrity of internal states holds as long as the integrity of primary inputs holds.

• HE should not be asserted when no error is injected and integrity of I holds.

This property means that Check1 and Check2 in Figure 1 should not fire in normal operation. Figure 3 shows a PSL code for the property. Two properties (pIntegrityI and pNoErrInjection) are assumed, and one property (pNoError) is verified.

Output Data Integrity

The third property is for output data integrity. The design property is to check if the integrity of primary outputs holds as long as the integrity of primary inputs holds.

• The integrity of O should hold when no error is injected and integrity of I holds.

This property means that primary output O in Figure 1 should not have parity error in normal operation. Figure 4 shows a PSL code for the property. Two properties (pIntegrityI and pNoErrInjection) are assumed, and one property (pIntegrityO) is verified.

Design Flow for Verification

This section describes the design flow of formal verification we adopted. Figure 5 shows the overall design flow at the front-end side. The logic designers are in charge of releasing Verifiable RTL, which is explained in section 4.1, test scenarios for functional verification, and properties or specification of data integrity. A dedicated engineer was assigned for formal verification. The verification engineer creates PSL codes based on the specification of data integrity, performs model check, and makes feedback the results to the logic designers. RTL can be Verifiable by adding one line of code per such entity. The error injection ports should be tied to zero in the upper layer module because it is not used in real silicon. Figure 6 shows an example of such Verifiable RTL code in verilog.

The second task of logic designers for formal verification is to release the specification of data integrity. It can be either in text format or described as PSL codes.

Tasks of Verification Engineer

Three tasks are assigned for formal verification engineer.

First task is to develop PSL codes if the integrity specification is written in text format. For portability of the codes, we tried not to use tool dependent features in the process.

The second task is to perform model checking and debugging. We also consider the size of the properties in this process. When a property turned out beyond the power of available tools, for example time out happens during execution; the property can be divided for making small corns. Figure 7 shows an example of how to divide a property. The original property in Figure 7 (1) is for the output data integrity of Data D; i.e., the integrity of Data D should hold as long as the integrity of Data A, Data B, and Data C holds. The property is manually divided as shown in Figure 7 (2). The followings are the details of the divided properties. The last task is to feedback the results of property checking to logic designers for bug fix and verifiability.

Results

We used a commercial formal verification tool and an in-house formal verification engine. The commercial formal verification tool is capable of handling PSL properties and verilog RTL codes, equipped with various formal solver algorithms.

The in-house formal verification engine is a powerful solver for properties with UMC (unbounded model checking) based on POBDDs (Partitioned reduced Ordered Binary Decision Diagrams) and its related algorithms as well as combined forward and backward traversal for OBDD-based invariant checking. [START_REF] Jain | Breaking Barriers of BDD-based Verification by Partitioning[END_REF]

Verified Properties

We described 2047 PSL properties in total and all properties were verified successfully as shown in Table 2. The table shows the module names, the number of submodules, the number of logic bugs found by formal verification, and the number of PSL properties for each target category. Note that the number of properties in Table 2 is only for assertions. It takes about 20 hours to verify all the properties on a typical Linux workstation with single CPU and single license.

The break down of the properties in number is as follows; 1306 properties are for checking ability of error detection, 200 properties are for checking soundness of internal states, 520 properties are for checking output data integrity, and 21 properties are for checking other features. We found 7 logic bugs in formal verification. This is about 5% of total logic bugs. The following sections describe the detail of each logic bug, the design impact, and the side effect of the error injection implementation.

Logic Bugs Found by Formal Verification

This section describes the detail of each logic bug. We found 7 logic bugs in formal verification. Table 3 shows the type of property and difficulty of finding the logic bugs by logic simulation.

After the detail analysis of results, B1, B3, B5 and B6 were turned out to be difficult to detect by logic simulation. The details are shown below.

B1)

When a non-zero-value is written into a reserved field of a register, the internal parity of the register is not maintained correctly. Consequently, it causes an internal parity error. It is very difficult to find this type of logic bug by logic simulation because the scenario to hit this condition is very complicated.

B3)

Although a signal comes from a macro is not guaranteed immediately after release of reset, the logic assumes a certain value with the signal. Therefore, a false parity error is logged and reported. The logic bug was not found by logic simulation because the behavior model of the macro cell was wrong. Actually, this is a problem of logic simulation environment, so it is impossible to find it by logic simulation.

B5, B6)

An address decoder has ninety-one valid cases when decoding 8-bit address spaces. Parity calculation in the data path is wrong specifically for two cases out of ninety-one cases. The parity error is not always detected because it depends on the data pattern, so it is very difficult to detect it by logic simulation since it needs exhaustive data pattern.

In summary, at least four of seven logic bugs are difficult to detect by logic simulation, whereas they can be easily found by formal verification.

Design Impact and Side Effect

This section describes the design impact and the side effect of the error injection implementation. Since the logic for the error injection remains in the netlist as shown in Figure 1, we checked the design impact in terms of area increase and timing delay using several modules. Basically, the design impact is caused by a selector added shown in Figure 1.

Table 4 shows the area increase caused by implementing the error injection feature, and the area increase is less than 2%. Note that module name in Table 4 corresponds to Table 2. The timing delay of the selector is about 200 ps that are about 4 % of total delay when frequency is 250MHz. This timing delay was acceptable for the target chip and caused no timing closure issue.

In summary, the penalty caused by implementing the error injection feature is almost negligible in terms of area increase and timing delay.

One unexpected and good side effect is that those remaining gates can be used as spare logic gates. We performed ECO (post-route fixes) six times and we used these remaining gates twice.

Conclusions

We have applied formal verification method when we developed the component chip for servers with rich RAS feature. There are three reasons why we adopted formal verification.

• The target chip requires main-frame class reliability so that there are huge check points for data integrity.

It is difficult to verify the data-centric properties exhaustively and effectively by conventional logic simulation. • The description of the properties for integrity check is easy and simple because the properties are broken down into module level. • The methodology above is clear for logic designers to release Verifiable RTL Four logic designers and one verification engineer have developed more than 2000 PSL properties. Since the properties are written for leaf modules, it was easy to develop properties rather than logic simulation patterns.

As a result, we found seven logic bugs. Four of seven logic bugs were difficult to detect by logic simulation. Thus, it is shown that formal verification is powerful and effective.

We also investigated the design impact of implementing the error injection feature, and we found that the penalty was almost negligible in terms of area increase and timing delay.

What was novel in our approach was to break down properties for RAS features into three stereotype properties. Such framework enabled us to deploy formal methodology systematically and thoroughly over all the leaf modules. Each designer designed Verifiable RTL and described properties quite easily, although it was a very difficult task to complete verification for huge number of integrity checkpoints. As the result of our methodology, we conclude that significant increase of productivity is achieved.

Figure 1 .

 1 Figure 1. Typical leaf module

  . In the PSL code, Check1 I: Primary Inputs O: Primary Outputs EC: Error Injection Control ED: Error Injection Data HE: Path and Check2 are corresponding to pCheck1 and pCheck2 respectively. Here we have two data integrity check points.

Figure 2 .

 2 Figure 2. PSL code for checking ability of error detection

Figure 3 .

 3 Figure 3. PSL code for checking soundness of internal states

Figure 4 .

 4 Figure 4. PSL code for checking output data integrity

Figure 5 .

 5 Figure 5. Design flow

-

  the integrity of Data A' should hold as long as the integrity of Data A holds the integrity of Data B' should hold as long as the integrity of Data B holds the integrity of Data C' should hold as long as the integrity of Data C holds the integrity of Data D should hold as long as the integrity of Data A', Data B' and Data C' holds

Figure 6 .Figure 7 .

 67 Figure 6. An example of Verifiable RTL code

Table 1 . Chip implementation

 1

	Item	Implementation
	Chip die size	12.8 x 12.5 mm 2
	Technology	0.11 um CMOS ASIC
	Logic size	3.5M gates
	Core frequency	250MHz

Table 2 . Number of verified properties

 2

	Module	# of	# of		Type of Property
	Name	Sub	Bug	P0	P1	P2	P3	Total
	A	19	3	204	23	113	15	355
	B	2	0	25	23	82	0	130
	C	13	1	43	20	38	0	101
	D	3	1	70	46	137	6	259
	E	58	2	964	88	150	0 1202
	Total	95	7	1306	200	520	21 2047
	P0: Ability of Error Detection
	P1: Soundness of Internal States
	P2: Output Data Integrity
	P3: Other Properties

Table 3 . Classification of logic bugs

 3

	Defect ID	Type of Property	Can be found by logic simulation easily?
	B0	Soundness of Internal States	Yes
	B1	Soundness of Internal States	No
	B2	Soundness of Internal States	Yes
	B3	Ability of Error Detection	No
	B4	Output Data Integrity	Yes
	B5	Output Data Integrity	No
	B6	Output Data Integrity	No

Table 4 . Area increase caused by implementing the error injection feature

 4

	Module Name	Area Increase
	A	1.4 %
	B	0.4 %
	D	0.2 %

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

Proceedings of the Design, Automation and Test in Europe Conference and Exhibition (DATE'05)

Acknowledgement

We thank Takashi Miyoshi, Yoichi Koyanagi, Akihiko Okutsu, and Takuya Saze for their contribution of developing properties. We also thank Jawahar Jain and Christian Stangier for their support of using the in-house formal verification engine.

Tasks of Logic Designers

First of all, the logic designers need to release the Verifiable RTL code. The Verifiable RTL code should satisfy the following requirements.

• Simple error injection method against every integrity check point is well-defined through primary input ports. • Error injection should be controlled independently per entity for integrity checking.


Ali Habibi
email: habibi@ece.concordia.ca

Iqbal Asif

Otmane Ahmed
email: aahmed@ece.concordia.ca

Mohamed Ait
email: ait@ece.concordia.ca

Sofiène Tahar
email: tahar@ece.concordia.ca

On the Design and Verification Methodology of the Look-Aside Interface

In this paper, we present a technique to design and verify the Look-Aside (LA-1) Interface standard used in network processors. Our design flow includes several refinements starting from an informal UML specification until getting to an RTL modeled in Verilog. We integrate the verification of the LA-Interface in the design flow by considering two intermediate levels: (1) Abstract State Machines (ASM); and (2) SystemC. The first one serves the verification by model checking of a set of PSL properties, while the second includes a set of assertions to be verified by simulation. To evaluate the performance of our approach, we used the Rule-Base model checker to verify the same properties; and the OVL library to verify the same assertions.

Introduction

New IPv6 systems and carriers increasingly demanding detailed lookups on packets and flows, the interface between network processors and other components, such as external co-processors and memory devices, is taking the spot light in the networking sector. Currently, the Look-Aside 1 (LA-1) interface [START_REF]Look-Aside (LA-1) Interface, Implementation Agreement[END_REF] is the defacto standard for linking these components [START_REF] Bhugra | La-1b: Moving the look-aside interface forward[END_REF]. It is being the key to several networking-specific applications, including packet forwarding, packet classification, admission control, and security.

Designing LA-1 directly at the RTL level is possible, however, it is time and effort consuming and certainly an error-prone process. In this paper, we propose an approach to design and verify the LA-1 interface in a hierarchical flow using an object-oriented (OO) methodology and several refinements levels. We aim to design an IP (Intellectual Property) module that can be used as a Look-Aside Interface or as a validation unit for LA-1 compatible devices. For this reason, we propose to use a top-down design and verification approach.

In our model, UML presents the top level to capture a precise specification of the design and its properties. Then, comes Abstract State Machines (ASM) [START_REF]AsmL for Microsoft .NET Framework[END_REF], a high level language providing a variety of features that allow the description of the relevant state of a system in a high level of abstraction, to represent a formal and precise model of the design. At this level, we introduce the first step of the verification process which is model checking.

The properties of the under verification model are in PSL (Property Specification Language) [START_REF]Accellera Property Specification Language reference manual[END_REF], a standard language for properties specification. PSL language supports specifying a large class of real design properties that range from simple to complex ones in a hierarchical yet very well organized structure consisting of four layers: Boolean, temporal, verification and modeling layers.

Once the model verified at the ASM level we translate it to SystemC [START_REF]Open SystemC Initiative[END_REF], a relatively new system level language for embedded system design and verification. The PSL properties modeled in ASM are also translated to C# and combined to the SystemC model in order to perform assertion based verification using simulation. Finally, we derive the synthesizable RTL implementation in Verilog from the SystemC design.

In order to prove the correctness of the refinement process, with respect to the verified properties, we re-verify the same PSL properties for the RTL Verilog code using the RuleBase [START_REF]RuleBase Formal Verification Tool (Version 1.5)[END_REF] model checker. For instance, such a proof will set that both the high level model in ASM and the low RTL level satisfy the same set of properties. In addition to that, comparing our model checking methodology to RuleBase represents a good evaluation of the integration of the verification at the early design stages (ASM level for our case). We also used the Open Verification Library (OVL) to verify the same assertions as those integrated in the SystemC model in order to compare the simulation performance of Sys-temC against the Verilog/OVL based approach.

As related work to ours, we cite the approach proposed by Kanna et al. [START_REF] Shimizu | Monitor-based formal specification of PCI[END_REF] to implement a PCI bus as a Verilog monitor and to verify its properties using SMV [START_REF] Mcmillan | Symbolic Model Checking[END_REF]. In [START_REF] Shimizu | Monitor-based formal specification of PCI[END_REF], the bus was implemented in Verilog with all the properties embedded as part of the code. This makes its modification or upgrade a very complex task. Besides, the Verilog model they verified includes only 2 agents (one master and one slave), which considers a relatively small design in comparison to LA-Interface with four banks.

The rest of this paper is organized as follows: Section II introduces the SystemC, PSL and ASM. Section III presents the LA-1 Interface. Section IV describes the proposed LA-1 Design Methodology. Section V details the verification approach. Section VI contains the experimental results. Finally, Section VII concludes the paper.

SystemC, PSL and ASM

SystemC

SystemC is a set of C++ class definitions and a methodology for using these classes [START_REF] Osi | SystemC 2.0.1 language reference manual[END_REF]. SystemC introduces channels, interfaces, and events to enable communication and synchronization between modules or processes. The core language consists of an event-driven simulator as the base. It works with events and processes. The other core language consists of modules and ports for representing structures. Interfaces and channels are used to describe communications. The primitive channels are built-in channels such as signals, semaphores and FIFOs. SystemC provides data types for hardware modeling and certain types of software programming as well.

PSL

PSL is an implementation independent language to define properties. It does not replace, but complements existing verification methodologies like VHDL and Verilog test benches. The syntax of PSL is very declarative and structural which leads to sustainable verification environments. PSL consists of four layers based on the functionality of interest [START_REF]Accellera Property Specification Language reference manual[END_REF]:

The modeling layer is used to model behavior of design inputs for formal verification tools, and to model auxiliary parts of the design that are needed for verification. The verification layer is used to tell the verification tool what to do with the properties described by the temporal layer. The temporal layer is used to describe properties of the design, as well as simple general properties. This layer can describe properties that involve complex temporal relations. Temporal expressions are evaluated over a series of evaluation cycles. The Boolean layer is used to build expressions for the other layers, specifically the temporal layer. Boolean expressions are evaluated in a single evaluation cycle.

PSL is a hierarchical language, where every layer is built on top of the layer below. This approach allows the expressing of complex properties from simple primitives. A property (also called assertion) is built from three types of building blocks: Boolean expressions, sequences, which are themselves built from Boolean expressions, and finally subordinate properties. Sequences, referred to as SEREs (Sequential Extended Regular Expressions), are used to describe a single-or multi-cycle behavior built from Boolean expressions.

ASM

An ASM model by definition encodes only those aspects of the system's structure that affect the behavior being modeled. ASM provides a variety of features that allow the description of the relevant state of a system in a very economical, high-level way. Each abstract state machine represents a particular view of the distinct operational steps that occur in the real system being modeled. AsmL [START_REF]AsmL for Microsoft .NET Framework[END_REF] is a language used to model systems in ASM. It is not, however, restricted to ASM but offers a rich programming language. It is integrated with Microsoft's software development environment including Visual Studio, MS Word, and Component Object Model (COM), where it can be compiled and connected to C# or to the .NET framework [START_REF]AsmL for Microsoft .NET Framework[END_REF].

Look-Aside Interface

The LA-1 standard is the look-aside interface to networkprocessing elements (NPEs). It targets look-up-tables and memory-based coprocessors and emphasizes as much as possible on the use of the existing technology. It is based on QDR and Sigma RAM technologies. Although modeled on an SRAM interface, the LA-1 specification aims to accommodate other devices as well, such as classifiers and encryption co-processors.

The LA-1 interface major features include:

• Concurrent read and write operation

• Unidirectional read and write interfaces

• Single address bus

• 18 pin DDR data output path transfers 32 + 4 bits of even byte parity per read. • 18 pin DDR data input path transfers 32 + 4 bits of even byte parity per write • Byte write control for writes The LA-1 interface requires a master-clock pair. The master clocks (K and K#) are ideally 180 degrees out of phase with each other, and they are outputs for the host device and inputs for the slave device. A write cycle is initiated by asserting WRITE SEL (W#) low at rising edge of K (K clock). The address of the Write cycle is provided at the following edge of K (K# clock which 180 degrees out phase from clock K). A read cycle is initiated by asserting READ SEL (R#) low at rising edge of K (K clock) and the read address is presented on the same rising edge.

LA-1 Design

Our approach is shown in Figure 2, where we start with an informal specification for the intended design developed in UML. This step provides a better view of the design components and their interactions. Based on the UML model (class diagram, sequence diagram, etc.), we develop an ASM model, which will enable the verification of the design using formal tools (model checkers for our case). When the verification terminates with an error, we update UML specification and re-capture them to ASM. Finally, when the verification passes without errors, we map the verified ASM model to a SystemC implementation. This latter is then refined and verified using assertion based verifications (ABV). Finally, we map the SystemC model to a low level syntehsizable HDL implementation (Verilog for our case).

UML Level

Use

Simulation performance Comparison

ABV results

ABV results

Figure 2. Look-Aside Interface Design and Verification Methodology.

We combined both the verification and design processes in the same path. We applied model checking at higher level of abstraction (ASM) to avoid state explosion problems. On the other hand, we used RuleBase at the lowest level (HDL) for comparison purpose against using ASM. ABV is applied to both SystemC and Verilog models in order to: (1) compare the simulation performances of the SystemC simulator against the commercial verilog simulators; and (2) to evaluate our ABV technique in comparison to the OVL/Verilog methodology [START_REF] Tahar | Open Verification Library[END_REF].

UML LA-1 Specification

We designed the LA-Interface considering a structure based on four principle classes: Write Port, Reading Port, SRAM Memory and a Light Simulator (optional classes include properties).

Such an architecture guarantees that the final design can be used in two different ways:

• A stand-alone IP: to integrate larger SoC.

• A Verification Unit: to validate other LA-1 Interface compatible devices.

In addition to the classes involved in the design, we embedded a light semantics of a light synchronous Verilog like simulator. As first impression we may consider that such an addition module in the system presents an overhead to the ASM model; nevertheless, its size is relatively small compared to the complete ASM design. Besides, such a module offers a higher level of programming and instantiation flexibility. For example, it allows to upgrade the design from 1 bank to 4 banks (actually, for any number N of banks) by just a matter of object instantiation. Basically, this is one of the main objectives to use a purely object-oriented approach to design the LA-1 Interface at the ASM level. On the other hand, in order to verify precise clocked properties at earlier stages of the design, it is mandatory to embed certain semantics of the simulation cycles.

In order to enable a better representation of the properties at the UML level, we propose to use a modified sequence diagram where new notation are included to enable specifying information principally to the methods activation clocks, execution cycles and duration of execution. An illustration of the modified sequence diagram, for the read mode scenario, is displayed in Figure 3. Such a diagram says that a read scenario starts by putting a read request at the clock K which causes the ReadPort to request the data from the SRAM in the next cycle at the same clock K. After formatting the data, the ReadPort releases it in two consecutive steps at the next rising edges of K and K#.

Network Processor SRAM_Memory ReadPort OnReadRequest[0]()@K LA-1-SRAM-OnReadRequest[1]()@K FormatData[1]() OnReadRequest[2]()@K OnReadRequest[2]()@K#

ASM Model

The ASM model includes both the design and the properties. All the design classes are mapped from the UML model. However, a number of updates is required to guarantee a correct generation by the AsmL tool of the model's FSM. For instance, the firstly explored action by the reachability analysis algorithm embedded in the tool must initialize all the model's objects. An execution with non-initialized objects may results to an exception or a misbehavior of the exploration algorithm. We also need to add at the entry of every method a pre-condition defining the rules filtering the states where the method can be executed. This is one of the most critical issues in defining the ASM model because a wrong definition of the pre-condition may totally change the behavior of the system and consequently modify the verification results. The pre-condition rules define also a way of communication between the embedded light simulator and the other modules. Actually, one of the basic rules relates the method to the clocks.

Figure 4 illustrates the ASM semantics of the light Verilog simulator. It includes in particular an initialization function that is executed after pre-condition "all the all the system modules have been initialized" (condition: SystemFlag = STARTED). The same method includes a second pre-condition setting that the method is only executed at the initialization phase (condition: SimStatus = INIT). This illustrates how the pre-condition constructor is used to manage the exploration algorithm performing the reachability analysis. The LA-1 Interface properties are extracted from both the sequence diagrams and the class diagram. Once mapped to ASM classes, assertions need to be instantiated correctly. Actually, some properties are referring to certain objects (Bank 2 for e.g.) which requires a particular instantiation of certain modules. Besides, some methods may require additional variables to enable recording certain system's variables. For example, in a read scenario, the assertion needs to record the number of clock cycles since the initial request has been issued.

In this work, we used the PSL to specify the design's properties. Actually, in addition to the fact that PSL is the standard for properties specification, our choice was guided by our previous work where we defined a deep embedding of PSL in ASM. PSL properties were implemented in a hierarchical way: (1) with all the components defined as objects; and (2) every PSL layer extends its lower layer using the inheritance feature of AsmL. This OO embedding of PSL promotes re-using the verification classes in other designs.

SystemC

The SystemC design is directly obtained from the ASM model using a syntax transformation. For instance basic types (including Boolean, integer, byte, etc.) are one-to-one mapped between C++ and AsmL with exactly the same operations and semantics. Every class from the ASM model is translated to SystemC module. The pre-conditions in the ASM methods are included in the SystemC Constructor section as triggering conditions for the Sys-temC methods.

The object instantiation in the ASM model is translated to a naming mapping in the SystemC design and is integrated in the design's main procedure sc main. We will discuss in Section 5 a technique to make sure both the ASM and systemC models behaves exactly the same way for the same inputs.

Verilog

A synthesizable Verilog implementation is derived from the SystemC design. For the case of the LA-1 Interface, we map each class to a Verilog module. The transformation is straight thanks to the basic types used in the LA-1 SystemC design (which only includes enumerated types, Boolean and integer). Multiple banks model is obtained from the single one by instantiating the Read, Write and Memory modules. The connection between the control signals is performed using tristate buffers.

Verification Approach

Using AsmL for Model Checking

The AsmL tool is not a model checker for PSL properties. However, it includes a general algorithm implementing reachability analysis (also called state space exploration [START_REF]AsmL for Microsoft .NET Framework[END_REF]). The AsmL tool generates the model's FSM by executing the model program in a special execution environment, keeping track of the actions it performs and recording the states it visits. This process is called exploration. Usually a model program implies so many states and transitions that it is not feasible to include them all in the FSM, so you must limit the number of states and transitions that the tool explores. The FSM that the tool builds is usually only a portion -an under-approximation -of the huge FSM that would result if the model program could be explored completely. As a result, the test suite generated from the FSM usually does not cover all possible states and transitions of the model program.

By adapting the exploration algorithm we've been able to implement a model checking procedure for PSL properties. For instance, we encode a PSL property (modelled in ASM) as two state variables Pstatus and P value meaning respectively that the property is under verification or already verified and giving the current value of the property. In other terms, a property is: (1) correct if Pstatus = true and P value = true; (2) incorrect if Pstatus = true and P value = false; and (3) having an undefined value if Pstatus = status (this is the case when a temporal property over several cycles is being verified in an intermediate state).

Verifying PSL properties by covering for all the system state space is not always feasible due to state explosion problem. Defining a smart configuration to guide the state exploration is a very important step towards enabling model checking using AsmL. For instance, defining the domains, which are defined as finite collections of values from which method arguments are taken, are the most important issues to consider. For instance, for an integer input that can only take a value in the range from 5 to 23, considering all possible integer values for the type AsmL.Integer is a waste of time; besides, this may get the verification to output wrong results.

In order to provide counter-examples when the verification fails we define for every property a filter stopping condition defined by the conjunction: "Pstatus = true & P value = false". The generated portion of the state machine from the initial state until getting to the stop error point forms a complete path for a counter-example, an information very useful in order to debug and correct the design's errors.

In order to guarantee that the translated SystemC model is conform to the original ASM model we perform a conformity check using AsmL. In fact, AsmL tool performs a conformance test by executing the program under test, called the implementation (SystemC model for our case), together with the model program in ASM. The tool executes the exploration algorithm in the same time on both the ASM model and a binary executable generated from the SystemC design. It then verifies if for all the possible inputs, both models behave the same. For instance, this is phase is sometimes time consuming, however, it is quite important to make sure the ASM to SystemC mapping preserves the system's properties.

Using RuleBase For Model checking

RuleBase is one of the first model checkers supporting PSL (actually it supports even its ancestor Sugar). We find it quite complicated to verify PSL properties using this model checker due to the important effort that we spent defining the environment and writing the behavioral model including all the design levels of hierarchy. We used the same properties that we verified at the ASM level with PSL. The main objective is to compare the efficiency of performing model checking at earlier stages of the design flow.

ABV using SystemC and C#

As it was shown in Figure 2, we propose to integrate PSL assertion to SystemC designs as external monitors implemented in C#. These latter are directly compiled from the PSL properties modeled in ASM. They are then integrated with the SystemC model. The integration requires, in particular, updating the SystemC design to interface to the assertion monitor. For instance, the signals (variables) that are used in the assertion must be seen as external signals in the model so that they can be input to the assertion monitor. So, the list of variables involved in the assertion is required in order to make them visible to the assertion monitor. This transformation does not affect the behavior of the code as it will only be accessed in a read-only mode.

Once the code is updated and the assertion is generated, an instance of the assertion is bound to the existing SystemC design modules. The assertion monitor, acting as part of the design, can do the following: (1) stop the simulation when the assertion is fired; (2) write a report about the assertion status and all its variables; and (3) send a warning signal to other modules (if required). We note that the internal code of the assertion is C# so the designer can update it or do any other functionalities that can be coded in C#.

ABV using OVL

The Accellera Open Verification Library (OVL) provides designers, integrators and verification engineers with a single, vendor-independent interface for design verification using simulation, semi-formal and formal verification techniques [START_REF] Tahar | Open Verification Library[END_REF]. Assertion monitors are instances of modules whose purpose is to verify that certain conditions hold true. An assertion monitor is composed of an event, a message, and a severity. Event is a property that is being verified by a monitor. An event can be classified as a temporal or static property. A static property is a property that must be valid at all times, whereas a temporal property is a property that is valid only during certain times. Message is the string that will be displayed in case of an assertion failure. Severity represents whether the error captured by the monitor is a major or a minor problem.

Using OVL assertions is promoting for small size HDL designs. Nevertheless, when the complexity of the design becomes important, writing OVL itself is not an easy task. Writing the assertion for the reading mode, for example, requires encoding all the atomic operations in separate modules which gets to complex final design in the simulation since every call to an OVL will load the correspondent module as part of the simulated design.

Experimental Results

In following, we describe our results on the verification of the LA-1 Interface using the proposed methodology. The ASM and SystemC experiments were performed on a 2.4 GHz Pentium IV and 512 MB of RAM (PC 2700) while the RuleBase and OVL experiments were performed on 2 X UltraSPARC-III+ machine with 2 900Mhz processors and 4096M of RAM.

Model Checking

Table 1 shows the CPU time required to verify all the interface properties combined together. The number of states and transitions refers to generated FSM. This illustrates the efficiency of our approach to handle model checking of relatively complex case study thanks to raising the abstraction level. We note that the number of nodes and transitions is not the total number present in the global system FSM. It represents the FSM that's generated according the AsmL configuration parameters including the domains, methods, variables and actions.

Table 2 gives a summary of the model checking results using RuleBase for the Read Mode operation. We notice that even though the tool succeeds to verify the property for up to 3 banks the required time is relatively big. So, considering more complex designs is out of the scope of the tool which is confirmed by the raise of the state explosion problem when considering 4 banks. It is not adequate to compare both levels ASM and Verilog considering the gap of abstraction between the two models, however, these results confirm that applying model checking cannot be reused the classical way for low level HDL models but needs to be applied at the early stages of the design's flow.

Simulation

Table 3 compares the average of execution time per cycle for the assertion based verification of SystemC design with assertions in C# and the Verilog design with assertions in OVL. For both cases we considered the same assertions describing the Reading Mode. We notice that the SystemC simulation runs always at least 20 times faster the Verilog design. In other terms, 1 day simulating SystemC is equivalent to more than 20 days simulating Verilog (and OVL) for LA-1 Interface. Besides, we notice that the larger is the system, the faster is the SystemC simulation in comparison to Verilog. This clearly confirms the adequation of using SystemC for the design and also for the verification by simulation of designs at the system level.

Number

Conclusion

In this paper, we presented a design and verification approach using UML, ASM and SystemC to create a Verilog IP for the Look-Aside Interface de-facto standard for interfacing network processors to other components. We first defined the interface's model in UML, then, we translated it to ASM in order to verify, using model checking, a set of PSL properties. After verifying all the PSL properties, we mapped the ASM code to Sys-temC and the PSL properties to C# assertions (modules) in order to enable ABV at the SystemC level. Finally, we implemented the SystemC model in a synthesizable Verilog RTL. By proving the writing and reading modes properties using RuleBase for the RTL implementation, we also proved the correctness of our refinement from ASM to RTL (for one, two and three banks). Besides, experimental results showed some limitations of the tool and hinted that using model checking is more efficient when integrated at the early design phases. We also, inserted the same assertions, used at the SystemC level, to the Verilog implementation using the OVL library. Simulation results displayed a superior performance of SystemC over the OVL based approach. Finally, we believe that the proposed approach improves the design and verification of IP blocks.

As future work, we consider proving the soundness of the complete refinement process from ASM to RTL. This will allow reusing the verification results that can be proved at any level for the other lower levels; thus, reduce the complexity of verifying RTL.

Figure 1 .

 1 Figure 1. Look-Aside Interface (4 Banks) [7].

Figure 3 .

 3 Figure 3. Sequence Diagram for the Reading Mode.

classFigure 4 .

 4 Figure 4. Light Verilog Simulator in ASM

Table 1 . Model Checing Using AsmL.

 1

	Number of	CPU	Number of FSM
	Banks	Time (s)	Nodes Transitions
	1	8.093750	93	106
	2	18.093750	212	185
	3	28.078125	277	318
	4	40.734375	369	424
	Number of	CPU	Memory Number of
	Banks	Time (s) (in MB)	BDDs
	1	675.13	58	812785
	2	2530.75	226	9.2 x 10 7
	3	15264.21	590	52.4 x 10 7
	4	State Explosion

Table 2 . Model Checking Using RuleBase: Read Mode.

 2

Table 3 . Simulation Results

 3

		Average of execution	Ratio =
	of	Time/cycle (δ in s)	δOV L/
	Banks	SystemC (δSC) OVL (δOV L)	δSC
	1	21.22 x 10 -9	0.44 x 10 -6	20.73
	2	26.25 x 10 -9	1.90 x 10 -6	72.38
	3	30.07 x 10 -9	2.91 x 10 -6	96.77
	4	38.73 x 10 -9	3.68 x 10 -6	95.01

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


Alina Eqtami
email: alina.eqtami@l2s.centralesupelec.fr

Antoine Girard
email: antoine.girard@l2s.centralesupelec.fr

Safety control, a quantitative approach

Keywords: Safety, controlled invariant sets, transition systems, abstraction, quantitative synthesis

published or not. The documents may come

Safety control, a quantitative approach

Alina Eqtami, Antoine

INTRODUCTION

In system design, safety refers to the ability of a controller to maintain the state of a system in a specified set of safe states (see e.g. [START_REF] Tabuada | Verification and Control of Hybrid Systems: A Symbolic Approach[END_REF]; [START_REF] Girard | Controller synthesis for safety and reachability via approximate bisimulation[END_REF]). The classical approach to safety synthesis is based on the notion of controlled-invariant sets (see e.g. [START_REF] Blanchini | Set-theoretic methods in control[END_REF]; [START_REF] Maler | Control from computer science[END_REF]; [START_REF] Rungger | Computing robust controlled invariant sets of linear systems[END_REF]), where states are said to be safety-controllable, or infinite-time reachable (as in [START_REF] Bertsekas | Infinite time reachability of state-space regions by using feedback control[END_REF]), if they belong to the maximal controlledinvariant subset of the safe set. This approach is therefore mostly qualitative (states are either safety-controllable or safety-uncontrollable) and does not allow to compare to states within the same category. However, intuitively, some states can be considered as safer than the others (i.e. those that are further from the unsafe set). Similarly, between two unsafe states, the one, which is closer to the safe set, would tend to be more desirable. Hence, it appears natural to take a quantitative approach where a measure of safety is associated to the states of the system. Such quantitative semantics of qualitative specifications, typically formulated in temporal logic have been given in [START_REF] Fainekos | Robustness of temporal logic specifications for continuous-time signals[END_REF]; [START_REF] Donzé | Robust satisfaction of temporal logic over real-valued signals[END_REF]). Intuitively, these semantics measure how much a trajectory can be perturbed before changing the qualitative value (true or false) of a given property. Hence, for safety properties, these quantitative se-This research was partially supported by Labex DigiCosme (project ANR-11-LABEX-0045-DIGICOSME) operated by ANR as part of the program "Investissement d'Avenir" Idex Paris Saclay . This project has received funding from the European Research Council (ERC) under the European Union's Horizon 2020 research and innovation programme (grant agreement No 725144). mantics can be interpreted as follows: for safe trajectories, it measures the minimal distance of the trajectory to the unsafe set; for unsafe trajectories, it measures the maximal distance of the trajectory to the safe set. Quantitative semantics of temporal logic have been used within the model predictive control framework to synthesize receding horizon controllers [START_REF] Raman | Reactive synthesis from signal temporal logic specifications[END_REF]; [START_REF] Sadraddini | Robust temporal logic model predictive control[END_REF]).

In this work, we propose a quantitative approach to safety control, based on a functional fixed-point iteration. Convergence of the fixed-point in finite-time is guaranteed for finite transition systems. The level sets of the fixed-point coincide with the maximal controlled invariant subsets of a family of sets parameterized by their distance to the safe set. This allows us to interpret the value of the fixed-point at a given state as a measure of the safety of that state. Moreover, we show that a common safety controller can be synthesized for the whole family of controlled invariant sets. A similar functional fixed-point iteration can be found in [START_REF] Chatterjee | Value iteration[END_REF]), however, the characterization of the level sets in terms maximal controlled-invariant sets and results on controller synthesis appear to be new. A second contribution of the paper is the joint use of the quantitative approach with abstraction-based techniques (see e.g. [START_REF] Tabuada | Verification and Control of Hybrid Systems: A Symbolic Approach[END_REF]; [START_REF] Girard | Controller synthesis for safety and reachability via approximate bisimulation[END_REF]), which allow us to lift the results from finite transition systems to infinite transition systems with finite abstractions. Let us remark that abstraction-based synthesis of safety controllers with quantitative objectives has also been studied in [START_REF] Meyer | Safety control with performance guarantees of cooperative systems using compositional abstractions[END_REF][START_REF] Meyer | Quantitative implementation strategies for safety controllers[END_REF]). However, in those works, the quantitative objective is an auxiliary performance cost, which is not directly related to the safety property.

The paper is organized as follows. In Section 2, we introduce the class of transition systems and provide a quick overview of the qualitative approach to the safety control problem. In Section 3, we introduce the quantitative approach to safety control for finite transition systems. In Section 4, we extend the approach to infinite transition systems using abstraction-based techniques. Finally, in Section 5, we show the effectiveness of the approach by appyling it to a simple boost DC-DC converter model.

Notation. In the following, R, R + 0 and N denote the set of real, nonnegative real and natural numbers, respectively. A relation

R ⊆ X × Y is identified with the set-valued map R : X → 2 Y where R(x) = {y ∈ Y | (x, y) ∈ R}. The inverse relation of R is R -1 = {(y, x) ∈ Y × X| (x, y) ∈ R}. The domain of R is dom(R) = {x ∈ X| R(x) = / 0}.

PRELIMINARIES

In this section, we introduce some concepts which will be helpful for the rest of the paper. First, the general modeling framework of transition systems is given and then, some concepts related to safety control are going to be discussed.

Transition systems

A common modeling framework for discrete, continuous and hybrid systems are the transition systems (see e.g. [START_REF] Tabuada | Verification and Control of Hybrid Systems: A Symbolic Approach[END_REF]), that are defined as follows: Definition 1. A transition system T is a quintuple T = (X,U, ∆,Y, H) consisting of a set of states X; a set of inputs U; a transition relation ∆ ⊆ X × U × X; a set of observations Y and an output map H : X → Y .

The transition relation captures the dynamics of the transition system and (x, u, x ) ∈ ∆, which will be denoted hereafter as x ∈ ∆(x, u), signifies that the state x can be reached initiating from x under the control input u. The set of enabled inputs at state x is given by enab ∆ (x) = {u ∈ U| ∆(x, u) = / 0}. If enab ∆ (x) = / 0, then x is said to be a blocking state, otherwise it is said to be non-blocking; the set of non-blocking states is denoted nbs ∆ . A transition system is called finite if the state and input sets X and U are finite sets, whereas a transition system that is not finite is called infinite. A transition system is called metric if the output set Y is equipped with a metric d.

In the framework of transition systems, (static state-feedback) controllers can be defined as follows: Definition 2. A controller for the transition system T is a map C : X → 2 U such that C(x) ⊆ enab ∆ (x), for all x ∈ X. The controlled transition system T C is defined as

T C = (X,U, ∆ C ,Y, H)
where the transition relation is given by:

x ∈ ∆ C (x, u) ⇐⇒ [(u ∈ C(x)) ∧ (x ∈ ∆(x, u))].
Note that a state x of the controlled system T C is non-blocking if and only if C(x) = / 0, i.e. nbs ∆ C = dom(C).

Safety specifications

Let us consider a transition system T and X s ⊆ X a set of safe states. In practice, X s can often be defined from a set of safe outputs Y s ⊆ Y by X s = H -1 (Y s ).

The problem considered in this paper, known as safety problem in computer science, is traditionally referred to as controlled invariance in control theory. The main objective in safety problems is to characterize a subset of safe states S ⊆ X s , such that when the system's state is initially in S, it can remain in S (and thus in X s ) forever under suitable control. Additionally, one aims at synthesizing a controller which makes it possible to restrict the behavior of a system so that its state remains inside the set S. The definition of controlled invariant subset and the notion of a safety controller are given next. Definition 3. Let us consider transition system T and X s ⊆ X a set of safe states:

• S ⊆ X s is a controlled invariant subset of X s if and only if for all x ∈ S, there exists u

∈ enab ∆ (x) such that ∆(x, u) ⊆ S. • S ⊆ X s is the maximal controlled invariant subset of X s if
and only if S is a controlled invariant subset of X s and for all controlled invariant subsets S ⊆ X s , we have S ⊆ S .

Notice that the uniqueness of the maximal controlled invariant subset is a well-known result, see e.g. [START_REF] Ramadge | Modular feedback logic for discrete event systems[END_REF]). Algorithms for computing the maximal controlled invariant subset are typically based on fixed-point iteration on sets, see e.g. [START_REF] Bertsekas | Infinite time reachability of state-space regions by using feedback control[END_REF]; [START_REF] Maler | Control from computer science[END_REF]; Rungger and Tabuada ( 2017)). A state x ∈ X is said to be safety-controllable if x ∈ S ; otherwise, it is said to be safety-uncontrollable.

Given a controlled invariant subset S ⊆ X s , a safety controller maintains the state of the system T C inside S: Definition 4. Let us consider transition system T and X s ⊆ X a set of safe states, let S ⊆ X s be a controlled invariant subset of X s . The controller C : X → 2 U is a safety controller for controlled invariant subset S if, S ⊆ dom(C) and for all x ∈ S, for all u ∈ C(x), we have ∆(x, u) ⊆ S.

Given a controlled invariant subset S ⊆ X s , it is always possible to obtain a safety controller C as follows:

C(x) := / 0 if x / ∈ S {u ∈ enab ∆ (x)| ∆(x, u) ⊆ S} if x ∈ S
(1)

QUANTITATIVE APPROACH TO SAFETY CONTROLLER SYNTHESIS

The approach to the safety problem presented in the previous section can be referred to as qualitative, in the sense that the states of T can be partitioned in two categories: the safety controllable states (i.e. x ∈ S ) and the safety uncontrollable states (i.e. x / ∈ S ). However, for states within a given category, the previous approach does not allow to make a distinction. For instance, given two safety controllable states, one may be interested to know if one is safer than the other; a similar question can be asked for safety uncontrollable states. To answer this question, one needs to take a quantitative approach, i.e. one needs to have a measure of the level of safety is a given state. Intuitively, for a safety controllable state, this measure should quantify how far one can stay from the unsafe set, starting from that state. Conversely, for an safety uncontrollable state, this measure should quantify how close one can stay from the safe set.

The quantitative approach would also be useful for the purpose of controller synthesis. Indeed, controllers obtained by (1) through the qualitative approach have non-deterministic values for safety controllable states and have an empty value (i.e. are undefined) for safety uncontrollable states. Instead, one could use the quantitative approach to choose the control input that would optimize the level of safety of the corresponding successors.

In this section, we make the assumption that the transition system T is finite. We believe that similar results can be derived for classes of infinite transition systems, but at the expense of more involved technical developments, so the infinite case is left as future work.

To substantiate the quantitative approach to safety controller synthesis, let us introduce a cost function h : X → R, which intuitively quantifies how safe or unsafe is a given state x. If T is metric, a natural choice for h(x) is the signed distance from the output H(x) to the safe output set Y s , i.e. Then, let us define the sequence (V k ) k∈N , where the maps V k : X → R ∪ {+∞} are given iteratively as follows. For k = 0, and x ∈ X, let V 0 (x) := h(x). Then, for every subsequent step, with k ∈ N and x ∈ X, let

h(x) = d s (H(x),Y s ) (2) with d s (y,Y s ) = sup{δ ≥ 0|B(y, δ ) ∩ S = / 0} if y / ∈ S -sup{δ ≥ 0|B(y, δ ) ⊆ S} if y ∈ S where B(y, δ ) = {y ∈ Y | d(y, y ) ≤ δ } denotes the
V k+1 (x) := (3) max h(x), min u∈enab ∆ (x) max x ∈∆(x,u) V k (x ) if x ∈ nbs ∆ +∞ if x / ∈ nbs ∆
The fixed-point is obtained by taking the limit of the sequence:

V (x) := lim k→+∞ V k (x). (4)
For finite state systems, one can show that the fixed-point is actually reached in a finite number of steps: Proposition 5. Let T be finite, then the limit (4) exists and there exists k ∈ N such that for all k ≥ k , for all x ∈ X,

V k (x) = V k (x) = V (x). Moreover, V satisfies the following fixed-point equation, for all x ∈ nbs ∆ , V (x) = max h(x), min u∈enab ∆ (x) max x ∈∆(x,u) V (x ) . (5)
Proof. First, we are going to prove that for all x ∈ X, the sequence (V k (x)) k∈N is nondecreasing. This is obviously the case if x / ∈ nbs ∆ . When x ∈ nbs ∆ , we have the following

V 0 (x) = h(x) V 1 (x) = max h(x), min u∈enab ∆ (x) max x ∈∆(x,u) V 0 (x ) ≥ V 0 (x) Assume now, that for some k ≥ 1, V k (x) ≥ V k-1 (x) for all x ∈ X.
Then, for all x ∈ nbs ∆ ,

V k+1 (x) = max h(x), min u∈enab ∆ (x) max x ∈∆(x,u) V k (x ) ≥ max h(x), min u∈enab ∆ (x) max x ∈∆(x,u) V k-1 (x ) = V k (x)
Note that for all x / ∈ nbs ∆ , we also have V k+1 (x) ≥ V k (x). Thus, by induction, it follows that for all k ∈ N, for all x ∈ X, we have V k+1 (x) ≥ V k (x), i.e. the sequence (V k (x)) k∈N is nondecreasing. A nondecreasing sequence converges to the supremum of its range. Thus, the limit (4) exists.

To show that the fixed point is reached in a finite number of steps, let us remark that for all x ∈ X, for all k ∈ N, V k (x) ∈ h(X) ∪ {+∞}, which is finite from the finiteness of X. Hence, for all x ∈ X, (V k (x)) k∈N is nondecreasing with values in a finite set, which implies that there exists k x ∈ N, such that for all

k ≥ k x , V k (x) = V k x (x) = V (x). Let k = max x∈X k x , which by finiteness of X is well-defined. Then, for all x ∈ X, for all k ≥ k , V k (x) = V k (x) = V (x)
. Finally, by (3) with k ≥ k , one gets (5). 2 Remark 6. If T was infinite, the previous procedure would need to be amended as follows. The minimum and maximum in (3) should be replaced by infimum and supremum, respectively. While the limit (4) would still exist (V k (x) would remain nondecreasing), the fixed-point would generally not be reached in a finite number of steps.

The relation of the quantitative approach described above to the qualitative approach is highlighted in the following result: Theorem 7. Let T be finite, then for all a ∈ R, S a = {x ∈ X | V (x) ≤ a} is the maximal controlled invariant subset of the set X a = {x ∈ X | h(x) ≤ a}. Let us consider the controller C defined by:

C (x) = / 0 if x / ∈ nbs ∆ arg min u∈enab ∆ (x) max x ∈∆(x,u) V (x ) if x ∈ nbs ∆ (6)
Then, for all a ∈ R, C is a safety controller for controlled invariant subset S a .

Proof. The proof of this Theorem is twofold: (i) firstly we are going to prove that the set S a is a controlled invariant subset of X a , and admitting C as an associated safety controller;

(ii) secondly, we will show that S a is the maximal controlled invariant subset X a .

(i) First, let us remark that dom(C ) = nbs ∆ . Let x ∈ S a , since V (x) ≤ a < +∞, it follows that x ∈ nbs ∆ , thus S a ⊆ dom(C ). By (5), we have h(x) ≤ V (x) ≤ a and x ∈ X a , thus, S a ⊆ X a . Then, let u ∈ C (x), and x ∈ ∆(x, u), then by definition of C one gets:

V (x ) ≤ max z ∈∆(x,u) V (z ) = min v∈enab ∆ (x) max z ∈∆(x,v) V (z ).
It then follows from (5) that min

v∈enab ∆ (x) max z ∈∆(x,u) V (z ) ≤ V (x).
Therefore, V (x ) ≤ V (x) ≤ a and the set S a is a controlled invariant subset of X a and C is an associated safety controller.

(ii) Now, the maximality of S a is going to be established. Let us consider a controlled invariant subset S ⊆ X a . We need to prove that S ⊆ S a . We have that for all x ∈ S, V 0 (x) = h(x) ≤ a.

Assume, now, that for some k ∈ N, for all x ∈ S, V k (x) ≤ a. Let x ∈ S, then there exists u ∈ enab ∆ (x) such that ∆(x, u) ⊆ S.

Hence, for all x ∈ ∆(x, u), V k (x ) ≤ a. This implies that min

u∈enab ∆ (x) max x ∈∆(x,u) V k (x ) ≤ a.
Moreover, since h(x) ≤ a, it follows from (3) that

V k+1 (x) = max h(x), min u∈enab ∆ (x) max x ∈∆(x,u) V k (x ) ≤ a.
By induction, we obtain that for all x ∈ S, for all k ∈ N, V k (x) ≤ a. Taking the limit, we obtain V (x) ≤ a for all x ∈ S and thus S ⊆ S a . 2

The advantages of the quantitative approach over the qualitative approach are clear from Theorem 7. Firstly, the quantitative approach allows us to compute, using a single fixed point iteration, the maximal controlled invariant subsets of a parameterized family of safe sets. To do the same thing, the qualitative approach would require to proceed with one fixed-point iteration for each value of the parameter. Secondly, while the qualitative approach, using (1), would synthesize one different safety controller for each maximal controlled invariant subsets of the parameterized family, the quantitative approach allows us to design a common safety controller C given by ( 6), for the whole family of maximal controlled invariant subsets.

We can see from (6), that C chooses inputs that will minimize the (worst-case) value of V at the next state. It is remarkable that using controller C , the function V acts as a weak Lyapunov function (i.e. it is non-increasing) along the trajectories of the controlled system T C . Then, the value V (x) provides a measure of the level of safety of x, since the value of V and thus of h along trajectories of T C starting from state x remains smaller than or equal to V (x). If x is safety uncontrollable, then V (x) > 0, and the outputs of trajectories starting from x remain at a distance from Y s smaller than or equal to V (x).

If x is safety controllable, then V (x) < 0, and the outputs of trajectories starting from x remain at a distance from the unsafe set Y \Y s greater than or equal to -V (x).

ABSTRACTION-BASED SYNTHESIS USING THE QUANTITATIVE APPROACH

In this section, we show how the quantitative approach can be used in the context of abstraction-based synthesis.

Approximate alternating simulation and bisimulation

Abstraction-based synthesis requires the use of formal behavioral relationships between transition systems. In the following, T 1 denotes a finite abstraction while T 2 denotes the concrete (possibly infinite) system. We consider transition systems formally related by approximate alternating simulation relations [START_REF] Tabuada | Verification and Control of Hybrid Systems: A Symbolic Approach[END_REF]) defined as follows:

Definition 8. Let T i = (X i ,U i , ∆ i ,Y, H i ) with i = 1, 2
, be two metric transition systems with the same set of outputs Y and let

δ ∈ R + 0 . A relation R ⊆ X 1 × X 2
is a δ -approximate alternating simulation relation from T 1 to T 2 if the following are satisfied:

(1) For every x 1 ∈ X 1 there exists

x 2 ∈ X 2 with (x 1 , x 2 ) ∈ R; (2) for every (x 1 , x 2 ) ∈ R we have d(H 1 (x 1 ), H 2 (x 2 )) ≤ δ ;
(3) for every (x 1 , x 2 ) ∈ R and for every u 1 ∈ enab ∆ 1 (x 1 ) there exists u 2 ∈ enab ∆ 2 (x 2 ) such that for every

x 2 ∈ ∆ 2 (x 2 , u 2 ) there exists x 1 ∈ ∆(x 1 , u 1 ) satisfying (x 1 , x 2 ) ∈ R
We say that T 1 is δ -approximately alternatingly simulated by T 2 , denoted by T 1 δ T 2 if there exists a δ -approximate alternating simulation relation from T 1 to T 2 .

Accordingly, we can define the approximate alternating bisimulation relations [START_REF] Tabuada | Verification and Control of Hybrid Systems: A Symbolic Approach[END_REF]) as follows: Definition 9. Let T i = (X i ,U i , ∆ i ,Y, H i ) with i = 1, 2, be two metric transition systems with the same set of outputs Y and let

δ ∈ R + 0 . A relation R ⊆ X 1 × X 2 is
said to be a δ -approximate alternating bisimulation relation between T 1 to T 2 if the following are satisfied:

(1) R is a δ -approximate alternating simulation relation from T 1 to T 2 ; (2) R -1 is a δ -approximate alternating simulation relation from T 2 to T 1 .

We say that T 1 is δ -approximately alternatingly bisimilar to T 2 , denoted by T 1 ∼ δ T 2 , if there exists a δ -approximate alternating bisimulation relation between T 1 and T 2 .

Abstraction-based synthesis

In this section, we show how the use of the quantitative approach on a discrete abstraction makes it possible to obtain a parameterized family of controlled invariant subsets for the concrete system. Theorem 10. Let T i with i = 1, 2, be two metric transition systems with the same set of outputs Y such that T 1 δ T 2 with δ -approximate alternating simulation relation R. Let Y s ⊆ Y be a subset of safe outputs and h i be given by ( 2) with i = 1, 2. Let us assume T 1 is finite and let V 1 and C 1 be accordingly given by ( 4) and ( 6). For a ∈ R, let

S a 1 = {x 1 ∈ X 1 | V 1 (x 1 ) ≤ a}, then • Sa 2 = R(S a 1 ) is a controlled-invariant subset of X a+δ 2 = {x 2 ∈ X 2 | h 2 (x 2 ) ≤ a + δ }. • A safety controller for Sa 2 is given for all x 2 ∈ X 2 by C a 2 (x 2 ) =    u 2 ∈ enab ∆ 2 (x 2 ) ∃x 1 ∈ R -1 (x 2 ) ∩ S a 1 , ∃u 1 ∈ C 1 (x 1 ), ∆ 2 (x 2 , u 2 ) ⊆ R(∆ 1 (x 1 , u 1 ))    (7)
Proof. We first prove that Sa 2 is a subset of X a+δ

2

. For all x 2 ∈ Sa 2 , there exists

x 1 ∈ S a 1 such that (x 1 , x 2 ) ∈ R. From Definition 8, we have d(H 1 (x 1 ), H 2 (x 2 )) ≤ δ . From Theorem 7, S a 1 is a subset of X a 1 = {x 1 ∈ X 1 | h 1 (x 1 ) ≤ a}.
Since h i are given by (2) with i = 1, 2, it follows from the triangular inequality that

h 2 (x 2 ) ≤ h 1 (x 1 ) + d(H 1 (x 1 ), H 2 (x 2 )) ≤ a + δ . Hence x 2 ∈ X a+δ 2 .
We now prove that Sa 2 is a controlled invariant subset admitting C a 2 as safety controller. We first prove that Sa 2 ⊆ dom(C a 2 ). Let x 2 ∈ Sa 2 then there exists

x 1 ∈ S a 1 such that (x 1 , x 2 ) ∈ R. From Theorem 7, S a
1 is a controlled invariant subset with C 1 as associated safety controller. Hence

x 1 ∈ S a 1 ⊆ dom(C 1 ). Then, let u 1 ∈ C 1 (x 1 ), from Definition 8, there exists u 2 ∈ enab ∆ 2 (x 2 ) such that ∆ 2 (x 2 , u 2 ) ⊆ R(∆ 1 (x 1 , u 1 )). It follows from (7) that u 2 ∈ C a 2 (x 2 ) and thus x 2 ∈ dom(C a 2 ). Now, let x 2 ∈ Sa
2 , and u a 2 ∈ C a 2 (x 2 ), then from (7) there exists

x 1 ∈ R -1 (x 2 ) ∩ S a 1 and u 1 ∈ C 1 (x 1 ) such that ∆ 2 (x 2 , u 2 ) ⊆ R(∆ 1 (x 1 , u 1 )). Since x 1 ∈ S a 1 and u 1 ∈ C 1 (x 1 ), it follows from Theorem 7, that ∆ 1 (x 1 , u 1 ) ⊆ S a 1 . Hence, ∆ 2 (x 2 , u 2 ) ⊆ R(S a 1 ) = Sa 2 .

Hence Sa

2 is a controlled invariant subset and C a 2 is an associated safety controller. 2 One can see from (7) that the controller C a 2 generally depends on the value of the parameter a, while the controller C 1 for the abstraction does not and is common for all controlled-invariant subset S a 1 , a ∈ R. For the concrete system, a common safety controller for all controlled-invariant subset Sa 2 , a ∈ R, can be obtained as follows: Corollary 11. Under the assumptions of Theorem 10, a common safety controller for Sa 2 , a ∈ R is given for all x 2 ∈ X 2 by

C 2 (x 2 ) =      u 2 ∈ enab ∆ 2 (x 2 ) ∃x 1 ∈ arg min z 1 ∈R -1 (x 2 ) V 1 (z 1 ), ∃u 1 ∈ C 1 (x 1 ), ∆ 2 (x 2 , u 2 ) ⊆ R(∆ 1 (x 1 , u 1 ))      (8) Proof. Let a ∈ R, let x 2 ∈ Sa 2 , and x 1 ∈ arg min z 1 ∈R -1 (x 2 ) V 1 (z 1 ). Since Sa 2 = R(S a 1 ), we have V 1 (x 1 ) = min z 1 ∈R -1 (x 2 ) V 1 (z 1 ) ≤ a,
which gives that x 1 ∈ S a 1 . Hence, it follows that for all x 2 ∈ Sa 2 , C 2 (x 2 ) ⊆ C a 2 (x 2 ). It then follows from Theorem 10 that C 2 is a safety controller for all Sa 2 , a ∈ R, such that Sa 2 ⊆ dom(C 2 ). Then, let x 2 ∈ Sa 2 and x 1 ∈ arg min z 1 ∈R -1 (x 2 ) V 1 (z 1 ), from above we have x 1 ∈ S a 1 ⊆ dom(C 1 ). Then, let u 1 ∈ C 1 (x 1 ), from Definition 8, there exists

u 2 ∈ enab ∆ 2 (x 2 ) such that ∆ 2 (x 2 , u 2 ) ⊆ R(∆ 1 (x 1 , u 1 )). It follows from (8) that u 2 ∈ C 2 (x 2 ) and thus x 2 ∈ dom(C 2 ). Hence Sa 2 ⊆ dom(C 2 ). 2
When both transition systems T 1 and T 2 are finite, the following result makes it possible to compare the functions V 1 and V 2 : Theorem 12. Let T i with i = 1, 2, be two metric transition systems with the same set of outputs Y . Let Y s ⊆ Y be a subset of safe outputs and h i be given by ( 2) with i = 1, 2. Let us assume T 1 and T 2 are finite and let V 1 and V 2 be accordingly given by (4). Then,

• If T 1 δ T 2 , with δ -approximate alternating simulation relation R, we have

∀(x 1 , x 2 ) ∈ R, V 2 (x 2 ) ≤ V 1 (x 1 ) + δ . • If T 1 ∼ δ T 2 , with δ -approximate alternating bisimulation relation R, we have ∀(x 1 , x 2 ) ∈ R, V 1 (x 1 ) -δ ≤ V 2 (x 2 ) ≤ V 1 (x 1 ) + δ .
Proof. We prove the first item.

Let (x 1 , x 2 ) ∈ R, let a = V 1 (x 1 ) and let S a 1 = {z 1 ∈ X 1 | V 1 (z 1 ) ≤ a}.
Clearly, x 1 ∈ S a 1 and therefore x 2 ∈ Sa 2 = R(S a 1 ). From Theorem 10, we have that Sa 2 is a controlled invariant subset of X a+δ 2 . By Theorem 7,

S a+δ 2 = {z 2 ∈ X 2 | V 2 (z 2 ) ≤ a + δ } is the maximal controlled invariant subset of X a+δ 2 . Thus, Sa 2 ⊆ S a+δ 2 . It follows that V 2 (x 2 ) ≤ a + δ = V 1 (x 1 ) + δ .
We now prove the second item. T 1 ∼ δ T 2 implies that R is a δ -approximate alternating simulation relation from T 1 to T 2 . Then, it results from the above that, for all

(x 1 , x 2 ) ∈ R, V 2 (x 2 ) ≤ V 1 (x 1 ) + δ . R -1 is also a δ -approximate alternating simulation relation from T 2 to T 1 . Then, for all (x 1 , x 2 ) ∈ R, V 1 (x 1 ) ≤ V 2 (x 2 ) + δ . 2

NUMERICAL RESULTS

In this section, we illustrate the results presented in the previous sections using the boost DC-DC converter. This electric power convertor has two operation modes depending on the position of a switch. It can be modeled as a switched system with two modes and the two dimensional dynamics associated with both modes are affine of the form: ẋ(t) = A p(t) x(t) + b with p(t) ∈ {1, 2} and x(t) ∈ R 2 . For numerical values of the system matrices, see [START_REF] Girard | Approximately bisimilar symbolic models for incrementally stable switched systems[END_REF]).

We sample time with period τ = 0.5 and represent the sampled dynamics of the switched system as an infinite transition system T 2 . Following the approach described in [START_REF] Girard | Approximately bisimilar symbolic models for incrementally stable switched systems[END_REF]), one can compute δ -approximately (alternatingly) bisimilar discrete abstractions for arbitrary precision δ > 0. Choosing δ = 0.2 and restricting the dynamics of the abstraction to the compact set X = [0.65, 1.65] × [4.95, 5.95], one obtains a finite abstraction T 1 with 264196 states. Note that in this approach, there is no distinction between states and outputs (i.e. the output map is the identity map).

We consider the safety control problem, which consists in maintaining the state of the system within the set X S = Y S = [1.1, 1.6] × [5.4, 5.9]. Using the finite abstraction, we apply the functional fixed-point algorithm (3), which terminates after 107 iterations. The fixed-point V 1 is shown in Figure 1, while the resulting safety controller C 1 given by ( 6) is shown on Fig. 2. In particular, one can see that V 1 characterizes maximal controlled-invariant subsets of a family of sets parameterized by their distance to the safe set. Remarkably, the controller C 1 is a common safety controller for all these controlled-invariant subsets.

On Figure 3, one can check that V 1 acts as a weak Lyapunov function (i.e. it is non-increasing) for the controlled transition system T 1C 1 , where we used a lazy implementation of the controller C 1 : when there is a choice between mode 1 and 2, the controller selects the one that is already on. Figure 4 shows a trajectory of the concrete system T 2 (i.e. the switched system), associated to the trajectory of the controlled abstraction T 1C 1 depicted in Figure 3. It can be witnessed that the trajectory never goes beyond the safe set, which is represented by the green dashed lines in the figure. Moreover, the controller tends to keep to trajectory away from the boundary of the safe set.

CONCLUSION

In this paper, we have presented a quantitative approach to safety controller synthesis. We have shown how using a functional fixed-point iteration, one can compute a measure of safety of the sates of a finite transition system. The measure also provides a simple design for a safety controller that is common to a family of parameterized controlled-invariant sets. Using abstraction-based techniques, we have shown that the approach can be lifted to infinite transition systems. A numerical example shows the effectiveness of the approach.

This work opens many further research directions. The most immediate extension of the work is to adapt the theoretical results to generalize the functional fixed-point iteration to a class of infinite transition systems. Secondly, similar quantitative controller synthesis approaches should be developed for other types of specifications such as reachability, stability or more complex properties expressed in some temporal logic. Thirdly, an intriguing question is to investigate the relation between quantitative synthesis and the synthesis of robust controllers for qualitative specifications.

Fig. 1 .Fig. 2 .

 12 Fig. 1. Fixed-point V 1 of algorithm (3) for the boost DC-DC converter. The dashed blue lines depict different level sets X a 1 of the function h 1 for different values of the parameter a ∈ R. Gray colors depict different level sets S a1 of the function V 1 for the same values of a; white color correspond to states x 1 such that V 1 (x 1 ) = +∞.Safety controller C 1 *

Fig. 3 .Fig. 4 .

 34 Fig. 3. Time evolution of the function V 1 along a trajectory of the controlled abstraction T 1C 1 .