Workcraft supports scripting using JavaScript language. Two modes of script execution are supported:
-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 substringapropos(substring) – output all the helper functions whose name or description contains the given substringgetHelp(substring, searchDescription) – return a string with all helper functions whose name contains the substring; if the searchDescription is true, then also search the function descriptionsprint(msg) – output msg to stdout and add a newlineeprint(msg) – output msg to stderr and add a newlinewrite(text, fileName) – write text to a file fileName (relative to the working directory) or to stdout if fileName is skippedNote 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 stdoutSystem.err.print(text) – output text to stderrstartGUI() – start GUIstopGUI() – stop GUI and switch to console modequit() 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 singletonworkspaceEntry – 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 worksgetWorkFile(work) – return a file object for the model workgetModelDescriptor(work) – return a descriptor string for the model workgetModelTitle(work) – return a title string for the model worksetModelTitle(work, title) – set a title of the model work to the string titlecloseWork(work) – close the model workcloseAllWorks() – close all the open workssetWorkingDirectory(path) – set path as the working directory since v3.3.7getWorkingDirectory() – get the working directory since v3.3.7select(ref, …) – select the nodes passed as a list of references since v3.5.1load(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 workimport(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 ES6importCircuitVerilog(vFileName) – import a Circuit from the given Verilog netlist (*.v) file vFileName and return its work since v3.3.8importCircuitVerilog(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.9importFstSg(sgFileName) – import an FST from the State Graph (*.sg) file sgFileName and return its work since v3.3.8importStgG(gFileName) – import an STG from the Signal Transition Graph (*.g) file gFileName and return its work since v3.3.8importStgLpn(lpnFileName) – import an STG from the Labeled Petri Net (*.lpn) file lpnFileName and return its work since v3.3.8save(work, fileName) – save the model work into a file with the given fileNameexportSvg(work, fileName) – export the model work as a Scalable Vector Graphics (*.svg) file fileNameexportPng(work, fileName) – export the model work as a Portable Network Graphics (*.png) file fileNameexportPdf(work, fileName) – export the model work as a Portable Document Format (*.pdf) file fileNameexportPs(work, fileName) – export the model work as a PostScript (*.ps) file fileNameexportEps(work, fileName) – export the model work as an Encapsulated PostScript (*.eps) file fileNameexportDot(work, fileName) – export the model work as a GraphViz (*.dot) file fileNameexportStgG(work, fileName) – export the STG work as a Signal Transition Graph (*.g) file fileNameexportStgLpn(work, fileName) – export the STG work as a Labelled Petri Net (*.lpn) file fileNameexportFstSg(work, fileName) – export the FST work as a State Graph (*.sg) file fileNameexportCircuitVerilog(work, fileName) – export the Circuit work as a Verilog netlist (*.v) file fileNameexportDfsVerilog(work, fileName) – export the DFS work as a Verilog netlist (*.v) file fileNamesetConfigVar(key, val) – set the config variable key to value valgetConfigVar(key) – return the value of config variable keysaveConfig() – save settings into the default config fileloadConfig() – load settings from the default config file
Config variables are saved in config.xml file (located under ~/.config/workcraft/ in Linux or ~\AppData\Roaming\workcraft\ in Windows). The variable name you pass to setConfigVar/getConfigVar functions can be derived from config.xml file and should include its dot-separated path in the XML tree. For example, setConfigVar("CircuitSettings.clearPin", "RN"); sets the variable clearPin under CircuitSettings group to a string RN.
execFile(fileName) – execute JavaScript file fileNamerunCommand(work, className) – apply the command className to the model work as a background taskexecuteCommand(work, className) – apply the command className to the model work and wait for the resultCommands 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.
convertCircuitToStg(work) – convert the Circuit work into a new STG workconvertCircuitToStgWithEnvironment(work) – convert the Circuit work and its environment into a new STG workconvertDfsToStg(work) – convert the DFS work into a new STG workconvertFsmToFst(work) – convert the FSM work into a new FST workconvertFsmToGraph(work) – convert the FSM work into a new Graph workconvertFsmToPetri(work) – convert the FSM work into a new Petri net workconvertFstToFsm(work) – convert the FST work into a new FSM workconvertFstToStg(work) – convert the FST work into a new STG workconvertGraphToFsm(work) – convert the Graph work into a new FSM workconvertGraphToPetri(work) – convert the Graph work into a new Petri net workconvertPetriToFsm(work) – convert the Petri net work into a new FSM workconvertPetriToPolicy(work) – convert the Petri net work into a new Policy net workconvertPetriToStg(work) – convert the Petri net work into a new STG workconvertPolicyToPetri(work) – convert the Policy net work into a new Petri net workconvertStgToBinaryFst(work) – convert the STG work into a new binary FST workconvertStgToFst(work) – convert the STG work into a new FST workconvertStgToPetri(work) – convert the STG work into a new Petri net workconvertWtgToStg(work) – convert the WTG work into a new STG workconvertPetriSynthesis(work) – convert the Petri net/STG/FSM/FST work into a new work using net synthesisconvertPetriSynthesisEr(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 regionconvertPetriHideTransition(work) – convert the Petri net/STG work into a new work hiding selected transitionsconvertPetriHideErTransition(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 regionconvertStgUntoggle(work) – convert the STG work into a new work where the selected (or all) transitions are untoggledconvertStgHideDummy(work) – convert the STG work into a new work without dummiesThese 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 workstatStg(work) – advanced complexity estimates for the STG workstatCircuit(work) – advanced complexity estimates for the Circuit workstatCircuitRefinement(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.
resolveCscConflictPetrify(work) – resolve complete state coding conflicts in the STG work using PetrifysynthComplexGatePetrify(work) – logic synthesis of the STG work into a complex gate Circuit work using PetrifysynthGeneralisedCelementPetrify(work) – synthesis of the STG work into a generalised C-element Circuit using PetrifysynthStandardCelementPetrify(work) – synthesis of the STG work into a standard C-element Circuit work using PetrifysynthTechnologyMappingPetrify(work) – technology mapping of the STG work into a Circuit work using PetrifyresolveCscConflictMpsat(work) – resolve complete state coding conflicts in the STG work using MPSatsynthComplexGateMpsat(work) – logic synthesis of the STG work into a complex gate Circuit work using MPSatsynthGeneralisedCelementMpsat(work) – synthesis of the STG work into a generalised C-element Circuit work using MPSatsynthStandardCelementMpsat(work) – synthesis of the STG work into a standard C-element Circuit work using MPSatsynthTechnologyMappingMpsat(work) – technology mapping of the STG work into a Circuit work using MPSatsynthComplexGateAtacs(work) – logic synthesis of the STG work into a complex gate Circuit work using ATACSsynthGeneralisedCelementAtacs(work) – synthesis of the STG work into a generalised C-element Circuit work using ATACSsynthStandardCelementAtacs(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 backendlayoutModelRandom(work) – randomly position graph nodes of the model work and connect them by straight arcslayoutCircuit(work) – place components and route wires of the Circuit worklayoutCircuitPlacement(work) – place components of the Circuit worklayoutCircuitRouting(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.
Note that the result of verification commands is of object Boolean type (with capital B), as opposed to primitive boolean type (with small b). In addition to the conventional true and false values, Boolean may also evaluate to null (e.g. when verification command is not applicable to the supplied model).
Care should be taken when handling Boolean values in JavaScript – they cannot be directly used in logic expressions. For example, consider function 'f()' that returns a Boolean.
The following code snippet would always print pass, because the Boolean value is implicitly converted into a non-empty string ("true", "false" or "null"), which always evaluates to boolean true:
if (f()) print("pass"); else print("fail"); // PROBLEM: this always prints pass
Instead, an explicit comparison to the expected boolean value should be used, thus forcing the cast of Boolean into boolean (instead of string) for subsequent comparison:
if (f() == true) print("pass"); else print("fail");
A cleaner way to encode logic expressions is to explicitly convert the value into boolean by using booleanValue() method of Boolean type (this code would throw an exception if the result of f() is not Boolean or the returned value is null):
if (f().booleanValue()) print("pass"); else print("fail");
checkCircuitBinateImplementation(work) – check the Circuit work for correct implementation of its binate functions since v3.2.5checkCircuitCombined(work) – combined check of the Circuit work for all essential properties (conformation to environment, output persistency, deadlock freeness)checkCircuitConformation(work) – check the Circuit work for conformation to environmentcheckCircuitCycles(work) – check if the Circuit work is free from cyclic pathscheckCircuitDeadlockFreeness(work) – check the Circuit work for deadlock freenesscheckCircuitOutputPersistency(work) – check the Circuit work for output persistencycheckCircuitReachAssertion(work, data) – check the Circuit work for REACH assertion data since v3.3.0checkCircuitReset(work) – check if the Circuit work is correctly initialised via forced input portscheckCircuitSignalAssertion(work, data) – check the Circuit work for signal assertion data since v3.3.0checkCircuitStrictImplementation(work) – check the Circuit work for strict implementation of its signals according to the environmentcheckDfsCombined(work) – combined check of the DFS work for deadlock freeness and output persistencycheckDfsDeadlockFreeness(work) – check the DFS work for deadlock freenesscheckDfsOutputPersistency(work) – check the DFS work for output persistencycheckFsmDeadlockFreeness(work) - check the FSM/FST work for deadlock freenesscheckFsmDeterminism(work) - check the FSM/FST work for determinismcheckFsmReachability(work) - check the FSM/FST work for reachability of all statescheckFsmReversibility(work) - check the FSM/FST work for reversibility of all statescheckGraphReachability(work) – check the Graph work for reachability of all its nodes checkPolicyDeadlockFreeness(work) – check the Policy net work for deadlock freenesscheckStgCombined(work) – combined check of the STG work for all essential properties (consistency, output determinacy, input properness, mutex protocol, output persistency, absence of local self-triggering, deadlock freeness, delay insensitive interface)checkStgConformation(work, data) – check the STG work for conformation to the STG specified by file name data since v3.3.0checkStgConsistency(work) – check the STG work for consistencycheckStgCsc(work) – check the STG work for CSCcheckStgDeadlockFreeness(work) – check the STG (or Petri net) work for deadlock freenesscheckStgDiInterface(work) – check the STG work for delay insensitive interfacecheckStgHandshakeProtocol(work, data) – check the STG work for following a handshake protocol as specified by data, e.g. {req1 req2} {ack12} since v3.3.0checkStgInputProperness(work) – check the STG work for input propernesscheckStgLocalSelfTriggering(work) – check the STG work for absence of local self-triggeringcheckStgMutexImplementability(work) – check the STG work for implementability of its mutex placescheckStgNormalcy(work) – check the STG work for normalcycheckStgNwayConformation(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.0checkStgOutputDeterminacy(work) – check the STG work for output determinacycheckStgOutputPersistency(work) – check the STG work for output persistencycheckStgPlaceRedundancy(work, data) – check the STG (or Petri net) work for redundancy of places in space-separated list data since v3.3.0checkStgReachAssertion(work, data) – check the STG work for REACH assertion data since v3.3.0checkStgSignalAssertion(work, data) – check the STG work for signal assertion data since v3.3.0checkStgSpotAssertion(work, data) – check the STG work for SPOT assertion data since v3.3.0checkStgUsc(work) – check the STG work for USCcheckWtgInputProperness(work) – check the WTG work for input propernesscheckWtgReachability(work) – check the WTG work for reachability of nodes and transitionscheckWtgSoundness(work) – check the WTG work for soundness and consistencycheckWtgSynthesisGuidelines(work) – check the WTG work for compliance with the synthesis guidelines
These commands modify the given work of a specific model type.
transformModelAnonymise(work) – anonymise the model work by randomly renaming its nodestransformModelCopyLabel(work) – transform the model work by copying unique names of the selected (or all) nodes into their labelstransformModelStraightenConnection(work) – transform the model work by straightening selected (or all) arcstransformFsmMergeState(work) – transform the FSM/FST work by merging selected statestransformFsmContractState(work) – transform the FSM/FST work by contracting selected statestransformCircuitContractComponent(work) – transform the Circuit work by contracting selected single-input/single-output componentstransformCircuitContractJoint(work) – transform the Circuit work by contracting selected (or all) jointstransformCircuitDetachJoint(work) – transform the Circuit work by detaching selected (or all) jointstransformCircuitDissolveJoint(work) – transform the Circuit work by dissolving selected (or all) jointstransformCircuitInsertBuffer(work) – transform the Circuit work by inserting buffers into selected wirestransformCircuitPropagateInversion(work) – transform the Circuit work by propagating inversion through selected (or all) gatestransformCircuitSplitGate(work) – transform the Circuit work by splitting selected (or all) complex gates into simple gatestransformCircuitToggleBubble(work) – transform the Circuit work by toggling inversion of selected contacts and outputs of selected componentstransformCircuitToggleZeroDelay(work) – transform the Circuit work by toggling zero delay of selected inverters and bufferstransformCircuitOptimiseZeroDelay(work) – transform the Circuit work by discarding redundant zero delay attribute for selected (or all) inverters and buffers since v3.2.5transformCircuitMutexProtocolEarly(work) – transform the Circuit work by setting early protocol for selected (or all) mutex components since v3.5.1transformCircuitMutexProtocolLate(work) – transform the Circuit work by setting late protocol for selected (or all) mutex components since v3.5.1insertCircuitResetActiveHigh(work) – insert active-high reset into the Circuit workinsertCircuitResetActiveLow(work) – insert active-low reset into the Circuit worktagCircuitForcedInitAutoAppend(work) – append force init pins as necessary to complete initialisation of the Circuit worktagCircuitForcedInitAutoDiscard(work) – discard force init pins that are redundant for initialisation of the Circuit worktagCircuitForcedInitClearAll(work) – clear all force init input ports and output pins in the Circuit worktagCircuitForcedInitInputPorts(work) – force init all input ports in the Circuit work (environment must initialise them)tagCircuitForcedInitProblematicPins(work) – force init output pins with problematic initial state in the Circuit worktagCircuitForcedInitSequentialPins(work) - force init output pins of sequential gates in the Circuit worksetCircuitDriverInitToOne(work, ref, value) – set value as Init to one attribute for driver ref (input port or output pin) in Circuit work since v3.4.0getCircuitDriverInitToOne(work, ref) – get Init to one attribute for driver ref (input port or output pin) in Circuit work since v3.4.0setCircuitDriverForcedInit(work, ref, value) – set value as Forced init attribute for driver ref (input port or output pin) in Circuit work since v3.4.0getCircuitDriverForcedInit(work, ref) – get Forced init attribute for driver ref (input port or output pin) in Circuit work since v3.4.0constrainCircuitInputPortRiseOnly(work, ref) – constrain input port ref in Circuit work as rise only since v3.4.0constrainCircuitInputPortFallOnly(work, ref) – constrain input port ref in Circuit work as fall only since v3.4.0constrainCircuitInputPortAny(work, ref) – clear constrains from input port ref in Circuit work since v3.4.0getCircuitDriverSetFunction(work, ref) – get Set function of driver ref in Circuit work since v3.4.0getCircuitDriverResetFunction(work, ref) – get Reset function of driver ref in Circuit work since v3.4.0insertCircuitScan(work) – insert scan for path breaker components into the Circuit workinsertCircuitTestableGates(work) – insert testable buffers/inverters for path breaker components in the Circuit worktagCircuitPathBreakerAutoAppend(work) – append path breaker pins as necessary to complete cycle breaking in the Circuit worktagCircuitPathBreakerAutoDiscard(work) – discard path breaker pins that are redundant for cycle breaking in the Circuit worktagCircuitPathBreakerClearAll(work) – clear all path breaker pins in the Circuit worktagCircuitPathBreakerSelfloopPins(work) – path breaker output pins within self-loops in the Circuit worksetCircuitPinPathBreaker(work, ref, value) – set value as Path breaker attribute for pin ref in Circuit work since v3.4.0getCircuitPinPathBreaker(work, ref) – get Path breaker attribute for pin ref in Circuit work since v3.4.0transformDfsContractComponent(work) – transform the DFS work by contracting selected componentstransformDfsMergeComponent(work) – transform the DFS work by merging selected componentstransformDfsSplitComponent(work) – transform the DFS work by splitting selected components since v3.5.2transformDfsWagging2Way(work) – transform the DFS work by applying 2-way wagging to the selected pipeline sectiontransformDfsWagging3Way(work) – transform the DFS work by applying 3-way wagging to the selected pipeline sectiontransformDfsWagging4Way(work) – transform the DFS work by applying 4-way wagging to the selected pipeline sectiontransformFsmContractState(work) – transform the FSM/FST work by contracting selected statestransformFsmSplitState(work) – transform the FSM/FST work by splitting selected states since v3.5.2(work) – transform the FSM/FST work by merging selected statestransformPetriCollapseProxy(work) – transform the Petri net (or derived model, e.g.STG) work by collapsing selected (or all) proxy placestransformPetriContractTransition(work) – transform the Petri net work by contracting a selected transitiontransformPetriDirectedArcToReadArc(work) – transform the Petri net (or derived model, e.g.STG) work by converting selected arcs to read-arcstransformPetriDualArcToReadArc(work) – transform the Petri net (or derived model, e.g.STG) work by converting selected (or all) dual producing/consuming arcs to read-arcstransformPetriMergePlace(work) – transform the Petri net (or derived model, e.g.STG) work by merging selected placestransformPetriMergeTransition(work) – transform the Petri net work by merging selected transitionstransformPetriProxyDirectedArcPlace(work) – transform the Petri net (or derived model, e.g.STG) work by creating proxies for selected producing/consuming arc placestransformPetriProxyReadArcPlace(work) – transform the Petri net (or derived model, e.g.STG) work by creating selected (or all) proxies for read-arc placestransformPetriReadArcToDualArc(work) – transform the Petri net (or derived model, e.g.STG) work by converting selected (or all) read-arcs to dual producing/consuming arcstransformPolicyBundleTransition(work) – transform the Policy net work by bundling selected transitionstransformStgContractNamedTransition(work) – transform the STG work by contracting a selected transitiontransformStgDummyToSignalTransition(work) – transform the STG work by converting selected dummies to signal transitionstransformStgExpandHandshake(work) – transform the STG work by expanding selected handshake transitionstransformStgExpandHandshakeReqAck(work) – transform the STG work by expanding selected handshake transitions by adding _req and _ack suffixestransformStgExplicitPlace(work) – transform the STG work by making selected (or all) places explicittransformStgImplicitPlace(work) – transform the STG work by making selected (or all) places implicittransformStgInsertDummy(work) – transform the STG work by inserting dummies into selected arcstransformStgMergeTransition(work) – transform the STG work by merging selected transitionstransformStgMirrorSignal(work) – transform the STG work by mirroring selected (or all) signalstransformStgMirrorTransition(work) – transform the STG work by mirroring selected (or all) transition signtransformStgSelectAllSignalTransitions(work) – select all transitions of selected signals in the STG worktransformStgSignalToDummyTransition(work) – transform the STG work by converting selected signal transitions to dummiestransformStgSplitTransition(work) – transform the STG work by splitting selected transitions since v3.5.2transformWtgStructureWaveform(work) – transform the WTG work by structuring the waveformsThese commands are intended for cross-referencing between work files.
setCircuitEnvironment(work, env) – set env STG file or work as an environment for the Circuit work since v3.2.3getCircuitEnvironment(work) – get an environment STG file for the Circuit work since v3.2.3setCircuitComponentRefinement(work, ref, path) – set path file as refinement for component ref in Circuit work since v3.3.7getCircuitComponentRefinement(work, ref) – get path to refinement file for component ref in Circuit work since v3.3.7setStgRefinement(work, path) – set path file as refinement for STG work since v3.3.7getStgRefinement(work) – get path to refinement file for STG work since v3.3.7// Mirror signals and untoggle transitions of STG model inStgWork = load("in.stg.work"); transformStgMirrorSignal(inStgWork); outStgWork = convertStgUntoggle(inStgWork); save(outStgWork, "out.stg.work"); exit();
// 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();
// 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); }
// 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();
// 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();