Summer Formal 2011,Jason Baumgartner www.research.ibm.com/sixthsense IBM Corporation,Hardware Verification,Homework and Lab,Homework 1: Netlist Modeling Exercises,1.1) Properties are specially annotated as “outputs“ in the AIGER format. However, there are no special ways to annotate “constraints“. How may the netlist be manipulated to allow constraints be reflected in an AIGER netlist?,assume (busy not req_valid),Homework 1: Netlist Modeling Exercises,1.2) Latches are assumed to have constant-0 initial value in the AIGER format. Assume you wish to initialize a set of latches to an arbitrary one-hot state: i.e., exactly one of them will be active at any point in time. How may this be represented in the netlist?,0 0 0,assertable?,Homework 1: Netlist Modeling Exercises,1.3) Certain types of logic functions such as multipliers are very difficult to reason about using bit-level algorithms. “Uninterpreted functions“ are sometimes used to facilitate the verification of designs with such functions, wherein two instances of a particular function (e.g., one in the implementation and one in a reference model) are replaced with nondeterministic behavior. In particular, these two instances are each replaced by a multiplexor: if the arguments to the abstracted functions are identical, the same nondeterminstic values are sensitized through both multiplexors. Otherwise, different nondeterminstic values are sensisized through. Uninterpreted functions are useful when the correctness of the verification task is not dependent upon the precise values produced from the abstracted functions; only the *consistency* of identical results being produced under identical arguments is relevant. When verifying sequential netlists, a challenge with using uninterpreted functions is that the function pairs to be abstracted may be receive their arguments at different points in time. I.e., the implementation may be pipelined hence the timing with which it receives relevant arguments may not match the un-pipelined reference model. How could one model a precise “sequentially consistent“ uninterpreted function to cope with this? Comment on the size of the resulting implementation with respect to the width of the abstracted function. Could you think of lossy yet “sound“ shortcuts which are of smaller sizes and retain sequential consistency?,Homework 1: Netlist Modeling Exercises,1.4) Recall that “liveness checking” may be reduced to “safety checking” through a netlist transformation, which entails adding a “shadow register” for every register in the original netlist against which a state-repetition i.e. lasso loop may be detected. Consider checking a liveness property of the form: every request eventually gets a grant. A single assertion net may be synthesized which remembers that a request has occurred and is awaiting a grant hence the liveness check consists of checking whether this assertion net may stick at logical 1 forever. Work through the exercise of how to convert this overall check to safety, e.g. how to model the shadow registers, to end up with an AIGER-style safety assertion net capturing all liveness failures of the above. Liveness checking often also entails fairness constraints, which are logical conditions which must hold “infinitely often” along any counterexample trace. Consider a set of fairness constraints expressed as nets which assert to 1 when they are satisfied used to qualify the liveness check. Work through the exercise of how to support fairness constraints in the above modeling.,Homework 2: Algorithmic Exercises,2.1) Netlist Modeling Exercises #2 asks for a way to reflect constraints without a dedicated netlist construct. Can you think of drawbacks of this modeling in simulation and semi-formal verification frameworks? Can you think of potential drawbacks to such an approach in various verification frameworks such as induction and redundancy removal? Can you think of algorithmic ways to compensate for such a modeling if desired?,0 1 0,assertable?,Stimulus Generator,Homework 2: Algorithmic Exercises,2.2) Redundancy removal, which identifies and eliminates pairs of gates which are equivalent in all reachable states, is a powerful simplification technique capable of dramatically reducing overall verification resources (i.e., through simplifying the netlist for a subsequent proof technique), if not outright solving many intricate verification problems. In cases, a netlist may have pairs of gates which are equivalent only after several time-frames from the desired initial state set. Can you think of several ways to try to exploit this condition, i.e. to attain the desired reduction while strictly (or at least, conservatively) preserving property checking? E.g., ways to alternatively model a testbench; an automated transformation to accomplish something similar; a type of invariant which may capture the desired information?,Homework 2: Algorithmic Exercises,2.3) Reachability analysis may