Avoid using terminology with "formal" for SymbiYosys

[nmigen-issue-migration]

Issue by whitequark
Thursday Aug 15, 2019 at 02:59 GMT
Originally opened as m-labs/nmigen#171

---

Although Yosys calls it "formal verification", industry calls it "static functional verification", and I (coming from software) would call it "model checking with a SAT solver" or "property testing". Kami would be true "formal verification".

Privately, I expressed this concern for confusion with Yosys developers and they agree, so I think nMigen should be more careful in its use of "formal" also.

This affects 0.1 as we have nmigen.formal which needs to be renamed.

[nmigen-issue-migration]

Comment by whitequark
Monday Aug 19, 2019 at 20:24 GMT

---

Renamed to nmigen.asserts, because that module contains Assert, Assume and related items. Essentially, I am calling it "nMigen Assertions", similar to "SystemVerilog Assertions" aka SVA.