Loading
In this lab, you will have the opportunity to use a model-checker, namely NuSMV v2. NuSMV is based on BDDs. It also supports bounded model checking of LTL properties using a SAT solver, zchaff in this case.
NuSMV is installed in /it/kurs/relsyst/vt04/nusmv/. The name of the binary executable is NuSMV. Full instructions are available in the user manual
, which you are strongly advised to read. Typical uses are:
$ NuSMV somemodel.smv
$ NuSMV -bmc somemodel.smv
$ NuSMV -int somemodel.smv
The first command parses a model contained in somemode.smv and verifies all specifications. The second line performs bounded model checking using zchaff of the LTL properties (not the CTL ones). The third command allows you to use an interactive shell to simulate your model.
SMV models represent automatas with variables over finite discrete ranges. A model is made of several modules. From the tutorial:
MODULE inverter(input) VAR output : boolean; ASSIGN init(output) := 0; next(output) := !input;
A module can have local variables. It can also have inputs, which are references to other local variables in other modules. In this example, a inverter sets its output to the opposite value of the previous value of its input. In other terms, it sets the next value of the output to the opposite of the current value of the input.
All models must have a special module called main:
MODULE main
VAR gate1 : inverter(inp);
inp : boolean;
This module declares a boolean variable inp, which is set to be the input of an instance of inverter. The output of the inverter is accessible as gate1.output.
Further details are available in the tutorial.
A semaphore is an object commonly used when writing concurrent programs.
Semaphores are used to share access to a limited amount of resources. A
semaphore has two operations: grab and release. It also has a value. Initially,
the semaphore has the number N of available resources. A very common special
case is when N=1: this is used to implement mutual exclusion.
The grab operations works as follows: if the value of the semaphore is strictly
positive, it is decreased, and the process performing the grab is allowed to
continue. Otherwise, if the semaphore has value 0, the process is put to wait.
The release operation increases the semaphore by one. If there is one or more
process(es) waiting after having attempted a grab, exactly one of them is
allowed to decrease the semaphore and continue.
In this assignment, you are asked to model several processes (more than 2) and
to implement a semaphore controlling the access to N resources (with N>1, but
less than the number of processes).
Your semaphore implementation must respect the mutual exclusion property: no
more than N processes should ever be able to hold the semaphore simultaneously.
It should also be the case that any process requesting to grab a semaphore
should eventually do so.
The N-queens problem is a puzzle where the goal is to put N queens on NxN chess
board so that no queen may threaten another queen. In other words, no 2 queens
should be on the same diagonal, line nor file.
In this assignment, you will use smv to model the board and the N queens.
Then you will use a property describing valid solutions (no 2 queens threaten
eachother) and run the model checker to attempt to find such a solution. You
will model the problem for two sizes of the board: N=4 and N=5.
Sequential multiplier.
Goals:
checking.
Requires: Basic computer architecture
Description.
A sequential multiplier is a circuit computing the product of two integers. In
this assignment, we will limit ourselves to the case of unsigned (i.e. non
negative) numbers. One way to perform a multiplication is to use to good old
method kids learn at school:
21 X 57 -- 147 + 105. ---- 1197
This method is based and additions and shifts. The algorithm for computing the
product of two binary numbers A and B is:
Let C=0; While (B != 0) if (B is odd) then C = C+A B = B >> 1; (or B = B/2) A = A << 1; (or A = A*2) Done
Step 1:
Build an smv model of a one-bit adder. A one bit adder is a component adding two
bits and a carry bit. The result consists of the result bit and another carry
bit:
MODULE add1(a0, b0, cin)
VAR s0: boolean;
cout: boolean;
a0 and b0 are the two bits to add. cin is the input carry bit, it is required to
perfom the addition of two words of several bits. s0 is the result of the
addition, cout is the carry out bit, used in case the result of the addition
requires 2 bits.
This component is purely combinatorial, i.e. it computes the result
"immediately".
Step 2:
Build an 8 bits adder by chaining several one-bit adders:
MODULE add8(rA, rB, cin)
VAR rS: array 0 .. 7 of boolean;
cout: boolean;
rA and rB are two arrays of 8 bits representing two 8-bits registers. cin is the
input carry bit. Most of the time, it is set to 0. rS represents the 8-bits
register containing the result of the addition. cout is the output carry bit
(also called overflow bit). cin and cout are used when building adders for
larger words, in the same way that 1-bit adders are used to build 8-bits adders.
This component is also combinatorial.
Step 3:
We will now verify that the 8-bits adder is correct. Build a main component
defining two 8-bits registers, let's call them rA and rB. The main module should
also declare a local variable of type "add8", called rS. Write an LTL
property specifying that the interpretation of the result of the additions of rA
and rB is the sum of the interpretations of rA and rB. By "interpretation of
rA", it is meant "the number encoded in registered rA". You may want to create a
module to interpret registers. Although this module does not represent any
component in our system, it makes it easier to write the property we want to
verify:
MODULE convert(rA) VAR n: 0..255; ASSIGN n := rA[0] + 2*rA[1] + 4*rA[2] + ...;
Step 4:
Once you have verified that your 8-bits adder works correctly, you can start
building a 4-bits multiplier. This multiplier can perform multiplications of two
numbers encoded on 4 bits, resulting in a number whose encoding potentially
requires 8 bits.
This component is sequential in the sense that it requires several clock cycles
to perform its computation. Its interface is:
MODULE mult4(rA, rB, enable)
VAR r0: array of boolean;
r1: array of boolean;
rS: array of boolean;
ready: boolean;
...
rA and rB are two arrays of 4 bits. r0 and r1 are local variables used for
computing the multiplication. The result should finally appear in rS. The exact
sizes of r0, r1 and rS are not specified here, it is up to you to find how many
bits are required.
The component works as follows. When the component is ready to perform a
multiplication, it sets its "ready" bit to 1. When the "enable" input bit is set
to 1, the multipliers copies rA and rB into r0 and r1, resets "ready" to 0 and
performs the multiplication, possibly taking several clock cycles. When the
multiplier is done with the computation, it sets "ready" to 1 again. At this
point, rS must contain the result of the product.
Step 5:
You will now attempt to verify the multiplier. Modify the main module to replace
the adder by a multiplier, and insert new variables if needed.
Modify the LTL property as required. Unless you are using your own
ultra-performant personal computer, I advise you to restrict the verification to
small numbers, such as 4bits x 2bits. Start NuSMV to verify your design. Chances
are, NuSMV will fail the verification, taking an enormous amount of memory. It
is probably a good idea to run "top" to observe the consumption of the NuSMV
process.
Normally, you should have just observed a famous case defeating BDD-based
verification. Fortunately, NuSMV also supports verification using other methods
than BDDs: it can also perform SAT-based Bounded Model Checking using zChaff, a
SAT solver. To use this method, you need to set an environment variable:
Bash/Sh:
export sat_solver=zchaff
or for Csh:
setenv sat_solver zchaff
Then run NuSMV:
NuSMV -bmc yourmodel.smv
You may recall that Bounded Model Checking is normally used for debugging
systems, i.e. prove that systems are incorrect. It can also be used to prove
systems correctness. Depending on how you implemented the solution, your system
should take a maximum number N of steps to perform the computation. If the BMC
procedure fails to find a counter-examples after N steps, you know your system
is correct. How much is N in your case? Did you succeed to verify your
multiplier. Note that the computation may still take time (several minutes,
possibly hours). It should however be feasible to verify a 4bits x 2bits
multiplication in a few minutes, taking no more than 100Mb or RAM.
The report should include a link to your SMV model files. You should also describe the meaning of variables in your models, as well as your specifications.
| Link types on this page: | External link |