- Renaming namespace
AbsKnob
toabsknob
for consistency - Bug fixes in
Ilator
- New
PathUnroller
that takes templatedSmtShim
for broader SMT support - Bug fixes in
smt-switch
interface
- New
SmtShim
to provide a unified interface for both z3 and smt-switch - Update smt-switch interface for their new releases
- New pass
SanityCheckAndFix
for checking instruction set completeness and determinism (hierarchically) - Unify
ExprFuse
andast_fuse
into namespaceasthub
- New pass
SimplifySyntactic
- ILAtor support for initial condition setup using SMT queries
- ILAtor bug fix in cascaded conditional memory update
- Unroller support external interpretation of uninterpreted function
- Redesign expression node hashing (
ExprMngr
)
- New simulator generation (class
ilator
) to optimize compile time and simulation time. - Enrich top-level interface to help unrolling SMT (z3 specifically) of program fragments.
- Misc. utilities (e.g.,
util
andAbsKnob
).
- Support CMake build system for ILAtor generated simulators.
- Performance profiling and improvements.
- Regular maintenance and bug fixes.
- Revamp filesystem utilities with
c++17
features. - Set off (default) the synthesis engine interface for future OS (due to the deprecation of Python2).
- Update CI setups accordingly.
- Regular maintenance, e.g., clean up redundant unit tests and leaving temporary files.
- Include
smt-switch
interface support. - New external library
fmt
for string formatting. - New ILA passes for optimization and simplification.
- Include invariant synthesis support.
- New external project - SMT parser.
- New external project - VCD parser.
- Change numeric of bit-vector constant from
int
touint64_t
- Several improvements on the Verilog parser
- ILA modeling
- Importing from ItSy (synthesized abstraction)
- Importing/exporting ILA portables
- Exporting ILA to Verilog
- Unrolling and exporting ILA to SMT
- Generate verification targets based on the provided refinement relation
- Hard-fix Bison version in Travis CI OS X test since Verilog parser does not build for 3.3.1.
- Re-detect language in LGTM analysis.
- Restructure: move examples to PrincetonUniversity/IMDb.
- Improve code quality and clean up the repository.
- Backward compatibility for z3 below 4.6.0.