Yosys 0.21

Yosys 0.20 .. Yosys 0.21

• New commands and options

  • Added "formalff" pass - transforms FFs for formal verification
  • Added option "-formal" to "memory_map" pass
  • Added option "-witness" to "rename" - give public names to all signals
    present in yosys witness traces
  • Added option "-hdlname" to "sim" pass - preserves hiearachy when writing
    simulation output for a flattened design
  • Addded option "-scramble-name" to "rename" pass

• Formal Verification

  • Added $anyinit cell to directly represent FFs with an unconstrained
    initialization value. These can be generated by the new formalff pass.
  • New JSON based yosys witness format for formal verification traces.
  • yosys-smtbmc: Reading and writing of yosys witness traces.
  • write_smt2: Emit inline metadata to support yosys witness trace.
  • yosys-witness is a new tool to inspect and convert yosys witness traces.
  • write_aiger: Option to write a map file for yosys witness trace
    conversion.
  • yosys-witness: Conversion from and to AIGER witness traces.

• Verific support

  • Filename re-writing support for "verific" pass.

• Various

  • ABC performance improvements
  • Filename re-writing added for "show -lib".

• SmartFusion2 support

  • Added $alu support
  • Added SYSRESET and XTLOSC cells
  • Compatible now with LiberoSoc flow