|
| 1 | +# EBMC 5.1 |
| 2 | + |
| 3 | +* SVA abort properties and disable iff |
| 4 | +* $countones |
| 5 | +* fix for SVA 'and' and 'or', and sequence implication |
| 6 | +* SystemVerilog: compound blocking assignments |
| 7 | +* SystemVerilog: endmodule identifiers |
| 8 | +* SMV: fix for arithmetic on range types that start from non-zero |
| 9 | +* SMV: CTL operators AR, ER, AU, EU |
| 10 | + |
| 11 | +# EBMC 5.0 |
| 12 | + |
| 13 | +* Major revision of the SystemVerilog frontend, extending the support for SVA |
| 14 | +* CTL model checking with BDDs |
| 15 | +* Added a Homebrew formula |
| 16 | +* WASM build |
| 17 | +* Fix for AIG-based engine |
| 18 | +* SystemVerilog: $low, $high, $increment, $left, $right |
| 19 | +* SystemVerilog: $stable, $rose, $fell, $changed, $past |
| 20 | +* SystemVerilog named properties |
| 21 | +* SystemVerilog: fix for always_comb |
| 22 | +* SystemVerilog: size casts |
| 23 | +* SystemVerilog: cover properties |
| 24 | +* SystemVerilog: enums |
| 25 | +* SystemVerilog: added all integer types |
| 26 | +* Verilog: parameter ports |
| 27 | +* --json-modules |
| 28 | +* structs, unions |
| 29 | +* SVA followed-by operators, SVA if, indexed nexttime |
| 30 | +* random trace generation |
| 31 | +* SMV identifier syntax fix |
| 32 | +* SMV: LTLSPEC |
0 commit comments