http://workcraft.org/ 2026-04-11T10:26:22+00:00 http://workcraft.org/ http://workcraft.org/_media/logo.svg text/html 2017-03-06T14:54:39+00:00 Anonymous (anonymous@undisclosed.example.com) http://workcraft.org/help/assertion?rev=1488812079&do=diff Assertion language Assertions can be specified similar to System Verilog syntax, e.g. !(req1 && ack2) -- declare that req1 and ack2 signals are never high at the same time. The following logical operators are currently supported, in the order of increasing precedence: text/html 2020-06-12T02:42:44+00:00 Anonymous (anonymous@undisclosed.example.com) http://workcraft.org/help/boolean_expression?rev=1591929764&do=diff Boolean expressions The Boolean expressions are employed in the following plugins: * Conditional Partial Order Graph -- to specify the graph conditions * Digital Circuit -- to specify set/reset functions of circuit components. Workcraft recognises the following fairly standard syntax for the Boolean expressions: text/html 2024-12-18T15:08:31+00:00 Anonymous (anonymous@undisclosed.example.com) http://workcraft.org/help/cli?rev=1734534511&do=diff Command line interface Workcraft command line usage is as follows workcraft [OPTIONS] [FILES] * OPTIONS -- space-separated list of the following options: * -dir:DIR -- path to the working directory * -config:CONFIG -- user config file (default is global text/html 2020-12-17T09:59:05+00:00 Anonymous (anonymous@undisclosed.example.com) http://workcraft.org/help/genlib?rev=1608199145&do=diff SIS Genlib Synthesis backend tools Petrify and MPSat use SIS Genlib format to specify gate library for technology mapping. Detailed specification of the format can be found in [SIS Genlib format documentation]. Automated conversion from popular gate libraries is also possible, e.g.     text/html 2024-12-17T14:26:37+00:00 Anonymous (anonymous@undisclosed.example.com) http://workcraft.org/help/reach?rev=1734445597&do=diff REACH language The language REACH is used for specifying reachability properties. Using a language for specifying properties has the following advantages: * Custom properties can be easily and concisely specified. * The user does not have to modify the model in any way, in particular the model does not have to be translated into an input language of some model checker. text/html 2025-08-06T07:32:13+00:00 Anonymous (anonymous@undisclosed.example.com) http://workcraft.org/help/scripting?rev=1754465533&do=diff Scripting interface Workcraft supports scripting using JavaScript language. Two modes of script execution are supported: * Interactively, by entering the script commands in the Javascript tab and pressing to execute them. The output of the commands is redirected to the text/html 2024-11-15T13:08:58+00:00 Anonymous (anonymous@undisclosed.example.com) http://workcraft.org/help/start?rev=1731676138&do=diff Help * Tips and tricks Workcraft interface * Main window * New work dialog * Main menu * Model tools * Tool controls * Property editor * Global preferences Model plugins * Petri Net * Signal Transition Graph * Digital Circuit * Dataflow Structure * Waveform Transition Graph * Conditional Partial Order Graph * xMAS Circuit * Structured Occurrence Net Advanced topics * Reach language * Verification properties * Circuit synthesis * Backend tools option… text/html 2020-04-01T16:51:00+00:00 Anonymous (anonymous@undisclosed.example.com) http://workcraft.org/help/synthesis?rev=1585759860&do=diff Circuit synthesis This is a comparative analysis of Petrify and MPSat approaches to synthesis of speed-independent circuits. Representation of the state space The number of reachable states is generally exponential in the size of the STG, which is a fundamental problem known as        text/html 2022-08-24T12:05:27+00:00 Anonymous (anonymous@undisclosed.example.com) http://workcraft.org/help/verification?rev=1661342727&do=diff Verification properties STG properties Most STGs should satisfy the following properties (can be checked via Verification menu): * Consistency -- for all signals z, z+ and z- must alternate in each possible trace, always starting with the same sign. This is necessary for the encodings of the reachable states to be binary. text/html 2024-09-02T11:32:32+00:00 Anonymous (anonymous@undisclosed.example.com) http://workcraft.org/help/virtualbox?rev=1725276752&do=diff Installing Workcraft in VirtualBox This guide shows how to run Workcraft in a VirtualBox Ubuntu guest OS. Here are a couple of reasons for such a decision: * Your OS is not fully compatible with Workcraft, e.g. due to a lack of 32-bit support as found in more recent versions of OSX (such as Catalina and newer) or;