conditions may be checking previous values or type mismatch is causing trubles

BMC test of formal properties

Basic functionality is shown in verilator TB

Verilator not compiling, logic not tested

Codestyle improved and comments

Add name conventions for io signals, Solve warnings, refactor TB and launch scripts

Manual changes to Configuration.scala are requiered when changing between simulation or implementation

I have instantiated the pmu step by step and the first problem appear after using the real pmu with non writable registers. With dummy registers it boot. When it manages to boot with the instance of the pmu it throws io_irq_service(): no record