Add BMC verification

[alexandertepaev]

No description provided.

[alexandertepaev]

Hi @lou1306. This PR adds possibility to do the model checking using BMC (probably a draft, feel free to build upon it).
When BMC verification is invoked, the user is asked to provide a BMC bound (or simply hit enter, in this case bound is defaulted to 20).
If we need tests, pls let me know where/which/how.

[lou1306]

Thank you! Made a few slight changes: now I just use the pre-existing formatting function, and I call msat_check_ltlspec_bmc in the backend instead of check_ltlspec_ic3. This should be the "best" command when the model is compiled with go_msat. As I mentioned in the commit, sadly the nuXmv "API" is not the cleanest!

Anyway, it looks good enough for a merge now.

[lou1306]

• I do not think we need a separate formatting function, the one we used for IC3 should still work
• I think msat_check_ltlspec_bmc should be called instead of check_ltlspec_bmc.

Apart from this, the PR looks solid!