Remove gitignore from alu folder; added link to Yosys

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.
+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.

alu/.gitignore

@@ -1 +0,0 @@
-*/work/*

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