Verilog Synthesis and Formal Verification with Yosys