ILAng Versions Save

• Renaming Absknob to absknob
• Ilator bug fix

• New PathUnroller that takes templated SmtShim 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 and ast_fuse into namespace asthub

• 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 SystemC simulator generator for larger-scaled ILA models.
• More utilities for program fragment unrolling.

• Support CMake build system for ILAtor generated simulators.
• Performance profiling and improvements.
• Regular maintenance and bug fixes.

The first release of ILAng. Including

• 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

This pre-release is meant for a checkpoint as published in the TACAS19 paper. There should only be minor differences (no additional key feature supports) w.r.t. the coming v1.0.0 release.