CSC3333: Modelling Assignment
Aim
To gain experience in modelling, validation, and formal verification of a simple concurrent asynchronous
system.
Learning outcomes
This assignment will develop your knowledge and give you hands-on experience in:
• using Petri nets (in the form of Signal Transition Graphs) for modelling a concurrent system;
• using simulation to validate the model;
• using formal verification for detecting errors and increasing the confidence in the correctness of the
model;
• using software tools (Workcraft framework) for supporting the development process.
Deadline
* 4pm on Thursday 9
th December 2021 *
Weight
This assignment is worth 100% of the coursework mark for this module, i.e. 40% of the overall module
mark.
Assessment irregularities
This is an individual assignment, and the submitted models and report should be your own work (or
properly referenced). Do not share your work with other students to avoid facilitating plagiarism.
Multiway arbiters
The purpose of an N-way arbiter is to ensure mutually exclusive access to a shared resource used by N>1
clients. The‘early release’protocols of an N-way arbiter and a client are as follows.
Figure 1 – The‘early release’protocol of an N-way arbiter and the protocol of ith client.
Before accessing the resource, the i
th client sends a request to the arbiter (by raising signal ri). Such requests
can be sent concurrently by several clients. In response, the arbiter issues a grant (by raising signal gi).
Upon the receipt of the grant, a client can safely use the resource, with the guarantee that no interference
is possible from other clients. Having finished using the resource, the client lowers its request ri. At this
point the arbiter can issue a grant to another client, and concurrently lowers gi. Note that:
• It is guaranteed that at most one client can be in the critical section, i.e. the resource is used in a
mutually exclusive way.
• Even though it is possible that several of g1,…, gN are high simultaneously, it is guaranteed that all
but perhaps one clients to whom these grants have been issued have already indicated by lowering
their requests that they have exited their critical sections. In other words, at most one of the
Boolean expressions r1&g1,…,rN&gN can evaluate to 1, i.e. at most one client can be in its critical
section.
A stricter (a.k.a.‘late release’), arbitration protocol requiring that at most one of g1,…, gN is high at any time
is shown in Figure 2. Note that any correct implementation of this protocol will be also a correct
implementation of the‘early release’protocol in Figure 1, and for the purposes of this assignment either
protocol is acceptable.
Figure 2 – Late-release arbitration protocol requiring that the grants are mutually exclusive. Note the
difference from the protocol in Figure 1(left).
ME element (a.k.a. mutex) is described in the lecture notes, and its protocol is shown in Figure 3.
Figure 3 – The mutex protocol.
A single mutex can arbitrate between two clients, i.e. it implements a 2-way arbiter following the‘late
release’protocol (and thus also the less strict‘early release’protocol in Figure 1(left)). For more than two
clients, several mutexes have to be combined using some logic gates. Consider the following interface, i.e.
names and types (input/output) of signals, of a basic cell (BC) for building multiway arbiters:
Figure 4 – The interface of a basic cell (BC) for building multiway arbiters.
Such a BC communicates with two clients using two 4-phase handshakes, r1/g1 and r2/g2. These
handshakes are initiated by clients. In particular, a BC must guarantee that at most one of the Boolean
expressions r1&g1 and r2&g2 can evaluate to 1, i.e. at most one of the clients is in its critical section. A BC
communicates also with its parent BC using the 4-phase r/g handshake. This handshake is initiated by the
BC itself, and the BC acts as a client from the point of view of its parent BC. Such an interface allows one to
implement multiway arbiters by building balanced binary trees with BCs as their nodes. Such a tree of BCs
must guarantee that the clients following the protocol in Figure 1(right) access their critical sections in a
mutually exclusive way, i.e. at most one of the Boolean expressions r1&g1,…,rN&gN can evaluate to 1; that is,
such a tree of BCs should implement the arbitration protocol in Figure 1(left) or Figure 2. Intuitively, it
represents a knockout tournament bracket
https://en.wikipedia.org/wiki…
where the arriving requests compete for the access to the resource. For example, an implementation of an
8-way arbiter as a balanced tree of BCs is shown below (in the root BC, the parent handshake is shortcircuited,
and so this BC can be replaced by a mutex as an optimisation).
Figure 5 – An 8-way arbiter built as a balanced tree of BCs.
Internally, BC must contain a mutex to cope with metastability associated with the arbitration between its
clients’requests, and several logic gates. As a part of this assignment, you must formally specify the
behaviour of BC as an STG. You are not expected to derive a circuit implementation (if you do, it will not
be marked). Note that mistakes in a circuit can be extremely expensive in terms of the costs of recalling
various products (e.g. TV sets and mobile phones) deploying it, as well as huge reputational damage. Still
worse, the circuit may be deployed in a safety-critical system (e.g. an aircraft) where malfunction can result
in a loss of human lives. Hence, exhaustive verification is of paramount importance, and will be an
important part of assessment.
Tasks
- Develop an executable formal model of BC in the form of a safe STG. The interface of BC must be as in
Figure 4, and the names of signals and their types (input or output) must be as shown. - Validate your model by simulation.
- Formulate and formally verify relevant correctness properties of your model. Even simple
asynchronous systems may exhibit non-trivial behaviour, so make sure your verification strategy yields
high confidence in the correctness of your model. - Write a brief (strictly not more than 500 words) report describing how you approached the design,
validation, and verification, any problems you encountered / solved, and any other relevant findings. It
must also contain an image of your final model. (Optionally, it may contain 1 or 2 other images.
Verification properties formulated in REACH will not count towards the word limit, but their
explanations will.) This limit applies even if you do the advanced task below. - [Advanced] If you perform the above tasks well, it is realistic to get a mark in the II.1 region. If you aim
at a 1st class mark, your model should additionally solve the following problem. As explained in the
lecture notes, the mutex is vulnerable to unbounded delays associated with metastability resolution. In
a basic implementation of a multiway arbiter as a balanced tree of BCs, several metastability
resolutions occur sequentially – their number corresponds to the number of rounds in the tournament,
i.e. to the height of the tree. E.g. in the 8-way arbiter shown in Figure 5 the height of the tree is 3, so up
to 3 metastability resolutions take place sequentially, each having unbounded delay. This may result in
an unacceptably long response time of the arbiter as a whole. Re-design the BC so that no two
metastability resolutions in the whole tree happen sequentially, i.e. the response time of the arbiter is
no worse than the longest delay of a single metastability resolution that had to be performed, plus the
forward and backward signal propagation delays through the tree (which are not affected by
metastability and so are bounded). You must not modify the interface of BC or the way the tree of BCs
is constructed. Include a brief explanation of your ideas and an image of the final model (in addition to
the basic model) in the report. You should be able to reuse most of the verification strategy developed
for the basic model (so just state that in the report), but if you have any extra properties specific to this
design then you can include them too.
Submission
You should submit a single *.zip file to NESS by the above deadline. This file must contain:
• a Workcraft Signal Transition Graph (STG) models of:
o the basic model of a single BC, named“bc-basic.work”; and
o the advanced model of a single BC (a tree of such BCs would have concurrent metastability
resolution), named“bc-advanced.work”, if you have attempted the advanced part (note that
you still need to submit the basic model as well);
• a brief report in PDF format, named report.pdf (MS Word can save documents in PDF format).
Allocation of marks
The following indicative allocation of marks will be used for this assignment:
• Quality of the model [10 marks]
• Validation and formal verification [10 marks]
• Visual representation [4 marks]
• Report [6 marks]
• Concurrent metastability resolution [10 marks]
[Total 40 marks]
Notes and hints
• Avoid dummy transitions – they are not necessary for this model, have complicated semantics, and
some of the standard verification properties are limited to STGs without dummies.
• As the BC contains a mutex, there must be a mutex place in the STG. You may find it helpful to look at
the design of the CYCLE module in the online tutorial Hierarchical design of a realistic buck controller:
https://www.workcraft.org/tut…
Generally, look at the online tutorials which we do during practicals – there is a lot of useful stuff there.
• The signals representing the mutex’s outputs (grants) should be internal (otherwise you will break the
interface of BC). Note that the above practical requires one to insert internal signals to correct the
phases of mutex’s requests – in this assignment, the mutex’s grants should be internal, and there is no
need to correct signal phases; so these two things are unrelated. Avoid using any other internal signals –
you are not expected to derive a circuit, so no need to detect/resolve CSC conflicts, etc.
• Workcraft can verify whether given signals follow the handshake protocol – this feature is
described in the Handshakes Verification tutorial:
https://workcraft.org/tutoria…
• Workcraft is a cutting-edge tool with frequent releases, so some of its functionality has not been
tested extensively. If you suspect a bug, don’t suffer in silence! In the past, some students got bonus
marks for quality bug reports which led to improvements in Workcraft. Please check first whether
you are using the last version of Workcraft and whether the issue was already reported on GitHub:
https://github.com/workcraft/…
Don’t forget to CC me in the bug reports, and I might ask you to show the problem during a practical if I
cannot reproduce it myself.
• Formal verification is very important for this assignment – to get a good mark you should go well
beyond the standard STG properties (explained in workcraft.org/help/verification). If your STG is buggy
you will lose marks in both“Quality of the model”(for making a mistake) and“Validation and formal
verification”(for poor verification strategy that failed to catch the bug) sections.
• Remember that the STG must be safe. If your STG is unsafe, the verification in Workcraft will not
work – you will usually get an error message with a violation trace exhibiting unsafeness – it could be
either a pop-up window or a message in the Output pane. One may try to synthesise a safe STG from an
unsafe but bounded one via Conversion→Net synthesis* menu items. This will allow the verification to
proceed (though the mutex places are not always preserved by synthesis, so the choice between mutex
grants will cause violation of output-persistence), but may yield an incomprehensible STG.
• Your model should be visually comprehensible – nice layout, not messy, good use of node labels,
comments, good alignment of nodes, not too many crossing arcs, etc.
• For the report you will need to export images from Workcraft – this can be done is various graphics
formats via File→Export; in particular, SVG (vector graphics, so scales well) can be inserted into newer
versions of MS Word; PNG (raster graphics, so scales poorly) can be inserted into most text editors.
• The demonstrators are not expected to help you with this assignment – you should ask me (at a
practical or by email). I don’t normally answer questions like,“is this a correct way to model that?”,
“how to model that?”,“is this STG correct?”,“should I verify this property?”– these are related to the
modelling process and are a part of evaluation; the general advice is that you should capture in your
model the intended behaviour as well as possible, try to use the modelling techniques we considered in
the Petri nets part of the course, and think carefully about the verification strategy. However, I can
clarify the assignment spec if necessary, provide some general guidance concerning the intricacies of
Workcraft, the theory of Petri nets / STGs / circuits, etc., but without giving you any major spoilers.
If in doubt, just ask me – I may be able to help in some way, e.g. by pointing the relevant topics in the
lecture notes.