CPU Verification Lab

Due Date: May 14; Last Updated Date: Apr 30

Table of Contents

• Overview: Formally Verify the PSP
  • Your Verification Task
  • Code Structure
• Part 1: Get Familiar with the Starter Code
  • Part 1A: Specification Code (20%)
  • Part 1B: Implementation Code (5%)
  • Part 1C: Verification Code (10%)
• Part 2: Find the Adder Bug (5%)
• Part 3: Find the Backdoor Instruction
  • Simplications on the Original PSP Processor
  • Part 3A: Add Exceptions in the Specification (20%)
  • Part 3B: Find the Backdoor Instruction (40%)

Lab Details

Collaboration Policy

Our full Academic Honesty policy can be found on the Course Information page of our website. As a reminder, all 6.5950/6.5951 labs should be completed individually. You may discuss the lab at a high level with a classmate, but you may not work on code together or share any of your code.

Getting Started

This lab could be run on our lab machine unicorn.csail.mit.edu. Log in with the same user account as previous labs.

Alternatively, you can use the docker file provided in the starter code to run the lab locally. Instructions to run the docker are provided here.

Overview: Formally Verify the PSP

In the Fuzzing Lab, you have been playing with the buggy Pretty Secure Processor and found the ALU bug and the backdoor instruction. In this lab, you will try to find them again with another approach – Model Checking – as you have learned from the Formal Verification Recitation. Hope you will have a better understanding and comparison of fuzzing and formal verification.

Finish the Recitation First!

If you have not finished the Formal Verification Recitation, stop continuing on the lab and finish the Recitation first! The recitation is basically a simpler version of the lab and gets you familiar with the whole verification framework. A solution to the recitation has been provided on Piazza.

Your Verification Task

As explained in the “The Big Picture” Section of the Recitation, the basic idea of formal verification is to check the implementation matches the specification under all possible inputs to the hardware. In this lab, the 3 key components of this task are:

• Implementation: Verilog source code of the PSP Processor.
• Specification: (A small portion of) RISC-V ISA definition.
• Covering all possible inputs: Use Rosette, a symbolic execution framework.

Code Structure

You will gradually write the code to achieve this verification task. Here is an overview of the starter code structure, which is similar to the code structure in the Recitation. We will guide you through the starter code in Part 1 of this lab.

|-- core_to_verify         # System Verilog code of PSP
|   |-- ...
|   `-- core_to_verify.sv  # Top module
|
|-- scripts
|   |-- sv2rkt.sh          # Convert System Verilog to Rosette
|   |-- yosys_command.ys   # yosys commands used by `sv2rkt.sh`
|   `-- verify.sh          # Run the verification
|
|-- generated_src
|   `-- core_to_verify.rkt # Rosette code generated through `sv2rkt.sh`
|
`-- src           # Contain all verification code
    |-- param     # Parameters like instructions encodings
    |   `-- ...
    |-- array     # Functions operating on register arrays
    |   `-- ...
    |-- impl.rkt  # Functions to simulate the implementation
    |-- spec.rkt  # Functions to simulate the specification
    `-- veri.rkt  # Simulate the impl and spec and verify they match

Part 1: Get Familiar with the Starter Code

The processor you will verify this time will be more complex than the one in the Recitation. It could be hard to directly jump into the implementation part of the processor. So, let’s start by looking at the specification. The specification is used to represent how architecture states should be updated by each instruction. It does not need to reflect how long (i.e. how many cycles) an instruction should take in a real (pipelined / Out-of-Order) processor and we can just write a specification that executes 1 instruction per cycle for convenience.

Part 1A: Specification Code (20%)

We will look at spec.rkt and the 3 files it requires (i.e., imports), array/rf.rkt, array/imem.rkt, and param/inst.rkt in this part. The following exercises and discussions are designed to help you understand them.

Run a Test Program

1-1 Exercise

The main function of the spec.rkt file (i.e., the last line in it) contains a single function call to the testMe function. Run the spec.rkt file with racket src/spec.rkt command from the root folder in the terminal. Check the terminal output.

Broken Environment

In case the command above returns -bash: racket: command not found on unicorn, try source /knox/envSetup.sh to set environment variables. (This should not happen normally because this source command should be run automatically when you log in.)

The code you just ran initializes an instance of the specification data structure and simulates it by 5 cycles. The states of the specification are printed out at each cycle. You will be asked to explain this output along with the source code of testMe function in the following discussion question.

HINT: Rosette Libraries

Forget the meaning of a built-in function? You can:

• Check the “Learn Rosette Syntax” Section from the Recitation for basic keywords/functions including define, struct, bitvector, vector, printf, branch and loops.
• Search the function in Racket’s official document page, by putting the function name into the search box at the left-top corner. If you find multiple searched results, use the function “provided from /rosette/…”.

1-2 Discussion Question

1. Which function is called to initialize the variable spec? What is the data type of this variable?
2. What are the instructions stored in the initial instruction memory? How about the initial content of the data memory and register file? (Hint: find the file where init-debug-imem, init-zero-dmem, and init-zero-rf are defined.)
3. Move on to the simulation of spec. The function step-spec! is called to simulate it by 1 cycle. In this function, what is the function spec-pc doing?
4. The function inst-rd is defined in param/inst.rkt. What is it doing? (Hint: extract is a built-in function you could search in the Racket’s official document page)
5. In the starter code of step-spec!, what instruction has already been supported?

Now you should have a general idea about what spec.rkt is doing. Read through the file and confirm you understand the 5 key functions it defines, summarized in the table below. They will be used during the verification.

Support 4 More Instructions

Now that you have been familiar with the starter code of the specification, let’s extend it a little bit to test your understanding.

1-3 Exercise

Following the pattern of how step-spec! executes LUI instruction, extend it to support ADDI, SRLI, ADD, and BEQ instructions. Some helper functions to decode instructions are provided in param/inst.rkt.

You could test your code by updating the init-debug-imem function in array/imem.rkt to include these new instructions, and run it with racket src/spec.rkt from the root folder (where you will run all the rest commands in this lab) in the terminal.

HINT: ISA Definitions

Please refer to ISA Specification, starting at Page 18, for the detailed explanation of each instruction. A summary of these instructions is on Page 130.

If you are confused by what (assume #f) is doing in the else case of the cond block, don’t worry, you do not need to change it in this exercise, and we will talk about it later.

Part 1B: Implementation Code (5%)

Writing the specification code above is nothing more than writing a normal program, but in our newly learned Rosette language. In this part, however, you will explore more power of the framework and simulate the Verilog code cycle by cycle.

Most of the implementation code is automatically generated by the yosys+knox you have used in the “From RTL to Rosette” Section of Recitation. As you have seen in the Exercise 1 of the Recitation, this automatically generated code provides interface functions to initialize the state of a Verilog module, simulate it, and extract the output from it. The impl.rkt file uses these interface functions to define 5 functions for our verification (, which are similar to the functions defined in the spec.rkt file):

All these functions are provided in the file impl.rkt. You do not need to fully understand how these functions are implemented and only need to know how to use them. Specifically, you will run a testMe function in it to see how a Verilog module is simulated with a concrete instruction memory.

1-4 Exercise

Generate the .rkt file (i.e., generated_src/core_to_verify.rkt) from the System Verilog files by running ./scripts/sv2rkt.sh.

Run the impl.rkt file with racket src/impl.rkt command. Check the terminal output.

1-5 Discussion Question

Check the output of racket src/impl.rkt and answer: After simulating how many cycles did you observe the first and the second instructions being committed? Could you explain the reason for these two cycle numbers based on the micro-architecture of the pretty secure processor?

If you are curious about how these functions are implemented, feel free to read through the impl.rkt file. There are many comments to explain the code. They are implemented with two key ideas in mind:

• To simulate the pipeline of the processor, it uses the interface functions provided by the generated code from the yosys+knox toolchain. This is similar to how we simulate the Tiny CPU in the Recitation.
• It also simulates the interaction between the pipeline and the instruction/data memory. The memory takes 1 cycle to return the data: At cycle 0, it saves the inputs to a buffer register; At cycle 1, it returns the data.

Part 1C: Verification Code (10%)

Finally, we will start to do the verification! We will help you understand the veri.rkt file. It uses the 5 key functions from spec.rkt and the 5 from impl.rkt that you should already be familiar with. It also requires (i.e., imports) a small configuration file param/veri.rkt that will be explained later.

Verify a Concrete Test Program

Normally, we want to verify the specification and implementation match under any initial state of the instruction memory. This requires us to initialize the instruction memory with symbolic values (with the function init-sym-imem in array/imem.rkt). However, this might be inconvenient for us to debug or just to learn the code. Thus, let’s first try to run the framework with a concrete initial instruction memory, which essentially means we want to verify the specification and implementation match under a concrete program. We provide a simple variable in param/veri.rkt, the param-imem-type to determine whether to use symbolic or concrete initial instruction memory. Let’s start by setting the variable to “concrete” first.

1-6 Exercise

Change the param-imem-type variable in param/veri.rkt to “concrete” and run the veri.rkt file with racket src/veri.rkt.

You should see “No Counterexample” at the end of the terminal output. If not, it means the specification and the implementation mismatch when running the program returned by the init-debug-imem function in array/imem.rkt – You probably did Exercise 1-3 incorrectly.

Now, let me ask you a few questions to help you understand the output and the source code (i.e., the testMe function in veri.rkt). But before that, let me remind you of a few build-in functions for the verification in Rosette (that you will see in veri.rkt):

1-7 Discussion Question

1. When executing the line of code (verify (simu imem dmem #f)) in veri.rkt, what are the assertions generated?
2. In the for loop of function simu, the implementation and specification are simulated in a “synchronized” manner. What could go wrong if we just simulate both of them by 1 cycle in each loop iteration, without changing other code?

Test on Finding a Counterexample

It is not essentially fun to see no counterexample found. After all, we try to find bugs with our framework in the lab. So, let’s manually create a mismatch between the specification and the implementation and see how will the framework react.

1-8 Exercise

Go to the step-spec! function in spec.rkt and look at the code that executes the LUI instruction. Let’s change the line (write-rf! rf rd imm-U) to (write-rf! rf rd (bv 0 32)) and then run racket src/veri.rkt again.

Now, our specification and implementation will definitely mismatch because the specification is not executing the LUI instruction correctly. Let’s look at the terminal output and see how the framework figures out this mismatch.

Here is how the code in veri.rkt works:

• Line (define sol (verify (simu imem dmem #f))) simulates the specification and implementation. At the end of the simulation, it queries the SMT solver and finds a solution that contains a counterexample.
• Line (set! imem (evaluate imem sol)) looks into the counterexample in the sol and finds the concrete value of the instruction memory that triggers the assertion false. It updates the variable imem with this concrete value. (For now, this concrete imem is just the one you define in array/imem.rkt.)
• Line (simu imem dmem #t) simulates the specification and implementation again with this concrete instruction memory. It will print out a trace to show the counterexample.

1-9 Discussion Question

Check the terminal output and answer: after finishing simulating which cycle does the implementation and specification start to mismatch on the architectural state? What is the mismatch? Why do we have this mismatch?

Find a Counterexample with Symbolic Initial Instruction Memory

Now, let’s change the initial state of the instruction memory to symbolic value and release the full power of our framework.

1-10 Exercise

Change the param-imem-type variable in param/veri.rkt to “sym” and run racket src/veri.rkt.

1-11 Discussion Question

This time, what instruction triggers the mismatch in the architectural state at which cycle?

Debug with Concrete imem

Whenever your code does not work properly later in this lab, with symbolic initial instructions, you can always switch back to concrete initial instructions for debugging.

Constraint the Search Space

You might face a small trouble in investigating the counterexample in the last run: the concrete instruction is executing on a register whose index is quite large. However, our terminal only prints out the registers with index 0, 1, 2, and 3, due to the space limit. To see the value stored in this register with a large index, we have to adjust the printing function to include the specific register in the printings.

It could be annoying to do this for every new counterexample. We provide a convenient configuration variable to solve this problem: The param-limit-space in param/veri.rkt can be used to limit the search space of the solver by only considering the register file accesses whose indexes are within [0, 3] and memory requests whose addresses are within [0x0, 0x1f]. Let’s try it.

1-12 Exercise

Change the param-limit-space variable in param/veri.rkt to #t and run racket src/veri.rkt. We will keep it to #t for the rest of the lab.

Now, you should be able to see the counterexample uses a register with a smaller index and the state mismatch can be easily checked from the terminal printout.

Assumptions and Assertions

The param-limit-space configuration you just tried is no more than achieving a small engineering trick to help us debug. However, we want to bring your attention to how it is implemented, which will reveal a more fundamental concept in the formal verification – Constraining the search space with Assumptions.

You have already been familiar with the assertions, right? Basically, whenever you want to check a property, you assert it. Assumptions, on the other hand, have also been used in the code base a few times without being fully explained to you. Let’s take one example you just used to explain it. Check out the write-rf! function in array/rf.rkt. The assume is called to assume the higher 3 bits of the register index (i.e., pos) is always zero. You have just benefited from this assumption in a way that the counterexample generated only uses a register whose index is within [0, 3]. Here is a summary of how assumptions work:

• During the symbolic simulation, all expressions being assumed by the assume function are collected, in the same way the assertions are collected.
• When querying the SMT solver, instead of just asking the SMT solver to find a counterexample violating the assertions, we now ask for a counterexample, i.e., a concrete instance of instruction memory, that satisfies all assumptions but still violates some assertions.

In our example, the assumption in this write-rf! function makes sure the program in the counterexample will not use a register with larger indexes. Assumptions help us constrain the search space for those symbolic values.

Another place where you have been benefiting from assumption is the step-spec! function in the spec.rkt file. When an instruction type has not been supported (i.e., in the else case of the cond block), we use (assume #f). This makes sure programs using unsupported instructions will not be considered (as a counterexample).

HINT: Use assume!

If you could have a good understanding of assume and take advantage of it later in the lab, it could save you a lot of coding efforts while finding the same bug you are asked for.

1-13 Exercise

Go to the step-spec! function in spec.rkt and look at the code that executes the LUI instruction. Change the line (write-rf! rf rd (bv 0 32)) back to (write-rf! rf rd imm-U), run racket src/veri.rkt, and you should see “no counterexample found”.

Now, you are ready to go with real challenges!

Grading

The only code that we will grade for this part is Exercise 1-3. Other exercises are helping you to understand the framework and answer the discussion questions. The discussion questions will be graded.

Part 2: Find the Adder Bug (5%)

It is rather simple to find the adder bug after we have built up the framework. In fact, we already have all the code required to find this bug. The only thing you need to do in this part is to ask the model checker to check for more cycles.

Bounded Model Checking

We are doing a bounded model checking here, which means we only simulate the implementation for a bounded number of cycles and check whether the mismatch happens within this number of cycles. When it passes the check, it does not mean the implementation is fully correct and more bugs might be found when increasing the number of the bound. The number of the bound in our code base is defined in param/veri.rkt by the variable param-simuCycle.

2-1 Exercise

Increase the value of param-simuCycle in param/veri.rkt and redo the verification, until you could find the adder bug. (You might want to have a minimal param-simuCycle, so your counterexample showing the bug will also be short.)

2-2 Discussion

Describe the adder bug you found here.

Grading

The exercise in this part will not be graded, and only the discussion question will be graded.

Part 3: Find the Backdoor Instruction

Honestly, you have merely written any code so far in this lab, but just exploring the capability of the starter code. But now, it’s your turn to do some work.

Recall in the Fuzzing Lab, the backdoor instruction is an instruction with illegal encoding. Based on the specification, this illegal instruction should cause an exception. However, the implementation does something different – it is executed as a nop or even silently changes the privilege level. In this part, you will try to describe the behavior of illegal instructions (i.e., causing exceptions) in the specification and automatically find that a backdoor instruction mismatches this behavior. For simplicity, you do not have to find when this backdoor instruction will change the privilege level.

Simplications on the Original PSP Processor

The original PSP processor supports tens of instructions as well as many CSRs. It could be tedious for you to implement all of them in the specification. So we have simplified the Verilog code of the PSP processor and we list a summary of it:

• Only support 10 instructions: LUI, BEQ, LW, SW, ADDI, SRLI, ADD, ECALL, CSRRW, and MRET. The encodings of these instructions have been provided in param/inst.rkt. But you need to check the ISA Specifications for the expected behavior for each of them.

• Only support 3 CSRs: mtvec, mepc, and mpp. They are all zero after reset. Recall we have explained these CSRs here. Writing to any other CSRs will have no effect and reading from any other CSRs will return 0. Writing or reading to any other CSRs also will not check the privilege level or trigger exceptions.

• Only support 2 privilege levels: User Mode and Machine Mode. A 2-bit register stores the mode: 0 as User Mode and 3 as Machine Mode. The processor is in the Machine Mode after reset.

• When loading from or storing to an address that is misaligned (i.e., lower 2 bits are not zero), treat it as if the address is aligned (i.e., pretend the lower 2 bits are zero). This is the case for both instruction and data memories.

Part 3A: Add Exceptions in the Specification (20%)

The first step is to specify the behavior of Exceptions in the specification. The expected behavior of exceptions can be complex when many CSRs are involved. Thankfully, we only need to support 3 CSRs. Instead of pointing you to the official document of exceptions, which contains many CSR names that might scare you, here is a short summary of the expected behavior of exceptions in our simplified processor:

• Store the current pc to mepc and jump to the location stored in mtvec.
• Store the current (zero-extended-to-32-bit) privilege level to mpp and set the privilege level to Machine Mode.
• The current instruction will not be committed.

3-1 Exercise

Look at the step-spec! function in spec.rkt. When having an illegal (or currently unsupported) instruction, instead of doing (assume #f), trigger the exception as described above. Some CSR-related codes are provided in array/csr.rkt.

Test your code by adding an illegal (or currently unsupported) instruction to the init-debug-imem function in array/imem.rkt, run racket src/spec.rkt, and check the output.

Part 3B: Find the Backdoor Instruction (40%)

Only adding the exception is unlikely to be enough to find the backdoor instruction because our specification has not matched the implementation yet – it only supports 5 out of 10 instructions. But this might still be a good time to just go and try the verification, and to see what we can find. Try to run the verification with racket src/veri.rkt. What have you observed? You probably will see the same adder bug!

Assume the Adder Bug is not Triggered

It actually can be annoying during the formal verification that even if the design has many bugs, the formal verification framework might only be able to find one of them. This happens because as long as a program uses the add instruction and triggers the bug, it will cause the assertion to be false. The SMT solver will just become lazy and stop exploring other possible violations of the assertions.

One normal solution is just fixing the existing bugs – No one wants so many bugs lying in the code base. However, sometimes, it would also be nice to find multiple bugs and do the fix together. We could achieve so by adding an (assume #f) on the execution path triggering the bug.

3-2 Exercise

Go to the step-spec! function in spec.rkt. Add an (assume #f) to the path executing the ADD and ADDI instructions.

Then run racket src/veri.rkt and you should see no counterexample found (with the minimal param-simuCycle that gave you the adder bug).

Find the Backdoor Instruction, Finally

Now is the final time to find the backdoor instruction.

3-3 Exercise

Increase the value of param-simuCycle in param/veri.rkt and redo the verification, until you can find a counterexample generated by the solver.

If lucky enough, you might directly find the backdoor instruction even without changing the code. Then you could just skip the following Exercise 3-4. (Though we still hope you could try it a bit.)

Otherwise, you will find one of the 10 legal instructions (listed here) will trigger the assertion false – it will trigger an exception on the specification (because we have not supported it yet) while executing normally on the implementation. In this case, you need to add the support of this legal instruction and try the verification again until you can find the backdoor instruction.

3-4 Exercise

In the specification, gradually add the support of the legal instructions that trigger the assertion false until you can find the backdoor instruction. If needed, you could change the spec-archState and impl-archState functions to include CSRs and the Privilege level and check whether they match.

3-5 Discussion

What is the backdoor instruction you found? Take a screenshot of the terminal output at the cycle when this backdoor instruction is committed and include it in the report.

Reproducibility

Unless you support all 10 instructions, we might not be able to reproduce your result because the SMT solver might just decide to find a different counterexample when we run it. This is fine as long as you have the screenshot! However, we do encourage you to support more instructions.

3-6 Discussion

Based on your experience in lab6.A and lab6.B, how would you compare the pros and cons of fuzzing and formal verification techniques?

Grading

For Exercise 3-1/2/3, please finish them by following the instructions. For Exercise 3-4 you will get a full grade as long as you show the correct backdoor instruction being found through the screenshot in Discussion 3-5.

That’s All, Folks!

That’s all we have for you this semester. Congrats on completing Secure Hardware Design!! We sincerely hope you enjoyed this class and found the labs to be worthwhile.

If there’s anything we can do to improve the course for future students, please let us know! (Anonymous feedback here.)

Have a great summer!

Acknowledgements

Made by Yuheng Yang.