User Tools

Site Tools


Workcraft v3.3.4 (2021-05-21)

Usability improvements

  • Reuse of open workspace entries when loading models – this makes unsaved changes in environment/refinement models visible to verification commands
  • Restore highlights in Output tab after applying global preferences

Model and tool plugins

  • Digital Circuit plugin
    • Enhanced support two Mutex protocols: Late (previously Strict) and Early (previously Relaxed)
      • Add user-defined suffix for MUTEX cells with Late and Early protocols
      • Include two flavours of MUTEX cell into the library presets
      • Distinguish Late and Early MUTEX cell on Verilog import
    • Refresh set/reset functions on contact inversion
    • Refactor Scan and Reset insertion so they change the model only if needed
    • Fix conformation check for mutex whose outputs are not exposed
    • Fix simulation tool for highlighting suggested components
  • Signal Transition Graph plugin
    • Improvements for N-way conformation check
      • Composition trace for N-way conformation is extended with component violation events
      • Use projected composition events in Table and List views
    • Enhanced verification of mutex place implementability
      • Add Mutex protocol property to enable fine-grain tuning of mutex places
      • When syntactically detecting mutex requests, exclude grants from the set of triggers
    • Fix detection of place redundancy in presence of read arcs
    • Fix handling of replica (i.e. proxy) places in transition contraction
    • Fix undo/redo functionality when changing signal type via model-level property

Fixes and technical stuff

  • Update of UnfoldingTools backend
    • MPSat can now build unfolding prefix and supports LTL-X verification
    • MPSat's command line parameters have changed significantly to enable the above
    • Punf is phased out, as all its functionality is now available in MPSat
    • Fix technology mapping into libraries without C-elements
    • Fix PComp's storing of place and transition correspondence in XML formal when one of signal phases is absent in the composition and so a transition in a component STG has no corresponding transitions in the composition.
  • Update toolchain to Gradle v7.0.2, PMD v6.34, Checkstyle v8.42
Copyright © 2014-2024

Donate Powered by PHP Valid HTML5 Valid CSS Driven by DokuWiki