diff --git a/fsm-tut4/Makefile b/fsm-tut4/Makefile
new file mode 100644
index 0000000..eb87b90
--- /dev/null
+++ b/fsm-tut4/Makefile
@@ -0,0 +1,61 @@
+SIM_TARGET = build/top
+BIN_TARGET = build/top.bin
+PCF = constraints/iceFUN.pcf
+TIMING = constraints/timing.py
+YOSYS = yosys
+PNR = nextpnr-ice40
+IPACK = icepack
+BURN = iceFUNprog
+SBY = sby
+
+VERILATOR=verilator
+VERILATOR_ROOT ?= $(shell bash -c 'verilator -V|grep VERILATOR_ROOT | head -1 | sed -e "s/^.*=\s*//"')
+VINC := $(VERILATOR_ROOT)/include
+
+RTL_SRC := $(wildcard rtl/*.v)
+SIM_SRC := $(wildcard sim/*.cc)
+FV_SRC := sim/top.sby
+
+BUILD_DIR := ./build
+
+.PHONY: all burn fv clean
+all: $(SIM_TARGET)  $(BIN_TARGET)
+
+# -GWIDTH=5 allows passing parameter to verilog module
+$(BUILD_DIR)/Vtop.cc: $(RTL_SRC)
+	@echo "Running verilator"
+	@mkdir -p $(BUILD_DIR)
+	@$(VERILATOR) --trace -Wall -GWIDTH=10 -cc $^ --top-module top\
+		--Mdir $(BUILD_DIR) --timescale-override 10ns/1ns
+
+$(BUILD_DIR)/Vtop__ALL.a: $(BUILD_DIR)/Vtop.cc
+	@make --no-print-directory -C $(BUILD_DIR) -f Vtop.mk
+
+# std=c++11 flag is needed as of verilator v4.100
+$(SIM_TARGET): $(SIM_SRC) $(BUILD_DIR)/Vtop__ALL.a
+	@echo "Compiling simulation executable"
+	@g++ -I$(VINC) -I$(BUILD_DIR) -std=c++14 $(VINC)/verilated.cpp\
+		$(VINC)/verilated_vcd_c.cpp $^ -o $@
+	@echo "Run simulation with ./$(SIM_TARGET)"
+
+$(BUILD_DIR)/top.json: $(RTL_SRC)
+	@echo "Synthesizing ..."
+	@mkdir -p $(BUILD_DIR)
+	@$(YOSYS) -p "synth_ice40 -top top -json build/top.json" -q $^
+
+$(BIN_TARGET): $(BUILD_DIR)/top.json $(PCF) $(TIMING)
+	@echo "Routing and building binary stream ..."
+	@$(PNR) -r --hx8k --json $< --package cb132 \
+		--asc $(BUILD_DIR)/top.asc --opt-timing --pcf $(PCF) \
+		--pre-pack $(TIMING) -l $(BUILD_DIR)/pnr_report.txt -q 
+	@$(IPACK) $(BUILD_DIR)/top.asc $@
+	@echo "Done!"
+
+burn: $(BIN_TARGET)
+	@$(BURN) $<
+
+fv:
+	@$(SBY) -f $(FV_SRC) -d $(BUILD_DIR)/fv
+
+clean:
+	rm -rf $(BUILD_DIR)
diff --git a/fsm-tut4/constraints/iceFUN.pcf b/fsm-tut4/constraints/iceFUN.pcf
new file mode 100644
index 0000000..7ebdbe7
--- /dev/null
+++ b/fsm-tut4/constraints/iceFUN.pcf
@@ -0,0 +1,14 @@
+# For iceFUN board
+
+set_io --warn-no-port i_clk  	P7
+set_io --warn-no-port i_request 	A5
+
+set_io --warn-no-port o_led_row_0	A12
+set_io --warn-no-port o_led[0] 	C10
+set_io --warn-no-port o_led[1] 	A10
+set_io --warn-no-port o_led[2] 	D7
+set_io --warn-no-port o_led[3] 	D6
+set_io --warn-no-port o_led[4] 	A7
+set_io --warn-no-port o_led[5] 	C7
+# set_io --warn-no-port o_led[6] 	A4
+set_io --warn-no-port o_busy 	C4
diff --git a/fsm-tut4/constraints/timing.py b/fsm-tut4/constraints/timing.py
new file mode 100644
index 0000000..f949a2c
--- /dev/null
+++ b/fsm-tut4/constraints/timing.py
@@ -0,0 +1 @@
+ctx.addClock("i_clk", 100)
diff --git a/fsm-tut4/rtl/clk_gen.v b/fsm-tut4/rtl/clk_gen.v
new file mode 100644
index 0000000..491320f
--- /dev/null
+++ b/fsm-tut4/rtl/clk_gen.v
@@ -0,0 +1,13 @@
+`default_nettype none
+// dummy clock generator, should be replaced by a PLL clock gen eventually
+module clk_gen(
+   input wire i_clk,
+   output wire o_clk
+);
+
+assign o_clk = i_clk;
+
+endmodule
+// Local Variables:
+// verilog-library-directories:(".." "./rtl" ".")
+// End:
diff --git a/fsm-tut4/rtl/top.v b/fsm-tut4/rtl/top.v
new file mode 100644
index 0000000..648478b
--- /dev/null
+++ b/fsm-tut4/rtl/top.v
@@ -0,0 +1,127 @@
+`default_nettype  none
+
+module top(i_clk, o_led, o_led_row_0, i_request, o_busy);
+   parameter WIDTH = 22;
+   input wire i_clk;
+   output wire [5:0] o_led;
+   output wire o_led_row_0;
+   input wire i_request;
+   output wire o_busy;
+
+   wire clk_12MHz;
+
+   clk_gen clk_gen_0 (/*autoinst*/
+      // Outputs
+      .o_clk                 (clk_12MHz),
+      // Inputs
+      .i_clk                 (i_clk));
+
+   reg [WIDTH-1:0] counter;
+   reg [3:0] state;
+   reg [5:0] led_buf; // output buffer, take into account the icefun use active low LED
+   // reg strobe;
+   reg busy_buf;
+   wire req_buf;
+
+   assign o_busy = ~busy_buf;
+   assign o_led = ~led_buf;
+   assign o_led_row_0 = 1'b0;
+   assign req_buf = ~i_request;
+
+   initial begin
+      led_buf = 6'h0;
+      // {strobe, counter} = 0;
+      counter = 0;
+      state = 0;
+      busy_buf = 0;
+   end
+
+   always @(posedge clk_12MHz) begin
+      if (!busy_buf && req_buf)
+         busy_buf <= 1;
+      else
+         busy_buf <= (state != 4'h0);
+   end
+   // counter and strobe run only during busy signal is High
+   always @(posedge clk_12MHz) begin
+      if (busy_buf)
+         counter <= counter + 1'b1;
+         // {strobe, counter} <= counter + 1'b1;
+      else
+         // {strobe, counter} <= 0;
+         counter <= 0;
+   end
+
+   // state change once strobe starts
+   always @(posedge clk_12MHz) begin
+      if (!busy_buf && req_buf)
+         state <= 4'h1;
+      else if (state >= 4'hB)
+         state <= 4'h0;
+      else if (state != 0)
+         state <= state + 1'b1;
+   end
+
+   // fsm for led_buf
+   always @(posedge clk_12MHz) begin
+      // if (strobe)
+         case (state)
+            4'h1: led_buf <= 6'b00_0001;
+            4'h2: led_buf <= 6'b00_0010;
+            4'h3: led_buf <= 6'b00_0100;
+            4'h4: led_buf <= 6'b00_1000;
+            4'h5: led_buf <= 6'b01_0000;
+            4'h6: led_buf <= 6'b10_0000;
+            4'h7: led_buf <= 6'b01_0000;
+            4'h8: led_buf <= 6'b00_1000;
+            4'h9: led_buf <= 6'b00_0100;
+            4'ha: led_buf <= 6'b00_0010;
+            4'hb: led_buf <= 6'b00_0001;
+            default: led_buf <= 6'b00_0000;
+         endcase
+   end
+
+`ifdef	FORMAL
+   // state should never go beyond 13
+	always @(*)
+		assert(state <= 4'hd);
+
+	// I prefix all of the registers (or wires) I use in formal
+	// verification with f_, to distinguish them from the rest of the
+	// project.
+	reg	f_valid_output;
+   always @(*)
+   begin
+      // Determining if the output is valid or not is a rather
+      // complex task--unusual for a typical assertion.  Here, we'll
+      // use f_valid_output and a series of _blocking_ statements
+      // to determine if the output is one of our valid outputs.
+      f_valid_output = 0;
+
+      case(led_buf)
+         8'h01: f_valid_output = 1'b1;
+         8'h02: f_valid_output = 1'b1;
+         8'h04: f_valid_output = 1'b1;
+         8'h08: f_valid_output = 1'b1;
+         8'h10: f_valid_output = 1'b1;
+         8'h20: f_valid_output = 1'b1;
+         8'h40: f_valid_output = 1'b1;
+         8'h80: f_valid_output = 1'b1;
+      endcase
+
+      assert(f_valid_output);
+
+      // SV supports a $onehot function which we could've also used
+      // depending upon your version of Yosys.  This function will
+      // be true if one, and only one, bit in the argument is true.
+      // Hence we might have said
+      // assert($onehot(o_led));
+      // and avoided this case statement entirely.
+   end
+`endif
+
+endmodule
+
+// Local Variables:
+// verilog-library-directories:(".." "./rtl" ".")
+// End:
diff --git a/fsm-tut4/sim/top.cc b/fsm-tut4/sim/top.cc
new file mode 100644
index 0000000..c325842
--- /dev/null
+++ b/fsm-tut4/sim/top.cc
@@ -0,0 +1,60 @@
+#include <stdio.h>
+#include <stdlib.h>
+#include "verilated.h"
+#include "verilated_vcd_c.h"
+#include "Vtop.h"
+
+void	tick(int tickcount, Vtop *tb, VerilatedVcdC* tfp) {
+   tb->eval();
+   if (tfp)
+      tfp->dump(tickcount * 10 - 2);
+   tb->i_clk = 1;
+   tb->eval();
+   if (tfp)
+      tfp->dump(tickcount * 10);
+   tb->i_clk = 0;
+   tb->eval();
+   if (tfp) {
+      tfp->dump(tickcount * 10 + 5);
+      tfp->flush();
+   }
+}
+
+int main(int argc, char **argv) {
+   // Call commandArgs first!
+   Verilated::commandArgs(argc, argv);
+
+   // Instantiate our design
+   Vtop *tb = new Vtop;
+   Verilated::traceEverOn(true);
+   VerilatedVcdC* tfp = new VerilatedVcdC;
+
+   tb->trace(tfp, 99);
+   tfp->open("build/waveform.vcd");
+
+	int	last_led, last_state = 0, state = 0;
+	printf("Initial state is: 0x%02x\n", tb->o_led);
+   unsigned tickcount = 0;
+   last_led = tb->o_led;
+
+   tb->i_request = 1;
+
+   for (int k = 0; k < 4; k++) {
+      tick(++tickcount, tb, tfp);
+   }
+
+   tick(++tickcount, tb, tfp);
+   tb->i_request = 0;
+   tick(++tickcount, tb, tfp);
+   tb->i_request = 1;
+
+   for(int k=0; k<(1 << 16); k++) {
+      tick(++tickcount, tb, tfp);
+
+      // if (last_led != tb->o_led) {
+      // printf("k = %7d, led = %d\n", k, tb->o_led);
+      // }
+
+      last_led = tb->o_led;
+   }
+}
diff --git a/fsm-tut4/sim/top.sby b/fsm-tut4/sim/top.sby
new file mode 100644
index 0000000..3d0b7f6
--- /dev/null
+++ b/fsm-tut4/sim/top.sby
@@ -0,0 +1,13 @@
+[options]
+mode prove
+
+[engines]
+smtbmc
+
+[script]
+read -formal *.v
+prep -top top
+
+[files]
+rtl/top.v
+rtl/clk_gen.v