You should probably use Modelsim (which includes PSL) for this exercise. Alternatively, NUSmV can be used, but you must recode the example into SMV concrete syntax by hand. SoC D/M Proficiency Tick 4: 5 credits. Dynamic validation using Monitors/Checkers and PSL. An arbiter makes a decision about which requester for a shared resource will next be granted service. The material on the following link summarises a number of basic types of arbiter: http://www.cl.cam.ac.uk/teaching/1011/P35/arbiter/zhp711199d4d.html There are a number of stages to this assignment. The first three steps call for 'gate-level' designs. Feel free to present your 'gate-level' designs using structural RTL (Verilog or VHDL) or structural SystemC or using actual circuit diagrams. Warning: to keep your answers simple it is recommended that you choose a simple synchronous, static priority arbiter for your study. 1. Design at the gate-level an arbiter for three customers and a single resource and say what basic type of arbiter it is. (You do not need to include details of the resource or customers.) 2. Give a completely separate gate-level design that is a monitor (or checker) of the following safety property: "At all times, never is the resource granted to more than one requester". 3. Give a completely separate gate-level design that is a monitor/checker of the following liveness property: "Whenever reset is not asserted, when a request is made on the resource, it will eventually be granted". [This used to read like this (sorry for the minor confusion): "Whenever reset is not asserted, when a resource is requested, it will eventually be granted".] These two checkers should be implemented in separate files or modules and they are designed to connect to the external terminals of the arbiter to monitor its behaviour. The checkers should have an error output to indicate a detected failure. Note that there is a limit to the ability to check liveness properties with run-time monitors, as discussed in question 2. 4. Give a PSL (or similar temporal logic style) assertion that checks the safety property of stage 2 above. 5. Give a PSL (or similar temporal logic style) assertion that checks the liveness property of stage 3 above. 6. Answer three of the questions below. NOTE: Your arbiter design does not necessarily need to fulfil all the properties being checked. Questions: 1. Expain whether and why your gate-level checkers check exactly what you have specified in PSL. 2. What problem arises when trying to check so-called 'strong' properties using monitoring checkers and how did you handle this in your design ? 3. Arbiters can be classified as synchronous or asynchronous. Consider an arbiter that is the opposite to yours in this respect and show any corresponding modifications needed to your temporal logic expressions. 4. PSL deals with concrete values and not symbolic data values. Is it easy to describe a large arbiter that uses the round robin discipline using just concrete values? Try to sketch a better syntax. Do SystemVerilog assertions fair better? 5. Consider a TLM implementation of the arbiter - how would you adapt your PSL specifications to be used in the TLM environment (see Dahan and Bombieri etc) ? FULL CREDIT WILL BE GIVEN FOR 3 ANSWERS BUT IT IS RECOMMENDED TO TRY ALL OF THEM. - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - Questions arising > How are we going to implement the arbiter using built-in Verilog > primitives AND an always statement, since all these primitives > “accept” only nets as output variables? If you are making a gate-level design in structural RTL a module will consist only of component instances and nets. There will be no 'always' statement in a structural RTL design: the 'always' keyword introduces a thread of control used for behavioural expression. Whether you use the builtin Verilog gates or some others from any other library does not matter. I am not sure what concern you have when you say the gates only accept a net? Surely this is correct: we expect the gates to be wired to each other using nets with at most one output terminal from a gate connected to each net. >When reset is not asserted == (reset == 0)? Yes, for an "active high" signal, not asserted is when it has logic zero. > Could you further explain the liveness property? “When a resource is > requested, it will eventually be granted” -> do you refer to cases > where more than one resources are requested concurrently? There is just exactly one resource being allocated by the arbiter. However, we must consider the situation where there is more than one pending request for it at any instant. If there were never multiple concurrent requests, we would not need an arbiter. > Could you please indicate which is the appropriate syntax to use a > simple PSL assert in Verilog (in modelsim)? I tried a few variations > and I keep getting either compile or loading errors. E.g. error: > assert(grants[0] or grants[1] or grants[2]); (compile error) psl > error: assert(grants[0] or grants[1] or grants[2]); (compile error) > assert(grants[0] or grants[1] or grants[2]); (loading design error) At first glance the problem is that you dont say 'when' it should hold and also you are using the VHDL flavour of PSL where the symbol for logical disjunction is the word 'or' whereas in Verilog it is the '||' double stile operator. For a straightforward safety property that should always hold or never should hold then use something like: assert always (grants[0] || grants[1]) but this will not hold of a sensible arbiter of course. > Let's assume that the arbiter receives as input 3'b011. > 1. Obviously grants[0] is assigned 1. But what does the "eventually" mean? > 2. That on the next positive edge of the clock grants[1] is assigned 1? > Or just sentence 1? > > For 2 we would need to keep some kind of history right? In general, a liveness checker must keep some history. Also, not all arbiters will satisfy this sort of liveness condition: a request that is deasserted before it is granted might get entirely forgotten...