diff --git a/README.md b/README.md
index cd1b1e8..95bdf64 100644
--- a/README.md
+++ b/README.md
@@ -1,6 +1,6 @@
 # formal_verification
 
-Tests and examples of using formal verification to check correctness of digital hardware designs. All tests are done with SymbiYosys, a free formal verification tool based on Yosys. Some examples use the VHDL/SystemVerilog parser plugin by Verific which isn't free SW and nit included in the free Yosys version. See on the [Symbiotic EDA website](https://www.symbioticeda.com) for more information. 
+Tests and examples of using formal verification to check correctness of digital hardware designs. All tests are done with SymbiYosys, a front-end for formal verification flows based on [Yosys](https://github.com/YosysHQ). Some examples use the VHDL/SystemVerilog parser plugin by Verific which isn't free SW and not included in the free Yosys version. See on the [Symbiotic EDA website](https://www.symbioticeda.com) for more information. 
 
 ### alu
-A simple ALU design in VHDL, together with a formal testbench written in SystemVerilog. The testbench contains various simple properties for assert & cover directives which are proved with the SymbiYosys tool.
\ No newline at end of file
+A simple ALU design in VHDL, together with a formal testbench written in SystemVerilog. The testbench contains various simple SVA properties used by assert & cover directives which are proved with the SymbiYosys tool.
diff --git a/alu/.gitignore b/alu/.gitignore
deleted file mode 100644
index 26ad522..0000000
--- a/alu/.gitignore
+++ /dev/null
@@ -1 +0,0 @@
-*/work/*
\ No newline at end of file
diff --git a/alu/Makefile b/alu/Makefile
index b6df3b0..d1c6b73 100644
--- a/alu/Makefile
+++ b/alu/Makefile
@@ -1,2 +1,2 @@
-alu: alu.vhd alu_t.v alu_f.sby
+alu: alu.vhd alu_t.sv alu_f.sby
 	sby -f -d work alu_f.sby