Vérification et Test des Systèmes Embarqués

Session Horaire Titre du cours Responsable
1 lundi, 24 février Cours: Introduction vérification et test Ulrich Kühne
2 lundi, 24 février Cours: Test-Driven Design Ulrich Kühne
3 mercredi, 26 février TP: Test-Driven Design Ulrich Kühne
4 vendredi, 28 février

Cours: Introduction méthodes formelles

Étienne Borde
5 lundi, 2 mars Cours: Vérification du matériel
Cours: System Verilog Assertions
Ulrich Kühne
6 lundi, 2 mars  TP: Vérification du matériel avec SVA Ulrich Kühne
7

mercredi, 4 mars

TP: UPPAAL Étienne Borde
8 vendredi, 6 mars

Cours: Modélisation des systèmes embarqués

Ludovic Aprville

 

Fichier attachéTaille
PDF icon se767-intro.pdf2.01 Mo
PDF icon se767-tdd.pdf1.24 Mo
PDF icon Vérification du matériel2.52 Mo
PDF icon System Verilog Assertions556.84 Ko

Test Driven Design of Embedded C

In this exercise, we are going to design and implement a light scheduler in C. The purpose of this module is the autmatic switching of room lights following a programmed schedule. This could be used for example as an optical alarm clock in your bedroom, or in order to fake some activity during your holidays so as to prevent somebody from breaking into your house and stealing your toothbrush.

First thing to do: If you haven't done so already, you need to request access to the gitlab group, where your personal repository will then be created for you. Head over to the group on gitlab and request access. Your teacher will then take care of creating all the user repositories.


0. How (not) to do this Exercise

The purpose of this exercise is putting your newly learned TDD skills into practice. Please note that the primary goal is NOT to code a light scheduler, although - if you do it right - you will end up with a light scheduler. TDD requires some discipline and it is hard to resist temptation to coding ahead of the tests, or to skip tests, or to write more code than necessary to make the tests pass. So try to take a step back from pure coding in order to get the feeling of how TDD works. It might work for you. Here is the three golden rules that you should follow during this exercise:

  1. Write the test first
  2. Watch the test fail
  3. Write the minimal code required to make the test pass

1. Requirements

Before starting to code (even before writing the tests...), let's review the requirements of the light scheduler:

  1. The LightScheduler allows to schedule the switching of room lights (on or off) on a specific day at a specific time (hour and minute).
  2. Each light is identified by an integer number.
  3. The actual switching is taken care of by a separate light control driver.
  4. If an event is scheduled, it will be triggered only on the specified day and within one minute around the specified time.
  5. The user can schedule switching a light on or off on a specific day of the week at a specific time.
  6. The user can schedule switching a light on or off everyday at a specific time.
  7. The user can schedule switching a light on or off during weekends (Saturday and Sunday).
  8. The user can schedule switching a light on or off during week days (Monday till Friday).
  9. The user can schedule multiple events for the same light.
  10. The user can remove a scheduled event.
  11. The user can schedule a maximum number of 256 events.

Exercise: Write a test list for the above requirements (in English or French, don't start writing C code yet). It should briefly describe for each test case the actions to execute and the expected behavior. Make sure that you also test negative results (such as nothing happens if no event is scheduled at the present day and hour...). Keep the tests simple and self-contained. You should come up with at least 10 or 12 tests, maybe more. If you run out of ideas, don't worry. Do not spend too much time on this exercise. It is normal to add more test during the development, adapting them to the evolving interface and code structure.


2. Setting up your Working Environment

In your home directory (or any directory where you keep your code and exercises), open a terminal and execute the following commands in order to get the sources for this exercise. Please replace YourName by the correct name of your personal repository.

git clone git@gitlab.enst.fr:MSSE/TestVerif/2019-2020/YourName.git
cd YourName
git checkout master
git remote add tp-tdd git@gitlab.enst.fr:MSSE/TestVerif/tp-tdd.git
git remote update
git merge --allow-unrelated-histories tp-tdd/master
git submodule init
git submodule update

Don't forget to add - commit - push regularly!

Let's look at the content of the directory you just checked out:

.
├── include
│   ├── LightControl.h
│   ├── LightScheduler.h
│   └── TimeService.h
├── Makefile
├── README.md
├── src
│   └── LightScheduler.c
├── test
│   └── TestLightScheduler.c
└── Unity
    ├── ...
    ...

This does not look too scary. The directory include contains the header files for our production code. The sources can be found in src. The test cases will be put into test. Finally, Unity is the root of the Unity testing framework.

In order to see if your setup is working fine, try to build and run the tests:

$> make
rm -rf run_TestLightScheduler  *~ src/*~ test/*~ include/*~
ruby Unity/auto/generate_test_runner.rb test/TestLightScheduler.c test/TestLightScheduler_Runner.c
gcc -Wall -std=c99 -Iinclude -IUnity/src  Unity/src/unity.c  src/LightScheduler.c src/LightControlSpy.c  test/TestLightScheduler.c test/TestLightScheduler_Runner.c -o run_TestLightScheduler
Running run_TestLightScheduler
test/TestLightScheduler.c:16:testThatFailsBecauseItDoesNotTestAnything:FAIL: Go write some real tests!

-----------------------
1 Tests 1 Failures 0 Ignored
FAIL
Makefile:41: recipe for target 'run_tests' failed
make: *** [run_tests] Error 1

The output should look roughly as shown above. Don't worry about the error message. We will write useful tests later. If there is a compilation error, go see a teacher.


3. Module Dependencies

Let's have a look at the implied building blocks and their dependencies. The light scheduler depends on two modules, LightControl and TimeService. Both have transitive dependencies as shown in the following figure:

Dependencies of the LightScheduler

The LightControl is the abstract interface to the actual light switching hardware within some home automation system. At this time, we do not know anything about how it does its job, and that is actually a good thing: If we manage to keep the interfaces abstract and generic, then our final product will be portable to any home automation system that is capable of implementing the required interface functions. To know which functions we are talking about, let's have a look into the LightControl.h header file:

void LightControl_init(void);
void LightControl_destroy(void);
void LightControl_on(int id);
void LightControl_off(int id);

So besides functions to initalize and destroy the light driver, there is just two functions, switching on and off a light with some integer identifyer.

The TimeService is slightly more complicated. It is a module which builds on top of some real time operating system (RTOS) and it offers a convenient interface to user space programs to flexibly register callback functions that need to be called periodically. This is the interface defined in TimeService.h:

enum Day {
    NONE=-1,
    MONDAY=1,
    TUESDAY,
    WEDNESDAY,
    THURDSDAY,
    FRIDAY,
    SATURDAY,
    SUNDAY,
    EVERYDAY=10,
    WEEKDAY,
    WEEKEND
};

typedef enum Day Day;

typedef struct {
  Day day;
  int minuteOfDay;
} Time;

void TimeService_init(void);
void TimeService_destroy(void);
void TimeService_getTime(Time *time);
void TimeService_setPeriodicAlarm(int seconds, void (*callback)(void));
void TimeService_clearPeriodicAlarm(int seconds, void (*callback)(void));

In the first part, we have some convenient data types to represent the time of day, which will be useful for our own module later on. The API consists of three functions (besides initialization and finalization): Getting the current time and setting and removing a periodic callback, respectively.

The header of the module to be implemented is more or less empty for the moment. You are free to add and modify any number of functions needed to implement the requirements. To get an idea of the interaction of the different modules, here is a typical use case:

This is what happens: The user initializes the scheduler, which in turn tells the time service to wake him up once a minute. Then, the user schedules a switching event of light 3 for Sunday, 8:00 pm (1200 minutes after midnight). Some time later (Sunday, 7:59 pm), the time service wakes up the scheduler. However, the scheduler does not have any event scheduled for the current time, so it returns without further action (note that there is a small detail left out here: How does the scheduler now what time it is...?). One minute later, the scheduler is woken up again and this time, it triggers the scheduled event by calling the respective function of the light controler.


4. Test Infrastructure

Please be patient, we are still not starting to implement the light scheduler. First of all, we will set up the necessary test infrastructure in order to test our production code in a purely C based unit testing environment on a standard Linux host, thereby removing all hardware and operating system dependencies. We have already set up the Unity testing framework and a suitable Makefile, which you will need to modify during the exercises. The first thing to do is thus to build the right abstractions of the light controlling hardware and the real time services.

Look again at the use case in the sequence diagram in Section 2. The problem we face here is twofold: First of all, the time when the event is scheduled by the user and the moment when it is eventually triggered are completely asynchronous. In order to test the shown scenario with real hardware, we would need to waint until the next weekent to see if the event gets triggered. Secondly, in order to automate the tests, we would need some way to get to know the current state of the controlled lights. Therefore, we will use two different TDD design patterns to create test doubles for the two modules which our scheduler depends on: The TimeService will be replaced by a fake object, allowing us to set the current time deliberately and independently of the real time. The LightControl driver will be replaced bby a test spy, which will allow us to check that the scheduler has ordered the switching of the correct lights, without requiring any real hardware. The following figure shows the new situation:

Breaking dependencies with test doubles

The notation in the above diagram is (kind of) UML, the arrows between the LightControlSpy and LightControl denote that the LightControlSpy implements (or extends) the LightControl interface. Strictly speaking, there is no such notion as interface nor a class hierarchy in C, but this shows the basic idea of the test doubles.

4.1 Spying on the Lights

The desired effect of a scheduled event being triggered is that the respective light should be switched on or off at the right time. How do we check if the switching has taken place or not? If we would use real hardware, we could use a test engineer (or an intern, which comes at a lower cost...) to check on her watch that the lights go on and off at the right time. A more sophisticated setup would involve light sensors and some more hardware to automate this process. But in fact we do not really care about the physical lights so much, we only need to make sure that the LightScheduler makes correct use of the available hardware abstraction layer, which in this case is the LightControl driver. The problem here is that the given LightControl interface (see section 1) does not provide any possibility to obtain the current state of the lights or to detect the latest state change. Therefore, we will extend its interface with functions to retrieve this information during tests: A test spy.

So let's start coding the test spy... Oh, wait! Isn't this exercise about writing the tests first? That's right! We want to make sure that the test doubles that we write behave as expected. Furthermore, writing a test is a good way to force oneself to think about the interface first before starting to code. So let's write a simple test that uses our spy: Create a new file test/TestLightControlSpy.c and put in the following code:

#include "LightControlSpy.h"
#include "unity.h"

void testLightControlSpyReturnsLastStateChange(void)
{
    LightControl_init();
    LightControl_on(42);
   
    TEST_ASSERT_EQUAL( 42, LightControlSpy_getLastLightId() );
    TEST_ASSERT_EQUAL( LIGHT_ON, LightControlSpy_getLastState() );

    LightControl_destroy();
}

Instead of staring at the lights in our home, we just retrieve the last state change using the spy interface. In order to add this test to the build, we need to edit the Makefile, too. Look for the line TESTS = TestLightScheduler and add the following line below:

TESTS += TestLightControlSpy

The Makefile takes care to automatically generate the corresponding test runner and to execute the test after completing the build. Let's have a try:

$> make
rm -rf run_TestLightScheduler run_TestLightControlSpy  *~ src/*~ test/*~ include/*~
ruby Unity/auto/generate_test_runner.rb test/TestLightScheduler.c test/TestLightScheduler_Runner.c
gcc -Wall -std=c99 -Iinclude -IUnity/src  Unity/src/unity.c  src/LightScheduler.c src/LightControlSpy.c test/TestLightScheduler.c test/TestLightScheduler_Runner.c -o run_TestLightScheduler
src/LightControlSpy.c:1:10: fatal error: LightControlSpy.h: No such file or directory
 #include "LightControlSpy.h"
          ^~~~~~~~~~~~~~~~~~~
compilation terminated.
Makefile:37: recipe for target 'run_TestLightScheduler' failed
make: *** [run_TestLightScheduler] Error 1

Not surprisingly, this didn't work, since we did not implement the test spy yet nor did we create the header file. Create a new file include/LightControlSpy.h and put in it the following code:

#ifndef LIGHT_CONTROL_SPY_H
#define LIGHT_CONTROL_SPY_H

#include "LightControl.h"

enum {
    LIGHT_ID_UNKNOWN = -1,
    LIGHT_STATE_UNKNOWN = -1,
    LIGHT_OFF = 0,
    LIGHT_ON = 1
};

int LightControlSpy_getLastLightId(void);
int LightControlSpy_getLastState(void);

#endif

By including the original light control header file, we make sure to be compatible with its interface, adding our own secret spying super powers on top of it. The enum type just provides some easier to read values that you should use in your test code. The purpose of the two additional functions should be clear: The first one allows us to retrieve the light identifier used in the latest state change event. The second one gives us the type of state change (on/off).

Exercise: Implement the spy. Create the file src/LightControlSpy.c and implement all its functions. This includes both the functions of the LightControl interface and the extended spying functions. Remember to type make after each change in order to build and run the tests. The output should give you enough hints how to proceed. Also try to respect the "minimal code to make the test pass" rule. It is there to prevent you from taking design decisions too early. Once the first test passes, add at least another test verifying that the state and light ID is unknown after creation. You can find some hints on the Unity test macros and syntax on this page.

4.2 Faking Time

If we think about the interactions between the time service and the light scheduler, they boil down to two things:

  1. The time service calls a callback function in the scheduler once a minute
  2. The scheduler can get the current day and time of day by calling the time service

For testing purposes, we can easily circumwent the first item by just calling the respective function ourselves inside the test code. Furthermore, we can completely abstract from any notion of real time: We can fake a time service by providing a function to our test code that allows us to set the "current time" to whatever value we need. The next time the scheduler asks about the current time, it will just get this value set by us. In this way, we can examine any moment in time that we like during testing.

As before, the best way to figure out the interface of the fake time service is writing a test that uses it.

Exercise: As for the light control spy, write some tests for the fake time service. It is up to you to define its interface, realising the functionality described above. Use the file names include/FakeTimeService.h and src/FakeTimeService.c, respectively. The tests should go into test/TestFakeTimeService.c. Make sure that the fake time service properly extends the time service interface, so it can act as a link time replacement. Proceed as before (test - watch it fail - make it pass) until all tests pass and you are satisfied with your fake time service.


5. The Light Scheduler

So we have finally come to the point where we can think of the target module, the light scheduler itself. The setup of the test infrastructure should have prepared you to properly use the TDD methodology. Your are free to define the interface of the light scheduler, as long as the final code fulfills the requirements.

Exercise: Implement the light scheduler using TDD.

Below you can find some hints and guidelines that will help you to come up with a clean and correct implementation.

1. Slow down to speed up

Sometimes it will seem to you a waste of time to write the tests first, then watching them fail, and then taking little steps to make them pass before moving on to the next test. However, the original problem which TDD is trying to solve is the long debug cycles caused by missing tests or by post-implementation testing. So everytime you make a small mistake that is immediately caught by a test, you have actually saved debugging time. Using TDD, progress might seem slower, but it is safe and predictable. Imagine testing your finished product and finding out you started with some completely wrong hypotheses. This is less likely to happen using TDD.

2. Writing the minimal code to make a test pass

This guideline might be the one which is the most difficult to respect, since it is hard to resist the temptation to write more code than is really necessary to make a test pass. However, it helps to make design decisions (such as data structures, function layout, modularisation, ...) when they are really necessary and not earlier. Sometimes, it seems really dumb: Returning constant 42 makes a test pass? Great, let's just write return 42. Done! If this is not enough for the final design, then there will be a test that will force us to revise our decision!

3. Make it work for one case, then for all

It makes sense to write the tests (and therefore also the production code) for cases of increasing complexity. So don't start with testing multiple scheduled events for the same time with randomization, but with testing for example correct initialization, then scheduling a single event, and so on. This prevents you from writing large pieces of complex code at once, which in likely to introduce more and harder to find bugs.

4. Keep the tests concise and simple

A good unit test test one thing and not three or more. Tests should be independent. Avoid writing tests that go on and on until they fill a whole screen in your editor. If there is more to test, write another unit test! If you are repeating the same initialization code in each test, it is time to move it to a separate function. Unity provides two useful functions for this purpose, which are called automatically before and after each test in the same file:

void setUp(void)
{
    // put common initialization code here
}

void tearDown(void)
{
    // clean up after testing
}

Finally, give the test function a name that describes what you are really testing.

5. Refactoring

Once a test passes, take a step back and look at your code. Is it readable? If not, add comments and useful variable names. Did you use copy and paste? Refactor your code and put repeated functionality into a helper function. If you run the tests after each modification, you can make sure that you didn't break anything.


6. Code Review

Once 1) you have written all the tests that were on your list, and 2) your code passes all of them, and 3) you have refactored and cleaned up your code, take a step back. Reconsider the requirements and check if each of them is covered by at least one of your tests. If you have missed something, start over until you covered all of them.

Exercise: Exchange your test list with your neighbors. See if there are tests that you have forgotten. Compare your implementations. How do the interfaces differ? Are there any significant differences? if yes, discuss your design decisions with the other group.


7. Optional Exercise for the Quick Ones

7.1 Extended Functionality - Randomization

Just at the moment when you were satisfied with your implementation, the customer comes in and tells you that there is a new requirement. Some very clever criminals are watching the houses to see if the lights are always turning on at the same time to see if it's just a home automation system faking activity. To smart out these criminal minds, the customer requires that each event can optionally be randomized. For each event, the user should have the possibility to give a number of minutes r, such that the event scheduled at time t will take place within the interval [t - r, t + r]. Of course, the exact time the event is triggered must vary each time the event takes place.

In order to add this feature, we will rely on a random number generator. Its interface (put it into include/RandomNumber.h) looks like this:

#ifndef RANDOM_NUMBER_H
#define RANDOM_NUMBER_H

void RandomNumber_seed(int seed);
int RandomNumber_randomInt(int max);

#endif

Write some tests for the requested functionality and then implement it. You need to find a good strategy to test random behavior while keeping the tests determistic. Think about how you could fake randomness.

7.2 More Testing

If you are already done and don't know what to do, you can finish the exercises that you started during the lecture on your own:

  • Finish the circular buffer
  • Finish the LED driver

In both cases, try and set up your working directories from scratch, including checking out the unit test framework and writing a Makefile. This will help you getting started with TDD in the future.

7.3 Mock Objects

Besides Unity, there is an additional library that can automatically generate mock objects and stubs for you, called CMock. You can find it on this website. Read the documentation and try to generate a mock interface for one of the modules used during the exercise.

7.4 Coverage

Are you sure that your unit tests really cover all your code? Use gcc's --coverage option together with gcov / lcov in order to find out.

Unity Syntax and Macros

Test Functions

Your test code is organized in test cases, where each test case is just a C function:

#include "unity.h"

void testSomethingInterestingShouldHappen(void)
{
  // your test code goes here
}

ATTENTION: In order to distinguish unit tests from arbitrary C functions in the same file, the script that generates the test runner considers only those functions whose name starts with "test" as unit tests. Please make sure that you respect this rule!

If you have common code that is run before and after each test case, move it to these two special functions:

void setUp(void)
{
  // prepare test environment
}

void tearDown(void)
{
  // clean up after test
}

 

Assertion Macros

Testing a Boolean expression is true:

TEST_ASSERT( a == 4 );

Testing a Boolean expression with explicit outcome:

TEST_ASSERT_TRUE( flag );
TEST_ASSERT_FALSE( !flag );

Testing a Boolean expression, supplying a message that will be displayed if it fails:

TEST_ASSERT_MESSAGE( 2 == 1 + 1, "The end is coming!");

Testing equality of various types:

TEST_ASSERT_EQUAL_INT( 5, x );
TEST_ASSERT_EQUAL_UINT16( 0xcafe, cup );
TEST_ASSERT_EQUAL_FLOAT( 3.15, pi );
TEST_ASSERT_EQUAL_STRING( "Hello world!", s );

This also works for arrays:

TEST_ASSERT_EQUAL_INT_ARRAY( expectedArray, a, numElements );

You can add a message to about anything of the above:

TEST_ASSERT_EQUAL_INT_MESSAGE( 5, x, "This is bad!" );

This test always fails, it can be used to remind you of a missing test case:

TEST_FAIL_MESSAGE( "This is a gentle reminder" );

You can ignore (the rest of) a test case if there are some issues you want to postpone. Use with care!

TEST_IGNORE( ); // FIXME: should be reactivated later

 

TP: Vérification avec SVA

Le but de ce TP est de vous permettre de vous exercer à la spécification formelle à l'aide d'un langage de logique temporelle, les SystemVerilog Assertions (SVA). L'exercise est divisé en deux parties:

  1. La formalisation d'une spécification textuelle (En préparation du TP; la spécification complète vous sera fourni au début du TP)
  2. La correction d'un composant mal implémenté (arbitre) en utitlisant un outil de vérification statique

Pour la syntaxe et la sémantique des différents opérateurs SVA, regarder les supports du cours. En plus, il y a un document pdf plus exhaustif dans le répertoire git du TP.

1. Spécification

Il s'agit d'un arbitre qui est censé de contrôler l'accès à une ressource commune (tel qu'un bus mémoire) à trois masters. Les masters signalent leurs demandes en mettant l'entrée req correspondante à 1, et l'arbitre donne la main à un des masters - suivant son algorithme d'arbitrage - en mettant la sortie gnt correspondante à 1. Une propriété de l'algorithme "round robin" est qu'il n'y a pas de priorité statique. Si il y a plusieurs requêtes simultanées, l'arbitre va donner la main à tour de rôle. Ce qui a pour conséquence que l'algorithme ne laisse personne mourir de faim (non-starvation en anglais): chaque requête va être servie finalement.

Exemple de fonctionnement

La figure montre un exemple de fonctionnement de l'arbitre. A partir du cycle 1, les trois masters font des requêtes simultanées. La première requête est acquise au cycle 2. Le deuxième et troisième master obtiennent la main dans les cycles 4 et 6. Noter que le premier master, après avoir laché sa requête (cycle 3), demande la main directement après (cycle 4). Mais, suivant le protocol "round robin", c'est le troisième master qui est servi d'abord.

Hypothèses sur l'environnement

Comme c'est le cas pour beaucoup de composants, le bon fonctionnement de l'arbitre dépend de certaines hypothèses sur l'environnement. Dans notre cas, on suppose que les masters suivent un protocol très simple:

H1: Une requête, une fois émise, ne doit pas être retirée avant qu'elle soit acquittée.
H2: Une requête, une fois acquittée, devra être retirée.

Noter que pour H2, une requête qui a été acquittée va rester active pendant le temps que le master se sert de la ressource avant de retirer la requête. Ce temps peut varier, mais il reste fini.

Propriétés à vérifier

On définit en suite les propriétés qu'une implémentation correcte doit respecter:

P1: Pendant le cycle suivant un reset, il n'y a pas d'acquittement.
P2: Il n'y a jamais plus d'un acquittement actif en même temps.
P3: Chaque requête sera acquittée (après un temps fini).
P4: L'acquittement reste stable jusqu'à ce que la requête correspondante soit relachée.
P5: S'il n'y a pas d'autres requêtes, une requête doit être traitée après un cycle au plus tard.
P6: Il n'y a pas d'acquittement sans requête.
P7: L'arbitrage est "fair".

Alors que la plupart de ces propriétés devrait être claire, la dernière est sûrement la plus difficile à formuler et à vérifier. Une possibilité pour exprimer P7 d'une façon plus précise est la suivante: Si un master i emet une requête, avant que celle-ci soit acquittée, l'arbitre peut acquitter au plus une requête pour chaque autre master j (j≠i).


2. Formalisation

L'objectif du premier exercice (en préparation du deuxième) est de comprendre la spécification textuelle du module et de la formaliser en SVA.

2.1 Témoins et Contre-exemples

Dans un premier temps, avant de passer à l'écriture du code SVA, on va regarder de plus prêt les hypothèses et propriétés. Pour chaque hypothèse et propriété, répondez aux questions suivantes:

  • Identifiez s'il s'agit d'une propriété de sûreté (safety) ou de vivacité (liveness)
  • Donnez - sous forme d'un dessin - une trace qui vérifie la propriété (témoin / witness)
  • Donnez une autre trace qui ne vérifie pas la propriété (contre-exemple / counter-example)

Si vous n'arrivez pas tout de suite à identifier le type d'une propriété, il est souvent utile de construire un contre-exemple d'abord. S'il existe un contre-exemple de longeur finie, il s'agit d'une propriété de sûreté, sinon de vivacité. Vous pouvez écrire plusieurs traces par propriété si vous jugez cela utile pour la compréhension.

2.2 SystemVerilog Assertions

Après avoir visualisé les témoins et les contre-exemples, passez à la formalisation des propriétés en SVA. Pour le moment, il suffit d'écrire les propriétés sur papier. La syntaxe exacte n'est pas important, il s'agit de capter au mieux l'intention de chaque propriété. Pour beaucoup de propriétés, il peut y avoir plusieurs façons de les spécifier en SVA. Il est même possible que la spécification textuelle soit imprécise ou ambiguë. Par exemple, l'expression "jusqu'à" peut être formalisé avec différents opérateurs SVA comme until ou until_with qui n'ont pas la même sémantique. Dans ce cas, il va falloir choisir ce qui vous semble le plus raisonable. La formalisation sert en faite à clarifier la spécification et à éliminer les ambiguïtés.

2.3 Comparaison avec la Spécification Finale

Pour la deuxième partie du TP, vous allez avoir accès au dépôt git pour récupérer la spécification en SVA ainsi que des parties d'implémentation en SystemVerilog. Allez dans votre répertoire personelle du cours SE767 et effectuez les commandes suivantes:

git checkout master
git remote add tp-sva git@gitlab.enst.fr:MSSE/TestVerif/tp-sva.git
git remote update
git read-tree --prefix=tp-sva tp-sva/master
git commit -m "merged sources into repository"

Vous trouverez le dossier tp-sva avec le sous-dossier arbiter. Les propriétés SVA se trouvent dans le dossier verif.


3. Deboggage avec qformal

Pour pratiquer la vérification formelle, il s'agit de corriger une mauvaise implémentation de l'arbitre. Prenez le temps de regarder et comprendre la spécification avant de commencer le travail. Pour le moment, il existe une implémentation incomplète de la spécification dans le fichier src/arbiter.sv.

3.1 Simulation

Le dossier simu contient l'environnement de simulation. Si vous vous déplacez dans ce dossier, vous pouvez lancer Modelsim en tapant

make simu_gui

Cette commande va d'abord compiler les sources du module sous vérification et du test bench (qui se trouve dans le dossier tb_src). Pour les deux composants, le test bench va simuler aléatoirement des scénarios d'usage, en respectant les contraintes d'entrée (hypothèses). Cette simulation vous sert pendant le développement pour vous assurer que votre implémentation fait bien quelque chose qui n'est pas complètement faux. Mais attention: aucune vérification n'est effectuée pendant la simulation. Elle ne remplace donc pas la vérification formelle que vous devrez effectuer (voir instructions ci-dessous).

3.2 Vérification

Néanmoins, vous pouvez aussi lancer le processus de de vérification. Cela peut servir à effectuer un contrôle de la syntaxe de vos propriétés SVA. Pour cela, allez dans le dossier verif de votre projet et tapez

make check

pour la version en ligne de commande ou

make check_gui

pour lancer l'interface graphique de l'outil de vérification. Attention, l'outil est assez bavard et il n'est pas toujours facile de retrouver les messages d'erreurs de syntaxe dans le bruit ASCII que produit la vérification. Après quelques temps la dernière commande devrez vous amener à une fenêtre comme la suivante:

Dans l'onglet Properties vous trouvez le résultat de la vérification. Les propriété qui n'ont pas été validées sont marquées par un F rouge. En faisant un double click sur le nom de l'assertion, un contre-exemple va être généré ce qui vous sert à debogger votre code ou la spécification. Des warnings sont indiqués par un petit triangle jaune. Attention: Dans la version testée, l'actualisation du modèle après un changement des sources (ou de la spécification) ne se fait pas toujours (ou jamais) automatiquement. Pour recharger le modèle et relancer la vérificatioin, ouvrez longlet Transcript et tapez dans la shell

source check.tcl

Le but ultime est d'arriver à implémenter le composant en respectant la spécification formelle. Vous avez atteint votre but si toutes les propriétés passent la vérification (sans warning).