Release Notes

1.1.4 - 2020-09-29

Updates

  • Renaming namespace AbsKnob to absknob for consistency

  • Bug fixes in Ilator

1.1.3 - 2020-08-24

Updates

  • New PathUnroller that takes templated SmtShim for broader SMT support

  • Bug fixes in smt-switch interface

1.1.2 - 2020-07-20

Updates

  • 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 and ast_fuse into namespace asthub

1.1.1 - 2020-07-14

Updates

  • 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)

1.1.0 - 2020-07-08

Updates

  • 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 and AbsKnob).

1.0.5 - 2020-06-18

Updates

  • Support CMake build system for ILAtor generated simulators.

  • Performance profiling and improvements.

  • Regular maintenance and bug fixes.

1.0.4 - 2020-06-17

Updates

  • 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.

1.0.3 - 2020-06-02

Updates

  • Include smt-switch interface support.

  • New external library fmt for string formatting.

  • New ILA passes for optimization and simplification.

1.0.2 - 2020-01-09

Updates

  • Include invariant synthesis support.

  • New external project - SMT parser.

  • New external project - VCD parser.

1.0.1 - 2019-11-01

Updates

  • Change numeric of bit-vector constant from int to uint64_t

  • Several improvements on the Verilog parser

1.0.0 - 2019-09-18

Updates

  • 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

0.9.0 - 2019-02-05 (pre-release if v1.0.0)

Updates

  • 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.

PreviousDevelopment

Last updated