CMU CS 15398 - Homework (4 pages)

Previewing page 1 of 4 page document View the full content.
View Full Document

Homework



Previewing page 1 of actual document.

View the full content.
View Full Document
View Full Document

Homework

71 views

Problems/Exams


Pages:
4
School:
Carnegie Mellon University
Course:
Cs 15398 - Introduction to Nanotechnology

Unformatted text preview:

15 398 Bug Catching Automated Program Verification and Testing Homework Assignment October 18 2002 1 The following SMV code models a simple in order pipeline stage Such a pipeline stage is part of all modern microprocessors The instructions of a program are processed as a car in an assembly line The signal that indicates that an instruction moves into the next stage is called update enable signal The instruction in this next stage is overwritten unless it also moves This update enable signal is used as clock signal for the registers of the next stage The module of the stage takes the following parameters The parameter first is set if the stage is the first stage This allows injection of new instructions The parameter prev ue is the update enable i e clock signal of the previous stage The parameter next stall is the stall signal of the next stage The stall signals allow stopping the execution in arbitrary stages A reason for such a stall condition might be slow external memory or in case of the assembly line that a worker dropped his screw driver MODULE simple stage first prev ue next stall VAR full boolean i stall boolean ASSIGN init full first next full prev ue stall first DEFINE 1 ue full stall stall i stall next stall full The module has two state variables the variable full indicates that there is an instruction in the stage If it is not set the stage is empty The variable i stall allows nondeterministic stalls within the stage as described above Describe informally the behavior of one stage 2 The stages can be composed to a five stage pipeline as follows MODULE main VAR stage0 simple stage 1 stage1 simple stage 0 stage2 simple stage 0 stage3 simple stage 0 stage4 simple stage 0 2 0 stage0 ue stage1 ue stage2 ue stage3 ue stage1 stall stage2 stall stage3 stall stage4 stall 0 stage0 f ull stage1 f ull stage2 f ull stage3 f ull stagen f ull Formalize and verify the following properties Liveness Eventually every stage will be clocked i e the update enable signal is



View Full Document

Access the best Study Guides, Lecture Notes and Practice Exams

Loading Unlocking...
Login

Join to view Homework and access 3M+ class-specific study document.

or
We will never post anything without your permission.
Don't have an account?
Sign Up

Join to view Homework and access 3M+ class-specific study document.

or

By creating an account you agree to our Privacy Policy and Terms Of Use

Already a member?