1 Release published by 1 person

• ebmc-5.6

  published May 10, 2025

49 Pull requests merged by 2 people

• SVA-to-Buechi: s_always

  #1131 merged Jun 5, 2025

• word-level BMC: empty sequences

  #1139 merged Jun 5, 2025

• SVA-to-Buechi: sequence repetition operators

  #1130 merged Jun 4, 2025

• Verilog: mark unsized literals

  #1137 merged Jun 4, 2025

• SVA: use from/to instead of lower/upper

  #1128 merged Jun 4, 2025

• SVA-to-Buechi: release/until operators

  #1132 merged Jun 4, 2025

• SVA-to-Buechi: #-# and #=#

  #1129 merged Jun 4, 2025

• SVA-to-Buechi: if

  #1134 merged Jun 4, 2025

• SVA-to-Buechi: eventually

  #1135 merged Jun 4, 2025

• CI: macos-14 -> macos-15

  #1133 merged Jun 4, 2025

• mark a test as broken-smt-backend

  #1136 merged Jun 4, 2025

• SMV: properties must not contain next(...)

  #1140 merged Jun 4, 2025

• Verilog: casts from real to int

  #1138 merged Jun 4, 2025

• SVA/LTL property instrumentation

  #797 merged May 29, 2025

• EBMC: show proof engine in result

  #1127 merged May 28, 2025

• SMV word-level output now prints range types

  #1126 merged May 28, 2025

• signature of show_trans* family of functions

  #1125 merged May 28, 2025

• SMV: rename STRING_Token, QSTRING_Token and QUOTE_Token

  #1124 merged May 28, 2025

• EBMC: include git commit in version

  #1118 merged May 28, 2025

• test for assignment extension and truncation

  #1123 merged May 28, 2025

• test for assignment statement with multiple assignments

  #1122 merged May 28, 2025

• Add a Dockerfile for building and running EBMC

  #1121 merged May 28, 2025

• SVA-to-LTL: sequence and/or

  #1114 merged May 22, 2025

• KNOWNBUG test for Verilog conversions

  #1120 merged May 21, 2025

• SVA-to-LTL: [*n], [*n:m]

  #1111 merged May 21, 2025

• Verilog: `elsif

  #1110 merged May 21, 2025

• Bugfix: use INVAR for SMV word-level in-state invariants

  #1117 merged May 21, 2025

• extract sva_sequence_matcht

  #1116 merged May 21, 2025

• SMV grammar: rename variable_name and qstring_list

  #1119 merged May 21, 2025

• SMV: convert typecasts to SMV

  #1094 merged May 18, 2025

• SVA-to-LTL: refactoring to use vector

  #1112 merged May 18, 2025

• use netlist_boolbvt for the property

  #1102 merged May 15, 2025

• BDD engine: transform SVA to LTL, then LTL to CTL

  #1096 merged May 15, 2025

• introduce sva_boolean_exprt

  #1083 merged May 13, 2025

• bump EBMC version to 5.7 post release

  #1109 merged May 12, 2025

• add a netlist_boolbvt member to convert_trans_to_netlistt

  #1101 merged May 11, 2025

• KNOWNBUG test for implict cast from real to int

  #1105 merged May 11, 2025

• KNOWNBUG test for nettype

  #1107 merged May 11, 2025

• KNOWNBUG test for interconnect

  #1108 merged May 11, 2025

• Bump Ubuntu version in CI release action

  #1106 merged May 10, 2025

• KNOWNBUG test for `elsif

  #1104 merged May 10, 2025

• SVA [*...] for sequence operands

  #1092 merged May 8, 2025

• SMV: introduce classes for extend, resize, signed, unsigned

  #1093 merged May 8, 2025

• implement NNF for SVA s_always

  #1095 merged May 8, 2025

• SMV netlists: use TRUE/FALSE instead of 1/0

  #1097 merged May 8, 2025

• extract SVA_to_LTL(exprt) into a separate file

  #1098 merged May 8, 2025

• extract instantiate_var_mapt into a separate header file

  #1099 merged May 8, 2025

• make the aig_prop_constraintt a member convert_trans_to_netlistt

  #1100 merged May 8, 2025

• fix for no-op assignments during Verilog synthesis

  #1103 merged May 8, 2025

9 Pull requests opened by 1 person

• SMV: bit selection operator

  #1113 opened May 18, 2025

• BMC: completeness thresholds larger than one

  #1115 opened May 18, 2025

• remove `ltl_sva_to_stringt::resultt::e`

  #1141 opened Jun 4, 2025

• SVA-to-Buechi: fix `[+]`

  #1142 opened Jun 5, 2025

• SMV: disallow `next(...)` in `INVAR`

  #1143 opened Jun 5, 2025

• add `sequence_matcht::condition()`

  #1144 opened Jun 5, 2025

• Test for SVA empty match and followed-by operator

  #1145 opened Jun 6, 2025

• fixup i2c_*.sv SVA

  #1146 opened Jun 6, 2025

• NeurIPS 2025 SystemVerilog benchmarks

  #1147 opened Jun 6, 2025

1 Issue closed by 1 person

• invariant violation: unimplemented in boolbv_width.cpp

  #1050 closed May 8, 2025

4 Unresolved conversations

Sometimes conversations happen on old items that aren’t yet closed. Here is a list of all the Issues and Pull Requests with unresolved conversations.

• Verilog: use zero_extend_exprt

  #796 commented on Jun 5, 2025 • 0 new comments

• vlindex: fix parsing for constraint_block

  #924 commented on Jun 2, 2025 • 0 new comments

• SVA monitor

  #1011 commented on May 18, 2025 • 0 new comments

• introduce `verilog_sva_property_typet`

  #1081 commented on Jun 5, 2025 • 0 new comments