CHASE 0.4.0

New:

• Words (chase_cps.words): unsigned and signed bit vectors of a fixed
  width, "word[8]" and "signed word[8]", as in nuXmv and SystemVerilog,
  with the arithmetic modulo 2^n. Operators: + - * / mod, the bitwise
  & | xor !, the shifts << >>, the concatenation ::, and the bits
  x[7:0], x[3] (a single bit is a Boolean). A formula whose operands do
  not have the same width and signedness, or a constant that does not fit,
  is refused when the contract is built. The checks give the words to nuXmv;
  the values of the traces are integers. extend(x, n), signed(x), and
  unsigned(x) change the width and the signedness, as in nuXmv. The
  contract algebra works on
  contracts with words: each comparison over words goes to the core library
  as a Boolean variable and comes back after the operation (the results are
  the same as on integers). State machines may declare words. Not in the
  logics language (to_spec) and not for slugs. MCP server: the types
  "word[n]" and "signed word[n]".
• SystemVerilog Assertions (chase_cps.sva): parse_sva reads the
  assume property and assert property statements of a text as a
  contract, with the widths of Verilog, $past and the functions on it,
  sequences of bounded length, disable iff, named properties and
  sequences, and definitions; the statements not read are listed with the
  reason. to_sva writes a contract as a checker module (and a bind
  statement). Packed arrays of several dimensions are words; hierarchical
  names (u1.state) are read as one name (u1__state, mapped back in
  names). The meaning is that of the standard (IEEE 1800-2017, Annex F
  for disable iff), not that of a tool. Tested against a reference
  interpreter of the standard, against Verilator, and against Jasper.
• past(x, n): the value of x n steps before (any value in the first n
  steps), for variables of any type. nuXmv gets it as history variables;
  the contract algebra treats a formula with it as one proposition; slugs
  and the logics language do not take it. parse_sva writes with it the
  comparisons of values two cycles apart or more (y == $past(x, 2)).
• The engine of nuXmv can be chosen: engine="portfolio" (the default),
  "ic3", "bdd", or "bmc", or in the back end, "nuxmv/bdd", as the
  results name it. Command line: --engine. engine="ic3" with NuSMV and
  an unknown engine are refused (before, they ran BDDs).

Changes:

• nuXmv runs IC3 and BDDs at the same time by default (portfolio; before,
  IC3 alone): the first verdict wins. BDDs are much faster than IC3 when a
  counterexample needs a long loop. The verdicts are the same; a
  counterexample may differ from one run to the next, and the one of BDDs
  can be a loop without a prefix.
• MCP server: the tools have the names of the Python functions:
  parse_spec and to_spec replace read_spec and write_spec, and
  parse_sva, to_sva are new.
• mod and xor are keywords of the formulas: they cannot be names.

Fixes:

• Variables named as keywords or functions of nuXmv (count, abs,
  next, init, E, ...) made nuXmv fail with a syntax error; they are
  renamed in the models given to it.
• IC3 of nuXmv 2.2.0 gives wrong answers on formulas with signed() and
  unsigned() (it finds G X (s < signed(x)) -> X G (s < signed(x))
  false); these formulas are checked with BDDs.