Verification Project

** Course** [02360346]

---

Authors

Name	mail
Raneen Assy	assiranin@campus.technion.ac.il
Tala Saba	tala.saba@campus.technion.ac.il
Wisam arraf	wisamarraf@campus.technion.ac.il

---

Milestone 0

• sw/basics/myDemo.py updated
• in this milestone we updated in the file myDemo the code, and we made it without relying on saving the intermidiate variables on the memory , only on the stack in both question one and two

Milestone 1- CHC-Based Verification

• sw/verify/Milestone1.ipynb updated
  we did our verification function , we only have one problem , we are not sure about the jz and jnz in making of the chcs , because when we did the first
  question from milestone 0 , all of our code ran as we wanted it and we got sat but in the chcs we got on the way false and we dont know why ,we fixed it on the day of submission

Milestone 2-

• sw foldere updated
  In This milestone We implemented the mem_peek and mem_poke functions in the bakend.py file, in addition we wrote a simple code in STAM IR in the sw/compiler/demo_backend.ipynb file which was complied to STAM asm and then we copied this program and demonstarted with the GUI. we draw two simple parallel lines. and filnally we created a new sw/verify/Milestone2-verification.ipynb where we changed the pre and the post condition to match our verification to the asm program that we got.

Milestone 3 -

• In this milestone we imelemented the net_to_smt function in the hw\base\circuit.py file in addition we implemented the create_rules function in the HW\base\verify.ipynb file that generates appropriate horn clauses automatically, these updates are found in the HW file

Milestone 4 - Bootloader-

• bootloader implementation for the "Adder Snake" custom CPU architecture. The bootloader is responsible for loading the OS kernel from an external GPIO device into the system RAM and transferring control to it. This bootloader is written in Python using the hw.cpu.instruction_set framework. It implements a robust handshake protocol to ensure reliable data transmission between the external input device (GPIO) and the CPU, accounting for potential timing differences between the hardware and software. this implementation is in file sw/basics/bootlaoder_prog.py

Memory Layout

The bootloader operates using the following memory map:

Memory Layout

Region	Address	Description
I_ADDR	0x0000	Local storage for the current instruction index ($i$).
GPIO Base	0xc000	Base address for Memory Mapped I/O.
Kernel	0xE800	Destination address where the kernel code is loaded.
EOI	0xFFFF	End-of-Input sentinel value.

GPIO Registers

• GPIO_IN_DATA (0xc000): Input data from the external device.
• GPIO_IN_SEQ (0xc001): Input sequence number (for flow control).
• GPIO_OUT_DATA (0xc002): Output data (used for ACKs).
• GPIO_OUT_SEQ (0xc003): Output sequence number (ACK signal).

Adder Snake Game Kernel

sw/verify/final_snake_game.py This module implements the core game logic for "Adder Snake". It is written in the project's custom assembly language and defines the game state machine, rendering logic, and input handling.

The code is structured into two main instruction lists: MOVE_final (the game loop) and WIN (the victory screen) and LOSE (the losing screen).

Memory Usage (Game Specific)

The game uses specific memory addresses to store state variables and flags:

Address	Variable	Description
0xa000	VRAM Base	Video memory start address.
0xc000	Input	Memory-mapped keyboard input.
0xd000	Head X	Current X coordinate of the snake head.
0xd010	Head Y	Current Y coordinate of the snake head.
0xd100	Length	Current length of the snake.
0xd110	Apple 1 Flag	1 = Active, 0 = Eaten.
0xd120	Apple 2 Flag	1 = Active, 0 = Eaten.
0xd200+	Temp/Tail	Scratchpad for storing old positions/tail coordinates during updates.

Logic Breakdown

1. MOVE_final (Main Game Loop)

This section contains the initialization and the primary state machine, which is divided into two phases (modes).

Initialization

• Draws the initial Snake Head at (8, 8).
• Spawns Apple 1 at (10, 10) and Apple 2 at (5, 10).
• Sets internal flags to indicate both apples are active.

Mode 1: Single-Block Snake

• Logic: The snake consists of just a head.
• Input: Polls address 0xc000 for key codes corresponding to Left (0x4b), Up (0x48), Right (0x4d), and Down (0x50).
• Collision: Checks bounds (1-30). If a wall is hit, the movement is rejected (position restored).
• Objective: Eat Apple 1.
• Transition: When Apple 1 is eaten, the snake length increases to 2, the tail is initialized, and logic jumps to two_wait_for_key.

Mode 2: Two-Block Snake

• Logic: Updates a Head and a Body/Tail segment.
• Movement: Uses a "shift" logic:
  1. Calculates a "Candidate Head" position based on input.
  2. Checks bounds.
  3. If valid: Old Body $\to$ Tail, Old Head $\to$ Body, Candidate $\to$ Head.
• Objective: Eat Apple 2.
• Transition: When Apple 2 is eaten, the game jumps to the won label.

2. WIN (Victory Screen)

This section handles the "Game Won" state.

• Rendering: It executes a sequence of hardcoded loops to manually draw the characters "W - I N" into the VRAM (0xa000 offset).
• Logic: It constructs the letters using pixel-by-pixel block drawing (likely 4x4 or similar block sizes) shifted into the correct VRAM positions.
• Termination: The program ends with a HALT instruction.

Formal Verification: Snake Game (Apple Reachability)

sw/verify/verify_snake.py

This module formally verifies that the Snake game logic allows for a state where both apples have been eaten. Unlike standard testing, which tries random inputs, this uses the Z3 Theorem Prover to mathematically prove that a sequence of inputs exists to reach this state.

1. Verification Goal

The goal is to prove reachability of the following memory state:

• Apple 1 Flag (0xd110) == 0 (Eaten)
• AND
• Apple 2 Flag (0xd120) == 0 (Eaten)

We do not verify the "Win Screen" display logic, only that the game state correctly registers both apples as consumed.

2. Technical Approach

Symbolic Input Tape

The game relies on an infinite loop (wait1_for_key) that reads from a memory-mapped keyboard address (0xc000).

• Problem: A static analysis would see this as an infinite loop and hang.
• Solution: We model 0xc000 as an Input Oracle. We create a symbolic array input_tape and a cursor input_cursor. Every time the CPU reads 0xc000, it gets the next symbolic value from the tape. The solver is free to choose any sequence of keystrokes to satisfy the goal.

Instruction Flattening

The Python game code uses nested lists (macros) for operations like ADD and SHL.

• Preprocessing: The script recursively flattens these nested lists into a linear instruction sequence.
• Label Resolution: It scans the flattened list to resolve string labels (e.g., 'move1_left') into concrete Program Counter (PC) indices.

Z3 Constraints (CHCs)

We generate Constrained Horn Clauses (CHCs) for every instruction:

• Transitions: Implies(State_at_i, State_at_i+1)
• Goal: We assert that reaching a state where both apple flags are 0 implies False.
  • Implies( (State_at_i AND Mem[Apple1]==0 AND Mem[Apple2]==0), False )

3. Interpreting the Output

When you run verify_snake.py, you will see one of two results:

RESULT: UNSAT (Success)

• Meaning: The solver found a contradiction in the claim "It is impossible to eat both apples."
• Conclusion: The game is winnable. There exists a valid sequence of keystrokes that results in both apples being eaten.

RESULT: SAT (Failure)

• Meaning: The solver satisfied the claim "It is impossible to eat both apples."
• Conclusion: The game is unwinnable. The solver proved that no matter what keys are pressed, the snake can never eat both apples (e.g., due to a wall collision or bug in the logic).

4. How to Run

Ensure z3-solver is installed (pip install z3-solver) and run:

python verify_snake.py

Examples and demonstrations

• in the correct_boarder_behavior.mp4 you can see that the snake is not getting out of the boarders of the memory and it stays in place
• in the correct_two_blocks_movement.mp4 you can see the correct movement of the snake after becoming two blocks.
• in the transition_to_two_blocks.mp4 you can see the one blocked snake becoming two blocks after eating the first apple
• in the verification_output.png you can see the output after running the verify_snake.py
• in the WIN.jpeg you can see the Win that is demonstarted on the screen when the two apples are eaten
• in the LOSE.jpeg you can see a lose demonstartion on the screen although we dont have a lose state in our game (just for the fun we decided to do that :) )