Îõ³h*"¹!w3.19 7(c) 2011 National Institute of Aerospace / Galois, Inc.SafeWcopilot-bluespec(Report an error due to a bug in Copilot.copilot-bluespec5Name of the function in which the error was detected.copilot-bluespec5Name of the package in which the function is located. Safe-InferredÊݪcopilot-bluespec%Representation of external variables.copilot-bluespec=Collect all external variables from the streams and triggers.’Although Copilot specifications can contain also properties and theorems, the C99 backend currently only generates code for streams and triggers.  Safe-Inferred  copilot-bluespecÀTurn a specification name into the name of its module interface. copilot-bluespecæTurn a specification name into the name of the package that declares its module interface. Note that  & is not necessarily the same name as  Ö, as the former does not need to begin with an uppercase letter, but the latter does.copilot-bluespec×Turn a specification name into the name of the package that declares its struct types.copilot-bluespec,Turn a stream id into a stream element name.copilot-bluespec!The name of the variable of type  prefixIfcÃ. This is used to select trigger functions and external variables.copilot-bluespecóCreate a Bluespec name that must start with an uppercase letter (e.g., a struct or interface name). If the supplied name already begins with an uppercase letter, this function returns the name unchanged. Otherwise, this function prepends a BS_, prefix (short for "Bluespec") at the front.copilot-bluespecðCreate a Bluespec name that must start with a lowercase letter (e.g., a function or method name). If the supplied name already begins with a lowercase letter, this function returns the name unchanged. Otherwise, this function prepends a bs_, prefix (short for "Bluespec") at the front.copilot-bluespec8Turn a stream id into a suitable Bluespec variable name.copilot-bluespec5Turn a stream id into the global varname for indices.copilot-bluespec7Turn a stream id into the name of its accessor functioncopilot-bluespec3Turn stream id into name of its generator function.copilot-bluespec2Turn the name of a trigger into a guard generator.copilot-bluespec4Turn a trigger name into a an trigger argument name.copilot-bluespec3Enumerate all argument names based on trigger name.   Safe-Inferred Ôcopilot-bluespec.Settings used to customize the code generated.copilot-bluespec;Default Bluespec settings. Output to the current directory. Safe-Inferred")* Çcopilot-bluespec,Translate a Copilot type to a Bluespec type.copilot-bluespecThe Vector Bluespec data type.copilot-bluespecThe  FloatingPoint Bluespec struct type. Safe-Inferred")*Tcopilot-bluespecÀTranslates a Copilot Core expression into a Bluespec expression.copilot-bluespecÏTranslates a Copilot unary operator and its argument into a Bluespec function.copilot-bluespecÑTranslates a Copilot binary operator and its arguments into a Bluespec function. copilot-bluespecÒTranslates a Copilot ternary operator and its arguments into a Bluespec function.!copilot-bluespecíBluespec does not have a general-purpose casting operation, so we must handle casts on a case-by-case basis."copilot-bluespecÛTransform a Copilot Core literal, based on its value and type, into a Bluespec expression.#copilot-bluespec8Transform a list of Copilot Core expressions of a given $ into a Bluespec Vector expression.%copilot-bluespec=Transform a list of Copilot Core expressions into a Bluespec Vector expression. When invoking genVector f es, where es has length n, the resulting Vector will consist of :[f 0 (es !! 0), f 1 (es !! 1), ..., f (n-1) (es !! (n-1))].&copilot-bluespec#Translate a literal number of type ty into a Bluespec expression.äPRE: The type of PRE is numeric (integer or floating-point), that is, not boolean, struct or array.'copilot-bluespec?Translate a Copilot integer literal into a Bluespec expression.(copilot-bluespecÆTranslate a Copilot floating-point literal into a Bluespec expression.)copilot-bluespec5Create a Bluespec expression consisting of a literal.*copilot-bluespec1Create a Bluespec expression that indexes into a Vector.+copilot-bluespec•Explicitly annotate an expression with a type signature. This is necessary to prevent expressions from having ambiguous types in certain situations.,copilot-bluespecéThrow an error if attempting to use a floating-point operation that Bluespec does not currently support.-copilot-bluespecðWe assume round-near-even throughout, but this variable can be changed if needed. This matches the behavior of fpRM in copilot-theorem's Copilot.Theorem.What4.Translate module.*)"%  Safe-Inferred"ݧ .copilot-bluespec(Write a generator function for a stream./copilot-bluespecÀBind a buffer variable and initialise it with the stream buffer.0copilot-bluespec.Make an index variable and initialise it to 0.1copilot-bluespecÈDefine an accessor function for the ring buffer associated with a stream2copilot-bluespecìDefine fields for a module interface containing a specification's trigger functions and external variables.3copilot-bluespec%Define a rule for a trigger function.4copilot-bluespec Writes the step rule that updates all streams.5copilot-bluespec3Write a struct declaration based on its definition.6copilot-bluespec copilot-bluespec+Compile a specification to a Bluespec file.ÃThe first argument is the settings for the Bluespec code generated.âThe second argument is used as a module name and the prefix for the .bs files that are generated.copilot-bluespec&Compile a specification to a Bluespec.ÃThe first argument is used as a prefix for the generated .bs files.8copilot-bluespec Generate a  prefix.bs file from a 94. This is the main payload of the Bluespec backend.€The generated Bluespec file will import a handful of files from the standard library, as well as the following generated files: prefixIfc.bsÙ, which defines the interface containing the trigger functions and external variables. prefixTypes.bs(, which defines any structs used in the 9.It will also generate a mk prefix :: Module  prefixIfc -> Module Empty8 function, which defines the module structure for this 9. The mk prefix& function has the following structure:!First, bind the argument of type Module  prefixIfcÐ so that trigger functions can be invoked and external variables can be used.)Next, declare stream buffers and indices.óNext, declare generator functions for streams, accessor functions for streams, and guard functions for triggers..Next, declare rules for each trigger function.ÎFinally, declare a single rule that updates the stream buffers and indices.:copilot-bluespec Generate a  prefixIfc.bs file from a 9'. This contains the definition of the  prefixIfc© interface, which declares the types of all trigger functions and external variables. This is put in a separate file so that larger applications can use it separately.;copilot-bluespec Generate a  prefixTypes.bs file from a 9Í. This declares the types of any structs used by the Copilot specification. This is put in a separate file so that larger applications can more easily substitute their own struct definitions if desired.<copilot-bluespec+Imports from the Bluespec standard library.=copilot-bluespec8List all types of an expression, returns items uniquely.>copilot-bluespec1List all types of a type, returns items uniquely.?copilot-bluespecÖCollect all expression of a list of streams and triggers and wrap them into an UEXpr. Safe-Inferred!gÀ      !"#$%&'()*+,-./012345678 9 : ; < = > ? @ A B C-DE F G H I J KÌ,copilot-bluespec-3.19-CcgXsDngdzB1tZZZZ7SjtaCopilot.Compile.Bluespeccopilot-bluespecCopilot.Compile.Bluespec.Error!Copilot.Compile.Bluespec.ExternalCopilot.Compile.Bluespec.Name!Copilot.Compile.Bluespec.SettingsCopilot.Compile.Bluespec.TypeCopilot.Compile.Bluespec.Expr Copilot.Compile.Bluespec.CodeGen Copilot.Compile.Bluespec.CompileBluespecSettingsbluespecSettingsOutputDirectorymkDefaultBluespecSettings compileWithcompile impossibleExternal gatherExtsextNameextType specIfcNamespecIfcPkgNamespecTypesPkgNamestreamElemName ifcArgName uppercaseName lowercaseName streamName indexNamestreamAccessorName generatorName guardNameargNameargNames transTypetVectortFloatingPoint transExprtransOp1transOp2transOp3 transCastconstTy constVector(copilot-core-3.19-BSiPuyuCgFPIA95rz9yiRUCopilot.Core.TypeType genVector constNumTyconstIntconstFPcLit cIndexVectorwithTypeAnnotationunsupportedFPOpfpRMmkGenFun mkBuffDecln mkIndexDecln mkAccessDeclnmkSpecIfcFields mkTriggerRule mkStepRule mkStructDeclnmkFieldtReg compileBSCopilot.Core.SpecSpec compileIfcBScompileTypesBS stdLibImports exprTypes typeTypes gatherExprs