Îõ³h*4ý34.0 7(c) 2011 National Institute of Aerospace / Galois, Inc.SafeVcopilot-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")*&\copilot-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 Translate " e, in Copilot Core into a Bluespec expression.signum e is translated as: 5if e > 0 then 1 else (if e < 0 then negate 1 else e) That is: If e is positive, return 1.If e is negative, return -1.Otherwise, return e. This handles the case where e is 0ò when the type is an integral type. If the type is a floating-point type, it also handles the cases where e is -0 or NaN.8This implementation is modeled after how GHC implements #  øhttps://gitlab.haskell.org/ghc/ghc/-/blob/aed98ddaf72cc38fb570d8415cac5de9d8888818/libraries/base/GHC/Float.hs#L523-L525here.$copilot-bluespecTranslate a Copilot x < y‚ expression into Bluespec. We will generate different code depending on whether the arguments have a floating-point type or not.%copilot-bluespecTranslate a Copilot x > y‚ expression into Bluespec. We will generate different code depending on whether the arguments have a floating-point type or not.&copilot-bluespecTranslate a Copilot x <= y‚ expression into Bluespec. We will generate different code depending on whether the arguments have a floating-point type or not.'copilot-bluespecTranslate a Copilot x >= y‚ expression into Bluespec. We will generate different code depending on whether the arguments have a floating-point type or not.(copilot-bluespec8Translate a Copilot floating-point comparison involving < or >, into a Bluespec expression. Specifically, x < y is translated to: compareFP x y == LT x > y& is translated similarly, except that GT is used instead of LT.See the comments on )Ä for why we translate floating-point comparison operators this way.*copilot-bluespec8Translate a Copilot floating-point comparison involving <= or >=, into a Bluespec expression. Specifically, x <= y is translated to: 3let _c = compareFP x y in (_c == LT) || (_c == EQ) x >= y& is translated similarly, except that GT is used instead of LT.See the comments on )Ä for why we translate floating-point comparison operators this way.)copilot-bluespec#Generate an expression of the form  compareFP x y9. This is used to power the translations of the Copilot <, <=, >, and >=' floating-point operators to Bluespec."Translating these operators using  compareFPù is a somewhat curious design choice, given that Bluespec already defines its own versions of these operators. Unfortunately, we cannot directly use the Bluespec versions of these operators, as they are defined in such a way that they will call errorÉ when one of the arguments is a NaN value. This would pose two problems: 7This would differ from the semantics of Copilot, where x < y will return Falseû (instead of erroring) when one of the arguments is NaN. (Similarly for the other floating-point comparison operators.)4Moreover, if you have a Bluespec program that calls x < y, where the value of x or y" is derived from a register, then bscþ will always fail to compile the code. This is because Bluespec must generate hardware for all possible code paths in <., and because one of the code paths calls error>, this will cause compilation to result in an error. (See  Ìhttps://github.com/B-Lang-org/bsc/discussions/711#discussioncomment-10003586& for a more detailed explanation.)ŠAs such, we avoid using Bluespec's comparison operators and instead translate Copilot's comparison operators to expressions derived from  compareFP9. Unlike Bluespec's other comparison operators, calling  compareFP will never result in an error.+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))].0copilot-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.1copilot-bluespec?Translate a Copilot integer literal into a Bluespec expression.2copilot-bluespecÆTranslate a Copilot floating-point literal into a Bluespec expression.3copilot-bluespec5Create a Bluespec expression consisting of a literal.4copilot-bluespec1Create a Bluespec expression that indexes into a Vector.5copilot-bluespec,Create a Bluespec expression that updates a Vector element at a particular index.6copilot-bluespec•Explicitly annotate an expression with a type signature. This is necessary to prevent expressions from having ambiguous types in certain situations.7copilot-bluespec2True if the type given is a floating point number.8copilot-bluespecéThrow an error if attempting to use a floating-point operation that Bluespec does not currently support.9copilot-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.$copilot-bluespecThe type of the arguments.%copilot-bluespecThe type of the arguments.&copilot-bluespecThe type of the arguments.'copilot-bluespecThe type of the arguments.(copilot-bluespecA Disorder6 label, which we check against the result of calling  compareFP. This should be either LT or GT.*copilot-bluespecA Disorder6 label, which we check against the result of calling  compareFP. This should be either LT or GT.43,/  Safe-Inferred"Ý)¯ :copilot-bluespec(Write a generator function for a stream.;copilot-bluespecÀBind a buffer variable and initialise it with the stream buffer.<copilot-bluespec.Make an index variable and initialise it to 0.=copilot-bluespecÈDefine an accessor function for the ring buffer associated with a stream>copilot-bluespecìDefine fields for a module interface containing a specification's trigger functions and external variables.?copilot-bluespec%Define a rule for a trigger function.@copilot-bluespec Writes the step rule that updates all streams.Acopilot-bluespec3Write a struct declaration based on its definition.Bcopilot-bluespec  Safe-Inferred")*3F 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.Dcopilot-bluespec Generate a  prefix.bs file from a E4. 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 E.It will also generate a mk prefix :: Module  prefixIfc -> Module Empty8 function, which defines the module structure for this E. 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.Fcopilot-bluespec Generate a  prefixIfc.bs file from a E'. 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.Gcopilot-bluespec Generate a  prefixTypes.bs file from a EÍ. 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.Hcopilot-bluespec+Imports from the Bluespec standard library.Icopilot-bluespec8List all types of an expression, returns items uniquely.Jcopilot-bluespec1List all types of a type, returns items uniquely.Kcopilot-bluespecÖCollect all expression of a list of streams and triggers and wrap them into an UEXpr. Safe-Inferred3oÌ      !"#$%&'()*+,-./0123456789:+;<=>?@ABCDEFG H I J K L M N O P Q R+ST U V W X Y ZÛ+copilot-bluespec-4.0-DIY5FdEEPpW9uFnIibAIUDCopilot.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 transSign'copilot-core-4.0-B9lCaMtDp2U7dmjeHjWFWhCopilot.Core.OperatorsSignbaseGHC.NumsignumtransLttransGttransLetransGe transLtOrGtFP compareFPExpr transLeOrGeFP transCastconstTy constVectorCopilot.Core.TypeType genVector constNumTyconstIntconstFPcLit cIndexVector cUpdateVectorwithTypeAnnotationtypeIsFloatingunsupportedFPOpfpRMmkGenFun mkBuffDecln mkIndexDecln mkAccessDeclnmkSpecIfcFields mkTriggerRule mkStepRule mkStructDeclnmkFieldtReg compileBSCopilot.Core.SpecSpec compileIfcBScompileTypesBS stdLibImports exprTypes typeTypes gatherExprs