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 Ctrl+Enter to execute them. The output of the commands is redirected to the Output tab.
• In batch mode, by passing the script file name or a one-liner script after the -exec: command line parameter.

For batch mode it is often convenient to start Workcraft without GUI and without reading/writing configuration files. This is achieved by using -nogui and -noconfig command line parameter as follows (We presume that Workcraft home is in the search PATH and the platform-specific .sh/.bat extension of Workcraft runner is omitted):

workcraft -nogui -noconfig -exec:'/path/to/script.js'

If a script contains file operation commands, such as loading work files or exporting the models, then all the file names in these commands are relative to the working directory. By default this coincides with Workcraft home, however, an alternative working directory can be passed after the -dir: command line parameter, as follows:

workcraft -nogui -noconfig -exec:script.js -dir:'/working/directory/path/'

since v3.2.3 For a short JavaScript snippet, it may be more convenient to pass it directly in the command line:

workcraft -nogui -exec:'print("Hello!");exit();'

For more information about these and other Workcraft startup options see Command line interface document.

Here is a list of predefined wrapper functions, partitioned into categories, and global variables available for scripting.

• help(substring) – output all the helper functions whose name contains the given substring
• apropos(substring) – output all the helper functions whose name or description contains the given substring
• getHelp(substring, searchDescription) – return a string with all helper functions whose name contains the substring; if the searchDescription is true, then also search the function descriptions

• print(msg) – output msg to stdout and add a newline
• eprint(msg) – output msg to stderr and add a newline
• write(text, fileName) – write text to a file fileName (relative to the working directory) or to stdout if fileName is skipped

Note that conventional Java print functions can be also used, e.g. if you need to output text without adding a newline:

• System.out.print(text) – output text to stdout
• System.err.print(text) – output text to stderr

• startGUI() – start GUI
• stopGUI() – stop GUI and switch to console mode
• quit() or exit() – request Workcraft shutdown after script execution is complete

  Note that quit() and exit() do not terminate Workcraft immediately, and therefore should not be used in the middle of JavaScript program as a way to abort its execution. Instead throw('message') JavaScript statement should be used for this purpose.

• args – command line parameters passed to Workcraft; these can be iterated over as follows: for each (arg in args) {…}
• framework – the Workcraft framework singleton
• workspaceEntry – the current work
• modelEntry – the current model entry, a shortcut to workspaceEntry.getModelEntry()
• visualModel – the current visual model, a shortcut to modelEntry.getVisualModel()
• mathModel – the current math model, a shortcut to modelEntry.getMathModel()

• getWorks() – return an iterable array of loaded works
• getWorkFile(work) – return a file object for the model work
• getModelDescriptor(work) – return a descriptor string for the model work
• getModelTitle(work) – return a title string for the model work
• setModelTitle(work, title) – set a title of the model work to the string title
• closeWork(work) – close the model work
• closeAllWorks() – close all the open works
• setWorkingDirectory(path) – set path as the working directory since v3.3.7
• getWorkingDirectory() – get the working directory since v3.3.7

• load(fileName) – load a model from the work file fileName (or import from external file and determine the model type by the extension) and return its work
• import(fileName) – import a model from the file fileName and return its work (the model type is determined by the fileName extension) deprecated since v3.3.8 in favour of model-specific functions, as import is a reserved keyword in JavaScript ES6
• importCircuitVerilog(vFileName) – import a Circuit from the given Verilog netlist (*.v) file vFileName and return its work since v3.3.8
• importCircuitVerilog(vFileName, topModuleName) – import a Circuit topModuleName (can be skipped for auto detection) with its dependencies from the given Verilog netlist (*.v) file vFileName and return its work since v3.3.9
• importFstSg(sgFileName) – import an FST from the State Graph (*.sg) file sgFileName and return its work since v3.3.8
• importStgG(gFileName) – import an STG from the Signal Transition Graph (*.g) file gFileName and return its work since v3.3.8
• importStgLpn(lpnFileName) – import an STG from the Labeled Petri Net (*.lpn) file lpnFileName and return its work since v3.3.8
• save(work, fileName) – save the model work into a file with the given fileName
• exportSvg(work, fileName) – export the model work as a Scalable Vector Graphics (*.svg) file fileName
• exportPng(work, fileName) – export the model work as a Portable Network Graphics (*.png) file fileName
• exportPdf(work, fileName) – export the model work as a Portable Document Format (*.pdf) file fileName
• exportPs(work, fileName) – export the model work as a PostScript (*.ps) file fileName
• exportEps(work, fileName) – export the model work as an Encapsulated PostScript (*.eps) file fileName
• exportDot(work, fileName) – export the model work as a GraphViz (*.dot) file fileName
• exportStgG(work, fileName) – export the STG work as a Signal Transition Graph (*.g) file fileName
• exportStgLpn(work, fileName) – export the STG work as a Labelled Petri Net (*.lpn) file fileName
• exportFstSg(work, fileName) – export the FST work as a State Graph (*.sg) file fileName
• exportCircuitVerilog(work, fileName) – export the Circuit work as a Verilog netlist (*.v) file fileName
• exportDfsVerilog(work, fileName) – export the DFS work as a Verilog netlist (*.v) file fileName

• setConfigVar(key, val) – set the config variable key to value val
• getConfigVar(key) – return the value of config variable key
• saveConfig() – save settings into the default config file
• loadConfig() – load settings from the default config file

• execFile(fileName) – execute JavaScript file fileName
• runCommand(work, className) – apply the command className to the model work as a background task
• executeCommand(work, className) – apply the command className to the model work and wait for the result

Commands for conversion, transformation and verification of specific models.

These commands are applied to the given work of a specific model type and produce a new model work.

• Conversion between different model types (sorted alphabetically)
  • convertCircuitToStg(work) – convert the Circuit work into a new STG work
  • convertCircuitToStgWithEnvironment(work) – convert the Circuit work and its environment into a new STG work
  • convertDfsToStg(work) – convert the DFS work into a new STG work
  • convertFsmToFst(work) – convert the FSM work into a new FST work
  • convertFsmToGraph(work) – convert the FSM work into a new Graph work
  • convertFsmToPetri(work) – convert the FSM work into a new Petri net work
  • convertFstToFsm(work) – convert the FST work into a new FSM work
  • convertFstToStg(work) – convert the FST work into a new STG work
  • convertGraphToFsm(work) – convert the Graph work into a new FSM work
  • convertGraphToPetri(work) – convert the Graph work into a new Petri net work
  • convertPetriToFsm(work) – convert the Petri net work into a new FSM work
  • convertPetriToPolicy(work) – convert the Petri net work into a new Policy net work
  • convertPetriToStg(work) – convert the Petri net work into a new STG work
  • convertPolicyToPetri(work) – convert the Policy net work into a new Petri net work
  • convertStgToBinaryFst(work) – convert the STG work into a new binary FST work
  • convertStgToFst(work) – convert the STG work into a new FST work
  • convertStgToPetri(work) – convert the STG work into a new Petri net work
  • convertWtgToStg(work) – convert the WTG work into a new STG work

• Conversion of STG and Petri net models using net synthesis of Petrify
  • convertPetriSynthesis(work) – convert the Petri net/STG/FSM/FST work into a new work using net synthesis
  • convertPetriSynthesisEr(work) – convert the Petri net/FSM or STG/FST work into a new Petri net or STG work using net synthesis with a different label for each excitation region
  • convertPetriHideTransition(work) – convert the Petri net/STG work into a new work hiding selected transitions
  • convertPetriHideErTransition(work) – convert the Petri net or STG work into a new Petri net or STG work hiding selected signals and dummies with a different label for each excitation region
  • convertStgUntoggle(work) – convert the STG work into a new work where the selected (or all) transitions are untoggled
  • convertStgHideDummy(work) – convert the STG work into a new work without dummies

These commands are applied to a set of STG works passed as a space-separated list of file names relative to the working directory, and produce a new STG work.

• composeStg(work, data) – compose STGs specified by the space-separated list of work file names data (work parameter is ignored) since v3.3.0

These commands produce a statistics string for the given work of a specific model type.

• statModel(work) – node and arc count for the model work (all model types are supported)
• statPetri(work) – advanced complexity estimates for the Petri net work
• statStg(work) – advanced complexity estimates for the STG work
• statCircuit(work) – advanced complexity estimates for the Circuit work
• statCircuitRefinement(work) – refinement dependencies for the Circuit work since v3.3.8

These commands are applied to the given work of a specific model type and return a new model work.

• Logic synthesis of Circuits from STGs using Petrify backend
  • resolveCscConflictPetrify(work) – resolve complete state coding conflicts in the STG 'work' using Petrify
  • synthComplexGatePetrify(work) – logic synthesis of the STG work into a complex gate Circuit work using Petrify
  • synthGeneralisedCelementPetrify(work) – synthesis of the STG work into a generalised C-element Circuit using Petrify
  • synthStandardCelementPetrify(work) – synthesis of the STG work into a standard C-element Circuit work using Petrify
  • synthTechnologyMappingPetrify(work) – technology mapping of the STG work into a Circuit work using Petrify

• Logic synthesis of Circuits from STGs using MPSat backend
  • resolveCscConflictMpsat(work) – resolve complete state coding conflicts in the STG 'work' using MPSat
  • synthComplexGateMpsat(work) – logic synthesis of the STG work into a complex gate Circuit work using MPSat
  • synthGeneralisedCelementMpsat(work) – synthesis of the STG work into a generalised C-element Circuit work using MPSat
  • synthStandardCelementMpsat(work) – synthesis of the STG work into a standard C-element Circuit work using MPSat
  • synthTechnologyMappingMpsat(work) – technology mapping of the STG work into a Circuit work using MPSat

• Logic synthesis of Circuits from STGs using ATACS backend
  • synthComplexGateAtacs(work) – logic synthesis of the STG work into a complex gate Circuit work using ATACS
  • synthGeneralisedCelementAtacs(work) – synthesis of the STG work into a generalised C-element Circuit work using ATACS
  • synthStandardCelementAtacs(work) – synthesis of the STG work into a standard C-element Circuit work using ATACS

These commands modify the given work of a specific model type.

• layoutModelDot(work) – position nodes and shape the arcs using of the model work using Graphviz backend
• layoutModelRandom(work) – randomly position graph nodes of the model work and connect them by straight arcs
• layoutCircuit(work) – place components and route wires of the Circuit work
• layoutCircuitPlacement(work) – place components of the Circuit work
• layoutCircuitRouting(work) – route wires of the Circuit work

These commands are applied to the given work of a specific model type and return a Boolean outcome of the check.

if (f()) print("pass"); else print("fail");  // PROBLEM: this always prints pass

if (f() == true) print("pass"); else print("fail");

if (f().booleanValue()) print("pass"); else print("fail");

• Commands specific for Circuit models
  • checkCircuitBinateImplementation(work) – check the Circuit work for correct implementation of its binate functions since v3.2.5
  • checkCircuitCombined(work) – combined check of the Circuit work for conformation to environment, deadlock freeness, and output persistency
  • checkCircuitConformation(work) – check the Circuit work for conformation to environment
  • checkCircuitCycles(work) – check if the Circuit work is free from cyclic paths
  • checkCircuitDeadlockFreeness(work) – check the Circuit work for deadlock freeness
  • checkCircuitOutputPersistency(work) – check the Circuit work for output persistency
  • checkCircuitReachAssertion(work, data) – check the Circuit work for REACH assertion data since v3.3.0
  • checkCircuitReset(work) – check if the Circuit work is correctly initialised via forced input ports
  • checkCircuitSignalAssertion(work, data) – check the Circuit work for signal assertion data since v3.3.0
  • checkCircuitStrictImplementation(work) – check the Circuit work for strict implementation of its signals according to the environment

• Commands specific for DFS models
  • checkDfsCombined(work) – combined check of the DFS work for deadlock freeness and output persistency
  • checkDfsDeadlockFreeness(work) – check the DFS work for deadlock freeness
  • checkDfsOutputPersistency(work) – check the DFS work for output persistency

• Commands specific for FSM/FST models
  • checkFsmDeadlockFreeness(work) - check the FSM/FST work for deadlock freeness
  • checkFsmDeterminism(work) - check the FSM/FST work for determinism
  • checkFsmReachability(work) - check the FSM/FST work for reachability of all states
  • checkFsmReversibility(work) - check the FSM/FST work for reversibility of all states

• Commands specific for Graph models
  • checkGraphReachability(work) – check the Graph work for reachability of all its nodes

• Commands specific for Policy net models
  • checkPolicyDeadlockFreeness(work) – check the Policy net work for deadlock freeness

• Commands specific for STG models
  • checkStgCombined(work) – combined check of the STG work for consistency, deadlock freeness, input properness, output persistency, and mutex implementability
  • checkStgConformation(work, data) – check the STG work for conformation to the STG specified by file name data since v3.3.0
  • checkStgConsistency(work) – check the STG work for consistency
  • checkStgCsc(work) – check the STG work for CSC
  • checkStgDeadlockFreeness(work) – check the STG (or Petri net) work for deadlock freeness
  • checkStgDiInterface(work) – check the STG work for DI interface
  • checkStgHandshakeProtocol(work, data) – check the STG work for following a handshake protocol as specified by data, e.g. {req1 req2} {ack12} since v3.3.0
  • checkStgInputProperness(work) – check the STG work for input properness
  • checkStgMutexImplementability(work) – check the STG work for implementability of its mutex places
  • checkStgNormalcy(work) – check the STG work for normalcy
  • checkStgNwayConformation(work, data) – check the STGs specified by space-separated list of file names data for N-way conformation (work parameter is ignored) since v3.2.3, changed v3.3.0
  • checkStgOutputDeterminacy(work) – check the STG work for output determinacy
  • checkStgOutputPersistency(work) – check the STG work for output persistency
  • checkStgPlaceRedundancy(work, data) – check the STG (or Petri net) 'work' for redundancy of places in space-separated list data since v3.3.0
  • checkStgReachAssertion(work, data) – check the STG work for REACH assertion data since v3.3.0
  • checkStgSignalAssertion(work, data) – check the STG work for signal assertion data since v3.3.0
  • checkStgSpotAssertion(work, data) – check the STG work for SPOT assertion data since v3.3.0
  • checkStgUsc(work) – check the STG work for USC

• Commands specific for WTG models
  • checkWtgInputProperness(work) – check the WTG work for input properness
  • checkWtgReachability(work) – check the WTG work for reachability of nodes and transitions
  • checkWtgSoundness(work) – check the WTG work for soundness and consistency
  • checkWtgSynthesisGuidelines(work) – check the WTG work for compliance with the synthesis guidelines

These commands modify the given work of a specific model type.

• Generic commands applicable to all models
  • transformModelCopyLabel(work) – transform the model work by copying unique names of the selected (or all) nodes into their labels
  • transformModelStraightenConnection(work) – transform the model work by straightening selected (or all) arcs

• Commands specific for FSM and derived models
  • transformFsmMergeState(work) – transform the FSM/FST work by merging selected states
  • transformFsmContractState(work) – transform the FSM/FST work by contracting selected states

• Commands specific for generic transformations in Circuit models
  • transformCircuitContractComponent(work) – transform the Circuit work by contracting selected single-input/single-output components
  • transformCircuitContractJoint(work) – transform the Circuit work by contracting selected (or all) joints
  • transformCircuitDetachJoint(work) – transform the Circuit work by detaching selected (or all) joints
  • transformCircuitDissolveJoint(work) – transform the Circuit work by dissolving selected (or all) joints
  • transformCircuitInsertBuffer(work) – transform the Circuit work by inserting buffers into selected wires
  • transformCircuitPropagateInversion(work) – transform the Circuit work by propagating inversion through selected (or all) gates
  • transformCircuitSplitGate(work) – transform the Circuit work by splitting selected (or all) complex gates into simple gates
  • transformCircuitToggleBubble(work) – transform the Circuit work by toggling inversion of selected contacts and outputs of selected components
  • transformCircuitToggleZeroDelay(work) – transform the Circuit work by toggling zero delay of selected inverters and buffers
  • transformCircuitOptimiseZeroDelay(work) – transform the Circuit work by discarding redundant zero delay attribute for selected (or all) inverters and buffers since v3.2.5

• Commands specific for reset insertion in Circuit models since v3.2.2, change in v3.2.3
  • insertCircuitResetActiveHigh(work) – insert active-high reset into the Circuit work
  • insertCircuitResetActiveLow(work) – insert active-low reset into the Circuit work
  • tagCircuitForcedInitAutoAppend(work) – append force init pins as necessary to complete initialisation of the Circuit work
    tagCircuitForceInitAutoAppend(work) before v3.4.0 – deprecated
  • tagCircuitForcedInitAutoDiscard(work) – discard force init pins that are redundant for initialisation of the Circuit work
    tagCircuitForceInitAutoDiscard(work) before v3.4.0 – deprecated
  • tagCircuitForcedInitClearAll(work) – clear all force init input ports and output pins in the Circuit work
    tagCircuitForceInitClearAll(work) before v3.4.0 – deprecated
  • tagCircuitForcedInitInputPorts(work) – force init all input ports in the Circuit work (environment must initialise them)
    tagCircuitForceInitInputPorts(work) before v3.4.0 – deprecated
  • tagCircuitForcedInitProblematicPins(work) – force init output pins with problematic initial state in the Circuit work
    tagCircuitForceInitProblematicPins(work) before v3.4.0 – deprecated
  • tagCircuitForcedInitSequentialPins(work) - force init output pins of sequential gates in the Circuit work
    tagCircuitForceInitSequentialPins(work) before v3.4.0 – deprecated
  • setCircuitDriverInitToOne(work, ref, value) – set value as Init to one attribute for driver ref (input port or output pin) in Circuit work since v3.4.0
  • getCircuitDriverInitToOne(work, ref) – get Init to one attribute for driver ref (input port or output pin) in Circuit work since v3.4.0
  • setCircuitDriverForcedInit(work, ref, value) – set value as Forced init attribute for driver ref (input port or output pin) in Circuit work since v3.4.0
  • getCircuitDriverForcedInit(work, ref) – get Forced init attribute for driver ref (input port or output pin) in Circuit work since v3.4.0
  • constrainCircuitInputPortRiseOnly(work, ref) – constrain input port ref in Circuit work as rise only since v3.4.0
  • constrainCircuitInputPortFallOnly(work, ref) – constrain input port ref in Circuit work as fall only since v3.4.0
  • constrainCircuitInputPortAny(work, ref) – clear constrains from input port ref in Circuit work since v3.4.0
  • getCircuitDriverSetFunction(work, ref) – get Set function of driver ref in Circuit work since v3.4.0
  • getCircuitDriverResetFunction(work, ref) – get Reset function of driver ref in Circuit work since v3.4.0

• Commands specific for loop breaking and scan insertion in Circuit models since v3.2.3
  • insertCircuitScan(work) – insert scan for path breaker components into the Circuit work
  • insertCircuitTestableGates(work) – insert testable buffers/inverters for path breaker components in the Circuit work
  • tagCircuitPathBreakerAutoAppend(work) – append path breaker pins as necessary to complete cycle breaking in the Circuit work
  • tagCircuitPathBreakerAutoDiscard(work) – discard path breaker pins that are redundant for cycle breaking in the Circuit work
  • tagCircuitPathBreakerClearAll(work) – clear all path breaker pins in the Circuit work
  • tagCircuitPathBreakerSelfloopPins(work) – path breaker output pins within self-loops in the Circuit work
  • setCircuitPinPathBreaker(work, ref, value) – set value as Path breaker attribute for pin ref in Circuit work since v3.4.0
  • getCircuitPinPathBreaker(work, ref) – get Path breaker attribute for pin ref in Circuit work since v3.4.0

• Commands specific for DFS models
  • transformDfsContractComponent(work) – transform the DFS work by contracting selected components
  • transformDfsMergeComponent(work) – transform the DFS work by merging selected components
  • transformDfsWagging2Way(work) – transform the DFS work by by applying 2-way wagging to the selected pipeline section
  • transformDfsWagging3Way(work) – transform the DFS work by by applying 3-way wagging to the selected pipeline section
  • transformDfsWagging4Way(work) – transform the DFS work by by applying 4-way wagging to the selected pipeline section

• Commands specific for Petri net and (if explicitly stated) for derived models
  • transformPetriCollapseProxy(work) – transform the Petri net (or derived model, e.g.STG) work by collapsing selected (or all) proxy places
  • transformPetriContractTransition(work) – transform the Petri net work by contracting a selected transition
  • transformPetriDirectedArcToReadArc(work) – transform the Petri net (or derived model, e.g.STG) work by converting selected arcs to read-arcs
  • transformPetriDualArcToReadArc(work) – transform the Petri net (or derived model, e.g.STG) work by converting selected (or all) dual producing/consuming arcs to read-arcs
  • transformPetriMergePlace(work) – transform the Petri net (or derived model, e.g.STG) work by merging selected places
  • transformPetriMergeTransition(work) – transform the Petri net work by merging selected transitions
  • transformPetriProxyDirectedArcPlace(work) – transform the Petri net (or derived model, e.g.STG) work by creating proxies for selected producing/consuming arc places
  • transformPetriProxyReadArcPlace(work) – transform the Petri net (or derived model, e.g.STG) work by creating selected (or all) proxies for read-arc places
  • transformPetriReadArcToDualArc(work) – transform the Petri net (or derived model, e.g.STG) work by converting selected (or all) read-arcs to dual producing/consuming arcs

• Commands specific for Policy net models
  • transformPolicyBundleTransition(work) – transform the Policy net work by bundling selected transitions

• Commands specific for STG models
  • transformStgContractNamedTransition(work) – transform the STG work by contracting a selected transition
  • transformStgDummyToSignalTransition(work) – transform the STG work by converting selected dummies to signal transitions
  • transformStgExpandHandshake(work) – transform the STG work by expanding selected handshake transitions
  • transformStgExpandHandshakeReqAck(work) – transform the STG work by expanding selected handshake transitions by adding _req and _ack suffixes
  • transformStgExplicitPlace(work) – transform the STG work by making selected (or all) places explicit
  • transformStgImplicitPlace(work) – transform the STG work by making selected (or all) places implicit
  • transformStgInsertDummy(work) – transform the STG work by inserting dummies into selected arcs
  • transformStgMergeTransition(work) – transform the STG work by merging selected transitions
  • transformStgMirrorSignal(work) – transform the STG work by mirroring selected (or all) signals
  • transformStgMirrorTransition(work) – transform the STG work by mirroring selected (or all) transition sign
  • transformStgSelectAllSignalTransitions(work) – select all transitions of selected signals in the STG work
  • transformStgSignalToDummyTransition(work) – transform the STG work by converting selected signal transitions to dummies

• Commands specific for WTG models
  • transformWtgStructureWaveform(work) – transform the WTG work by structuring the waveforms

These commands are intended for cross-referencing between work files.

• Commands specific for Circuit models
  • setCircuitEnvironment(work, env) – set env STG file or work as an environment for the Circuit work since v3.2.3
  • getCircuitEnvironment(work) – get an environment STG file for the Circuit work since v3.2.3
  • setCircuitComponentRefinement(work, ref, path) – set path file as refinement for component ref in Circuit work since v3.3.7
  • getCircuitComponentRefinement(work, ref) – get path to refinement file for component ref in Circuit work since v3.3.7

• Commands specific for STG models
  • setStgRefinement(work, path) – set path file as refinement for STG work since v3.3.7
  • getStgRefinement(work) – get path to refinement file for STG work since v3.3.7

stg-transform.js

// Mirror signals and untoggle transitions of STG model
inStgWork = load("in.stg.work");
transformStgMirrorSignal(inStgWork);
outStgWork = convertStgUntoggle(inStgWork);
save(outStgWork, "out.stg.work");
exit();

buck-synth.js

// Complex gate implementation for basic buck controller
stgWork = load("buck.stg.work");
circuitWork = synthComplexGatePetrify(stgWork);
save(circuitWork, "buck.circuit.work");
exportVerilog(circuitWork, "buck.v");
exit();

workspace-info.js

// Print info for each loaded work and convert its title to upper case
for each (work in getWorks()) {
    title = work.getTitle();
    print("Info for " + title);
    print("  * Descriptor: " + getModelDescriptor(work));
    print("  * File: " + getWorkFile(work).getName());
    setModelTitle(work, title.toUpperCase());
    print("  * Title: " + getModelTitle(work);
}

synth.js

// Technology mapping of the specified .g files whose names are passed
// without extension, as follows:
// workcraft -dir:WORKING_DIRECTORY_PATH -exec:synth.js TEST1 TEST2
setConfigVar("CircuitSettings.gateLibrary", "path-to-genlib-file");
for each (name in args) {
    stgWork = import(name + ".g");
    if (stgWork == null) {
        eprint("STG work loading failed!");
        exit();
    }
    if (checkStgCsc(stgWork) == true) {
        cscStgWork = stgWork;
    } else {
        cscStgWork = resolveCscConflictPetrify(stgWork);
        if (cscStgWork == null) {
            eprint("CSC conflict resolution failed!");
            exit();
        }
        save(cscStgWork, "vme-csc.stg.work");
    }
    tmCircuitWork = synthTechnologyMappingMpsat(cscStgWork);
    if (tmCircuitWork == null) {
        eprint("Circuit synthesis failed!");
        exit();
    }
    if (checkCircuitCombined(tmCircuitWork) == true) {
        exportVerilog(tmCircuitWork, name + ".v");
    } else {
        eprint("Circuit verification failed!");
    }
}
exit();

reset.js

// Define circuit initialisation scheme and insert active-low reset
// (requires Workcraft v3.2.3 or newer)
work = load("test-tm.circuit.work");
if (checkCircuitCombined(work) != true) {
    eprint("Circuit verification failed");
    exit();
}
tagCircuitForcedInitClearAll(work);
tagCircuitForcedInitInputPorts(work);
tagCircuitForcedInitAutoAppend(work);
insertCircuitResetActiveLow(work);
if (checkCircuitReset(work) != true) {
    eprint("Circuit cannot be reset to the required initial state");
    exit();
}
if (checkCircuitCombined(work) != true) {
    eprint("Circuit verification failed after reset insertion");
    exit();
}
exportVerilog(work, "test-tm-reset.v");
exit();