From da44685dc2bbecd5f363ddf89b6b175385897474 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Mon, 3 Nov 2025 06:28:53 -0500 Subject: [PATCH 01/27] copilot-bluespec: Flip direction of interface inputs and outputs in Bluespec. Refs #677. The current Bluespec backend leads to Verilog code that requires manual manipulations in order to work correctly. Specifically, Copilot externs, which are inputs to the Copilot monitoring system, are treated as _outputs_ in Verilog, and Copilot triggers, which can be considered outputs of the monitoring system, are treated as _inputs_. This order of inputs and outputs is the opposite what we would like users to work with, and of what other backends generate (e.g., C99). This commit updates the internals of `copilot-bluespec` to flip the order in which generated Bluespec module interfaces declare their inputs and outputs. A module interface now represents each Copilot extern as a method of type ` -> Action` (where `` is the type of the extern), as this type directly translates to a Verilog input. Moreover, a module interface now represents trigger arguments as interface methods of type `_i`, where each `_i` is the type of each trigger argument. Each `_i` directly translates to a Verilog output. In addition to changing the module interface definitions, this commit also changes the generated modules that instantiate the new interfaces. One of the more notable changes is that all extern values are stored as a Bluespec `Wire` in the module internals, as using `Wire`s leads to compact Verilog code without adding any user-visible inputs or outputs. Every time a value is read from an extern, the corresponding `Wire` must be read from, which means that several parts of the module internals have been updated to reference these `Wire`s. --- .../src/Copilot/Compile/Bluespec/CodeGen.hs | 155 +++++++++++++++--- .../src/Copilot/Compile/Bluespec/Expr.hs | 5 +- .../src/Copilot/Compile/Bluespec/Name.hs | 21 ++- 3 files changed, 149 insertions(+), 32 deletions(-) diff --git a/copilot-bluespec/src/Copilot/Compile/Bluespec/CodeGen.hs b/copilot-bluespec/src/Copilot/Compile/Bluespec/CodeGen.hs index 6d9fde04..859c73de 100644 --- a/copilot-bluespec/src/Copilot/Compile/Bluespec/CodeGen.hs +++ b/copilot-bluespec/src/Copilot/Compile/Bluespec/CodeGen.hs @@ -14,12 +14,17 @@ module Copilot.Compile.Bluespec.CodeGen -- * Stream generators , mkGenFun + -- * External streams + , mkExtWireDecln + -- * Monitor processing , mkStepRule + , mkExtRule , mkTriggerRule -- * Module interface specifications , mkSpecIfcFields + , mkSpecIfcRulesFields ) where -- External imports @@ -48,7 +53,17 @@ mkGenFun name expr ty = [] where nameId = BS.mkId BS.NoPos $ fromString $ lowercaseName name - def = BS.CClause [] [] (transExpr expr) + def = BS.CClause [] [] (transExpr expr) + +-- | Bind a @Wire@ variable using @mkBypassWire@. +mkExtWireDecln :: String -> Type a -> BS.CStmt +mkExtWireDecln name ty = + BS.CSBindT + (BS.CPVar (BS.mkId BS.NoPos (fromString (wireName name)))) + Nothing + [] + (BS.CQType [] (tWire `BS.TAp` transType ty)) + (BS.CVar (BS.mkId BS.NoPos "mkBypassWire")) -- | Bind a buffer variable and initialise it with the stream buffer. mkBuffDecln :: forall a. Id -> Type a -> [a] -> [BS.CStmt] @@ -133,44 +148,124 @@ mkAccessDecln sId ty xs = -- | Define fields for a module interface containing a specification's trigger -- functions and external variables. -mkSpecIfcFields :: [Trigger] -> [External] -> [BS.CField] -mkSpecIfcFields triggers exts = +mkSpecIfcFields :: [UniqueTrigger] -> [External] -> [BS.CField] +mkSpecIfcFields uniqueTriggers exts = + concatMap mkTriggerFields uniqueTriggers ++ map mkExtField exts + where + -- trigger_guard :: Bool + -- trigger_arg0 :: arg_ty_0 + -- ... + -- trigger_arg(n-1) :: arg_ty_(n-1) + mkTriggerFields :: UniqueTrigger -> [BS.CField] + mkTriggerFields (UniqueTrigger uniqueName (Trigger _name _ args)) = + triggerGuardField : triggerArgFields + where + triggerGuardField :: BS.CField + triggerGuardField = mkField (guardName uniqueName) [] BS.tBool + + triggerArgFields :: [BS.CField] + triggerArgFields = + zipWith + (\(UExpr arg _) argName -> mkField argName [] (transType arg)) + args + (argNames uniqueName) + + -- ext :: ty -> Action + mkExtField :: External -> BS.CField + mkExtField (External name ty) = + mkField + name + [ BS.PIPrefixStr "" + , BS.PIArgNames [BS.mkId BS.NoPos $ fromString $ lowercaseName name] + ] + (BS.tArrow `BS.TAp` transType ty `BS.TAp` BS.tAction) + +-- | Define fields for a module interface containing the actions to perform for +-- a specification's trigger functions and external variables. +mkSpecIfcRulesFields :: [Trigger] -> [External] -> [BS.CField] +mkSpecIfcRulesFields triggers exts = map mkTriggerField triggers ++ map mkExtField exts where - -- trigger :: args_1 -> ... -> args_n -> Action + -- trigger_action :: arg_ty_0 -> ... -> arg_ty_(n-1) -> Action mkTriggerField :: Trigger -> BS.CField mkTriggerField (Trigger name _ args) = - mkField name $ - foldr - (\(UExpr arg _) res -> BS.tArrow `BS.TAp` transType arg `BS.TAp` res) - BS.tAction - args + mkField (actionName name) [] triggerFieldType + where + triggerFieldType :: BS.CType + triggerFieldType = foldr addArgType BS.tAction args - -- ext :: Reg ty + addArgType :: UExpr -> BS.CType -> BS.CType + addArgType (UExpr arg _) res = + BS.tArrow `BS.TAp` transType arg `BS.TAp` res + + -- ext_action :: ActionValue ty mkExtField :: External -> BS.CField mkExtField (External name ty) = - mkField name $ tReg `BS.TAp` transType ty + mkField (actionName name) [] (BS.tActionValue `BS.TAp` transType ty) + +-- | Define a rule for an external stream that performs an action on the most +-- recently computed value from the stream. +mkExtRule :: External -> BS.CRule +mkExtRule (External name _) = + -- rules + -- "ext": when True ==> + -- action + -- extVal <- ifcRules.ext_action + -- ifc.ext extVal + BS.CRule + [] + (Just $ cLit $ BS.LString name) + [BS.CQFilter $ BS.CCon BS.idTrue []] + (BS.Caction BS.NoPos [callExtAction, callExt]) + where + ifcArgId = BS.mkId BS.NoPos $ fromString ifcArgName + ifcRulesArgId = BS.mkId BS.NoPos $ fromString ifcRulesArgName + + extActionId = BS.mkId BS.NoPos $ fromString $ actionName name + extId = BS.mkId BS.NoPos $ fromString name + extValId = BS.mkId BS.NoPos $ fromString $ name ++ "Val" --- | Define a rule for a trigger function. + -- extVal <- ifcRules.ext_action + callExtAction :: BS.CStmt + callExtAction = + BS.CSBind + (BS.CPVar extValId) + Nothing + [] + (BS.CSelect (BS.CVar ifcRulesArgId) extActionId) + + -- ifc.ext extVal + callExt :: BS.CStmt + callExt = + BS.CSExpr Nothing $ + BS.CApply (BS.CSelect (BS.CVar ifcArgId) extId) [BS.CVar extValId] + +-- | Define a rule for a trigger function that performs an action when the rule +-- fires. mkTriggerRule :: UniqueTrigger -> BS.CRule mkTriggerRule (UniqueTrigger uniqueName (Trigger name _ args)) = + -- rules + -- "trigger": when ifc.trigger_guard ==> + -- ifcRules.trigger_action ifc.trigger_arg0 BS.CRule [] (Just $ cLit $ BS.LString uniqueName) [ BS.CQFilter $ - BS.CVar $ BS.mkId BS.NoPos $ - fromString $ guardName uniqueName + BS.CSelect + (BS.CVar ifcArgId) + (BS.mkId BS.NoPos $ fromString $ guardName uniqueName) ] - (BS.CApply nameExpr args') + (BS.CApply actionNameExpr args') where - ifcArgId = BS.mkId BS.NoPos $ fromString ifcArgName + ifcArgId = BS.mkId BS.NoPos $ fromString ifcArgName + ifcRulesArgId = BS.mkId BS.NoPos $ fromString ifcRulesArgName -- Note that we use 'name' here instead of 'uniqueName', as 'name' is the -- name of the actual external function. - nameId = BS.mkId BS.NoPos $ fromString $ lowercaseName name - nameExpr = BS.CSelect (BS.CVar ifcArgId) nameId + actionNameId = BS.mkId BS.NoPos $ fromString $ actionName name + actionNameExpr = BS.CSelect (BS.CVar ifcRulesArgId) actionNameId args' = take (length args) (map argCall (argNames uniqueName)) - argCall = BS.CVar . BS.mkId BS.NoPos . fromString + argCall = BS.CSelect (BS.CVar ifcArgId) . BS.mkId BS.NoPos . fromString -- | Writes the @step@ rule that updates all streams. mkStepRule :: [Stream] -> Maybe BS.CRule @@ -233,19 +328,20 @@ mkStructDecln x = -- Derive a Bits instance so that we can put this struct in a Reg [BS.CTypeclass BS.idBits] where - structId = BS.mkId BS.NoPos $ fromString $ uppercaseName $ typeName x + structId = BS.mkId BS.NoPos $ fromString $ uppercaseName $ typeName x structFields = map mkStructField $ toValues x mkStructField :: Value a -> BS.CField mkStructField (Value ty field) = - mkField (fieldName field) (transType ty) + mkField (fieldName field) [] (transType ty) --- | Write a field of a struct or interface, along with its type. -mkField :: String -> BS.CType -> BS.CField -mkField name ty = +-- | Write a field of a struct or interface, along with its pragmas and type +-- signature. +mkField :: String -> [BS.IfcPragma] -> BS.CType -> BS.CField +mkField name pragmas ty = BS.CField { BS.cf_name = BS.mkId BS.NoPos $ fromString $ lowercaseName name - , BS.cf_pragmas = Nothing + , BS.cf_pragmas = Just pragmas , BS.cf_type = BS.CQType [] ty , BS.cf_default = [] , BS.cf_orig_type = Nothing @@ -260,3 +356,12 @@ tReg = BS.TCon $ , BS.tcon_sort = BS.TIstruct (BS.SInterface []) [BS.id_write BS.NoPos, BS.id_read BS.NoPos] } + +-- | The @Wire@ Bluespec type. +tWire :: BS.CType +tWire = BS.TCon $ + BS.TyCon + { BS.tcon_name = BS.mkId BS.NoPos "Wire" + , BS.tcon_kind = Just (BS.Kfun BS.KStar BS.KStar) + , BS.tcon_sort = BS.TItype 0 tReg + } diff --git a/copilot-bluespec/src/Copilot/Compile/Bluespec/Expr.hs b/copilot-bluespec/src/Copilot/Compile/Bluespec/Expr.hs index c4978aef..7297fad2 100644 --- a/copilot-bluespec/src/Copilot/Compile/Bluespec/Expr.hs +++ b/copilot-bluespec/src/Copilot/Compile/Bluespec/Expr.hs @@ -51,11 +51,8 @@ transExpr (Drop _ amount sid) = [BS.CLit $ BS.CLiteral BS.NoPos index] transExpr (ExternVar _ name _) = - let ifcArgId = BS.mkId BS.NoPos $ fromString ifcArgName in BS.CSelect - (BS.CSelect - (BS.CVar ifcArgId) - (BS.mkId BS.NoPos $ fromString $ lowercaseName name)) + (BS.CVar $ BS.mkId BS.NoPos $ fromString $ wireName name) (BS.id_read BS.NoPos) transExpr (Label _ _ e) = transExpr e -- ignore label diff --git a/copilot-bluespec/src/Copilot/Compile/Bluespec/Name.hs b/copilot-bluespec/src/Copilot/Compile/Bluespec/Name.hs index dbc714a3..19b78ca9 100644 --- a/copilot-bluespec/src/Copilot/Compile/Bluespec/Name.hs +++ b/copilot-bluespec/src/Copilot/Compile/Bluespec/Name.hs @@ -1,9 +1,11 @@ -- | Naming of variables and functions in Bluespec. module Copilot.Compile.Bluespec.Name - ( argNames + ( actionName + , argNames , generatorName , guardName , ifcArgName + , ifcRulesArgName , indexName , lowercaseName , specIfcName @@ -13,6 +15,7 @@ module Copilot.Compile.Bluespec.Name , streamElemName , streamName , uppercaseName + , wireName ) where -- External imports @@ -41,11 +44,14 @@ specTypesPkgName prefix = prefix ++ "Types" streamElemName :: Id -> Int -> String streamElemName sId n = streamName sId ++ "_" ++ show n --- | The name of the variable of type @Ifc@. This is used to select --- trigger functions and external variables. +-- | The name of a variable of type @Ifc@. ifcArgName :: String ifcArgName = "ifc" +-- | The name of a variable of type @RulesIfc@. +ifcRulesArgName :: String +ifcRulesArgName = "ifcRules" + -- | 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 @@ -86,6 +92,15 @@ generatorName sId = streamName sId ++ "_gen" guardName :: String -> String guardName name = lowercaseName name ++ "_guard" +-- | Turn the name of a trigger of external stream into the name of a method +-- that performs a Bluespec @Action@. +actionName :: String -> String +actionName name = lowercaseName name ++ "_action" + +-- | Turn the name of an external stream into a Bluespec @Wire@. +wireName :: String -> String +wireName name = lowercaseName name ++ "_wire" + -- | Turn a trigger name into a an trigger argument name. argName :: String -> Int -> String argName name n = lowercaseName name ++ "_arg" ++ show n From c3543283a9af6720dc86067999042f30d0fbd33d Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Mon, 3 Nov 2025 06:29:25 -0500 Subject: [PATCH 02/27] copilot-bluespec: Update Copilot.Compile.Bluespec.Compile to reflect new input/output order. Refs #677. The current Bluespec backend leads to Verilog code that requires manual manipulations in order to work correctly. Specifically, Copilot externs, which are inputs to the Copilot monitoring system, are treated as _outputs_ in Verilog, and Copilot triggers, which can be considered outputs of the monitoring system, are treated as _inputs_. This order of inputs and outputs is the opposite what we would like users to work with, and of what other backends generate (e.g., C99). A prior commit has updated the internals of `copilot-bluespec` to invert the order in which Verilog inputs and outputs are declared. This commit adapts the top-level code in `Copilot.Compile.Bluespec.Compile` accordingly. In particular, the `compileWith` function now generates a `.bs` file that defines two module interfaces: one interface that contains the core methods that will comprise the generated Verilog code, and another interface that helps automate the process of defining a `Module Empty` value that is more suitable for software simulation purposes. Previously, `compileWith` generated a separate `Ifc.bs` file that contained nothing but the module interface in isolation so that it could be used separately from the interface's `Module` definition. This distinction no longer makes as much sense, as in the new design, as (1) there are now multiple interfaces, and (2) it is unlikely that the interfaces are not particularly useful without having the `Module` definitions to accompany them. As such, this commit now omits generating a `Ifc.bs` file, instead opting to generate the interfaces as part of `.bs`. --- .../src/Copilot/Compile/Bluespec/Compile.hs | 293 ++++++++++++------ .../src/Copilot/Compile/Bluespec/Name.hs | 5 + 2 files changed, 195 insertions(+), 103 deletions(-) diff --git a/copilot-bluespec/src/Copilot/Compile/Bluespec/Compile.hs b/copilot-bluespec/src/Copilot/Compile/Bluespec/Compile.hs index c4701eaf..5343fd6a 100644 --- a/copilot-bluespec/src/Copilot/Compile/Bluespec/Compile.hs +++ b/copilot-bluespec/src/Copilot/Compile/Bluespec/Compile.hs @@ -57,13 +57,11 @@ compileWith bsSettings prefix spec | otherwise = do let typesBsFile = render $ pPrint $ compileTypesBS bsSettings prefix spec - ifcBsFile = render $ pPrint $ compileIfcBS bsSettings prefix spec bsFile = render $ pPrint $ compileBS bsSettings prefix spec let dir = bluespecSettingsOutputDirectory bsSettings createDirectoryIfMissing True dir writeFile (dir specTypesPkgName prefix ++ ".bs") typesBsFile - writeFile (dir specIfcPkgName prefix ++ ".bs") ifcBsFile writeFile (dir "bs_fp.c") copilotBluespecFloatingPointC writeFile (dir "BluespecFP.bsv") copilotBluespecFloatingPointBSV writeFile (dir prefix ++ ".bs") bsFile @@ -93,32 +91,8 @@ compile :: String -> Spec -> IO () compile = compileWith mkDefaultBluespecSettings -- | Generate a @.bs@ file from a 'Spec'. 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: --- --- * @Ifc.bs@, which defines the interface containing the trigger --- functions and external variables. --- --- * @Types.bs@, which defines any structs used in the 'Spec'. --- --- It will also generate a @mk :: Module Ifc -> Module Empty@ --- function, which defines the module structure for this 'Spec'. The --- @mk@ function has the following structure: --- --- * First, bind the argument of type @Module Ifc@ 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. +-- the Bluespec backend. See the @copilot-bluespec/DESIGN.md@ document for a +-- high-level description of what this file contains. compileBS :: BluespecSettings -> String -> Spec -> BS.CPackage compileBS _bsSettings prefix spec = BS.CPackage @@ -126,53 +100,157 @@ compileBS _bsSettings prefix spec = (Right []) (stdLibImports ++ genImports) [] - [moduleDef] + [ ifcDef + , mkModuleDefPragma + , mkModuleDef + , ifcRulesDef + , mkModuleRulesDef + , addModuleRulesDef + ] [] where -- import Types - -- import Ifc genImports :: [BS.CImport] genImports = [ BS.CImpId False $ BS.mkId BS.NoPos $ fromString $ specTypesPkgName prefix - , BS.CImpId False $ BS.mkId BS.NoPos $ fromString - $ specIfcPkgName prefix , BS.CImpId False $ BS.mkId BS.NoPos "BluespecFP" ] - moduleDef :: BS.CDefn - moduleDef = BS.CValueSign $ - BS.CDef - (BS.mkId BS.NoPos $ fromString $ "mk" ++ prefix) - -- :: Module Ifc -> Module Empty - (BS.CQType - [] - (BS.tArrow - `BS.TAp` (BS.tModule `BS.TAp` ifcTy) - `BS.TAp` (BS.tModule `BS.TAp` emptyTy))) - [ BS.CClause [BS.CPVar ifcModId] [] $ - BS.Cmodule BS.NoPos $ - BS.CMStmt - (BS.CSBind (BS.CPVar ifcArgId) Nothing [] (BS.CVar ifcModId)) - : map BS.CMStmt mkGlobals ++ - [ BS.CMStmt $ BS.CSletrec genFuns - , BS.CMrules $ BS.Crules [] rules - ] - ] + -- interface Ifc {-# always_ready, always_enabled #-} = + -- ... + ifcDef :: BS.CDefn + ifcDef = BS.Cstruct + True + (BS.SInterface [BS.PIAlwaysRdy, BS.PIAlwaysEnabled]) + (BS.IdK ifcId) + [] -- No type variables + ifcFields + [] -- No derived instances - ifcArgId = BS.mkId BS.NoPos $ fromString ifcArgName - ifcModId = BS.mkId BS.NoPos "ifcMod" + -- {-# properties mkFibs = { verilog } #-} + mkModuleDefPragma :: BS.CDefn + mkModuleDefPragma = BS.CPragma $ BS.Pproperties mkModuleDefId [BS.PPverilog] - rules :: [BS.CRule] - rules = map mkTriggerRule uniqueTriggers ++ maybeToList (mkStepRule streams) + -- mk :: Module Ifc + -- mk = + -- module + -- ... + mkModuleDef :: BS.CDefn + mkModuleDef = BS.CValueSign $ + BS.CDef + mkModuleDefId + (BS.CQType [] (BS.tModule `BS.TAp` ifcTy)) + [ BS.CClause [] [] $ + BS.Cmodule BS.NoPos $ + wireGlobalStmts ++ genFunStmts ++ ruleIfcStmts + ] + where + wireGlobalStmts :: [BS.CMStmt] + wireGlobalStmts = map BS.CMStmt (mkExtWires ++ mkGlobals) + + genFunStmts :: [BS.CMStmt] + genFunStmts = + -- language-bluespec's pretty-printer will error if it encounters a + -- CSletrec with an empty list of definitions, so avoid generating a + -- CSletrec if there are no streams. + [ BS.CMStmt $ BS.CSletrec genFuns | not (null genFuns) ] + + ruleIfcStmts :: [BS.CMStmt] + ruleIfcStmts = + [ BS.CMrules $ BS.Crules [] $ maybeToList $ mkStepRule streams + , BS.CMinterface $ BS.Cinterface BS.NoPos (Just ifcId) ifcMethodImpls + ] + + -- interface RulesIfc = + -- ... + ifcRulesDef :: BS.CDefn + ifcRulesDef = + BS.Cstruct + True + (BS.SInterface []) + (BS.IdK ifcRulesId) + [] -- No type variables + ifcRulesFields + [] -- No derived instances + + -- mkRules :: Ifc -> RulesIfc -> Rules + -- mkRules ifc ifcRules = + -- rules + -- ... + mkModuleRulesDef :: BS.CDefn + mkModuleRulesDef = + BS.CValueSign $ + BS.CDef + mkModuleRulesDefId + (BS.CQType [] mkModuleRulesType) + [ BS.CClause + (map BS.CPVar [ifcArgId, ifcRulesArgId]) + [] + (BS.Crules [] moduleRules) + ] + where + -- Ifc -> RulesIfc -> Rules + mkModuleRulesType :: BS.CType + mkModuleRulesType = + BS.tArrow `BS.TAp` ifcTy `BS.TAp` + (BS.tArrow `BS.TAp` ifcRulesTy `BS.TAp` BS.tRules) + + -- rules + -- ... + moduleRules :: [BS.CRule] + moduleRules = map mkTriggerRule uniqueTriggers ++ map mkExtRule exts + + -- addRules :: Ifc -> RulesIfc -> Module Empty + -- addRules ifc ifcRules = addRules (mkRules ifc ifcRules) + addModuleRulesDef :: BS.CDefn + addModuleRulesDef = + BS.CValueSign $ + BS.CDef + addModuleRulesDefId + (BS.CQType [] addModuleRulesType) + [ BS.CClause + (map BS.CPVar [ifcArgId, ifcRulesArgId]) + [] + addModuleRulesExpr + ] + where + -- Ifc -> RulesIfc -> Module Empty + addModuleRulesType :: BS.CType + addModuleRulesType = + BS.tArrow `BS.TAp` ifcTy `BS.TAp` + (BS.tArrow `BS.TAp` ifcRulesTy `BS.TAp` + (BS.tModule `BS.TAp` emptyTy)) + + -- addRules (mkRules ifc ifcRules) + addModuleRulesExpr :: BS.CExpr + addModuleRulesExpr = + BS.CApply + (BS.CVar (BS.idAddRules BS.NoPos)) + [BS.CApply + (BS.CVar mkModuleRulesDefId) + (map BS.CVar [ifcArgId, ifcRulesArgId])] + + mkModuleDefId = + BS.mkId BS.NoPos $ fromString $ "mk" ++ prefix + mkModuleRulesDefId = + BS.mkId BS.NoPos $ fromString $ "mk" ++ prefix ++ "Rules" + addModuleRulesDefId = + BS.mkId BS.NoPos $ fromString $ "add" ++ prefix ++ "Rules" streams = specStreams spec triggers = specTriggers spec uniqueTriggers = mkUniqueTriggers triggers exts = gatherExts streams triggers + -- Remove duplicates due to multiple guards for the same trigger. + triggersNoDups = nubBy compareTrigger triggers + + ifcArgId = BS.mkId BS.NoPos $ fromString ifcArgName + ifcRulesArgId = BS.mkId BS.NoPos $ fromString ifcRulesArgName + ifcId = BS.mkId BS.NoPos $ fromString $ specIfcName prefix - ifcFields = mkSpecIfcFields triggers exts + ifcFields = mkSpecIfcFields uniqueTriggers exts ifcTy = BS.TCon (BS.TyCon { BS.tcon_name = ifcId , BS.tcon_kind = Just BS.KStar @@ -181,12 +259,31 @@ compileBS _bsSettings prefix spec = (map BS.cf_name ifcFields) }) + ifcRulesId = BS.mkId BS.NoPos $ fromString $ specIfcRulesName prefix + ifcRulesFields = mkSpecIfcRulesFields triggersNoDups exts + + ifcRulesTy = + BS.TCon $ + BS.TyCon + { BS.tcon_name = ifcRulesId + , BS.tcon_kind = Just BS.KStar + , BS.tcon_sort = + BS.TIstruct (BS.SInterface []) (map BS.cf_name ifcRulesFields) + } + emptyTy = BS.TCon (BS.TyCon { BS.tcon_name = BS.idEmpty , BS.tcon_kind = Just BS.KStar , BS.tcon_sort = BS.TIstruct (BS.SInterface []) [] }) + -- Bind @Wire@ variables for each extern stream. + mkExtWires :: [BS.CStmt] + mkExtWires = map extWireStmt exts + where + extWireStmt :: External -> BS.CStmt + extWireStmt (External name ty) = mkExtWireDecln name ty + -- Make buffer and index declarations for streams. mkGlobals :: [BS.CStmt] mkGlobals = concatMap buffDecln streams ++ map indexDecln streams @@ -194,11 +291,9 @@ compileBS _bsSettings prefix spec = buffDecln (Stream sId buff _ ty) = mkBuffDecln sId ty buff indexDecln (Stream sId _ _ _ ) = mkIndexDecln sId - -- Make generator functions, including trigger arguments. + -- Make generator functions for streams. genFuns :: [BS.CDefl] - genFuns = map accessDecln streams - ++ map streamGen streams - ++ concatMap triggerGen uniqueTriggers + genFuns = map accessDecln streams ++ map streamGen streams where accessDecln :: Stream -> BS.CDefl accessDecln (Stream sId buff _ ty) = mkAccessDecln sId ty buff @@ -206,56 +301,48 @@ compileBS _bsSettings prefix spec = streamGen :: Stream -> BS.CDefl streamGen (Stream sId _ expr ty) = mkGenFun (generatorName sId) expr ty - triggerGen :: UniqueTrigger -> [BS.CDefl] - triggerGen (UniqueTrigger uniqueName (Trigger _name guard args)) = - guardDef : argDefs + -- Make interface methods for @Ifc@. + ifcMethodImpls :: [BS.CDefl] + ifcMethodImpls = + concatMap triggerMethodImpls uniqueTriggers + ++ map extMethodImpl exts + where + -- interface + -- ext val = ext_wire := val + extMethodImpl :: External -> BS.CDefl + extMethodImpl (External name _) = + BS.CLValue extMethodId [extMethodClause] [] + where + extMethodId = BS.mkId BS.NoPos (fromString name) + valId = BS.mkId BS.NoPos "val" + + -- ext val = ext_wire := val + extMethodClause :: BS.CClause + extMethodClause = + BS.CClause + [BS.CPVar valId] + [] + (BS.Cwrite + BS.NoPos + (BS.CVar (BS.mkId BS.NoPos (fromString (wireName name)))) + (BS.CVar valId)) + + -- interface + -- trig_guard = ... + -- trig_arg0 = ... + -- ... + -- trig_arg(n-1) = ... + triggerMethodImpls :: UniqueTrigger -> [BS.CDefl] + triggerMethodImpls uniqueTrigger = guardDef : argDefs where + UniqueTrigger uniqueName (Trigger _name guard args) = uniqueTrigger + guardDef = mkGenFun (guardName uniqueName) guard Bool argDefs = map argGen (zip (argNames uniqueName) args) argGen :: (String, UExpr) -> BS.CDefl argGen (argName, UExpr ty expr) = mkGenFun argName expr ty --- | Generate a @Ifc.bs@ file from a 'Spec'. This contains the --- definition of the @Ifc@ 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. -compileIfcBS :: BluespecSettings -> String -> Spec -> BS.CPackage -compileIfcBS _bsSettings prefix spec = - BS.CPackage - ifcPkgId - (Right []) - (stdLibImports ++ genImports) - [] - [ifcDef] - [] - where - -- import Types - genImports :: [BS.CImport] - genImports = - [ BS.CImpId False $ BS.mkId BS.NoPos $ fromString - $ specTypesPkgName prefix - ] - - ifcId = BS.mkId BS.NoPos $ fromString $ specIfcName prefix - ifcPkgId = BS.mkId BS.NoPos $ fromString $ specIfcPkgName prefix - ifcFields = mkSpecIfcFields triggers exts - - streams = specStreams spec - exts = gatherExts streams triggers - - -- Remove duplicates due to multiple guards for the same trigger. - triggers = nubBy compareTrigger (specTriggers spec) - - ifcDef :: BS.CDefn - ifcDef = BS.Cstruct - True - (BS.SInterface []) - (BS.IdK ifcId) - [] -- No type variables - ifcFields - [] -- No derived instances - -- | Generate a @Types.bs@ file from a 'Spec'. 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 diff --git a/copilot-bluespec/src/Copilot/Compile/Bluespec/Name.hs b/copilot-bluespec/src/Copilot/Compile/Bluespec/Name.hs index 19b78ca9..ebb87f29 100644 --- a/copilot-bluespec/src/Copilot/Compile/Bluespec/Name.hs +++ b/copilot-bluespec/src/Copilot/Compile/Bluespec/Name.hs @@ -10,6 +10,7 @@ module Copilot.Compile.Bluespec.Name , lowercaseName , specIfcName , specIfcPkgName + , specIfcRulesName , specTypesPkgName , streamAccessorName , streamElemName @@ -35,6 +36,10 @@ specIfcName prefix = uppercaseName (specIfcPkgName prefix) specIfcPkgName :: String -> String specIfcPkgName prefix = prefix ++ "Ifc" +-- | Turn a specification name into the name of its rules-specific interface. +specIfcRulesName :: String -> String +specIfcRulesName prefix = uppercaseName (prefix ++ "RulesIfc") + -- | Turn a specification name into the name of the package that declares its -- struct types. specTypesPkgName :: String -> String From e5536e49a2ebb9e7377b912932eb7662d668ec8e Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Mon, 3 Nov 2025 06:30:12 -0500 Subject: [PATCH 03/27] copilot-bluespec: Update test suite to match new input/output order. Refs #677. The current Bluespec backend leads to Verilog code that requires manual manipulations in order to work correctly. Specifically, Copilot externs, which are inputs to the Copilot monitoring system, are treated as _outputs_ in Verilog, and Copilot triggers, which can be considered outputs of the monitoring system, are treated as _inputs_. This order of inputs and outputs is the opposite what we would like users to work with, and of what other backends generate (e.g., C99). A prior commit has updated the internals of `copilot-bluespec` to invert the order in which Verilog inputs and outputs are declared. This commit updates the test suite to work with the new design. In addition to changing the code to reflect the new order of inputs and outputs, this commit also updates the names of some internal variables from "`input`" to "`input1`". This change is necessary because "`input`" is a reserved keyword in Verilog, and giving a Bluespec interface method the same name as a reserved Verilog keyword becomes an error when the interface is used in the result type of a synthesized module. --- .../tests/Test/Copilot/Compile/Bluespec.hs | 45 ++++++++----------- 1 file changed, 19 insertions(+), 26 deletions(-) diff --git a/copilot-bluespec/tests/Test/Copilot/Compile/Bluespec.hs b/copilot-bluespec/tests/Test/Copilot/Compile/Bluespec.hs index ee99c6e7..c6319faf 100644 --- a/copilot-bluespec/tests/Test/Copilot/Compile/Bluespec.hs +++ b/copilot-bluespec/tests/Test/Copilot/Compile/Bluespec.hs @@ -157,18 +157,15 @@ testRun = once $ ioProperty $ do [ "package Top where" , "" , "import CopilotTest" - , "import CopilotTestIfc" , "import CopilotTestTypes" , "" - , "copilotTestIfc :: Module CopilotTestIfc" - , "copilotTestIfc =" - , " module" - , " interface" - , " nop :: Action" - , " nop = return ()" - , "" , "mkTop :: Module Empty" - , "mkTop = mkCopilotTest copilotTestIfc" + , "mkTop =" + , " module" + , " copilotTestMod <- mkCopilotTest" + , " addCopilotTestRules copilotTestMod $" + , " interface CopilotTestRulesIfc" + , " nop_action = return ()" ] writeFile "Top.bs" bluespecProgram @@ -293,7 +290,7 @@ mkRegressionTest1 op haskellFun vals = t1 = typeOf t2 = typeOf - varName = "input" + varName = "input1" -- | Test the behavior of a binary operation (an @'Op2' a b c@ value) against -- its expected behavior (as a Haskell function of type @[a] -> [b] -> [c]@) @@ -762,7 +759,7 @@ mkTestCase1 genO gen = do t1 = typeOf t2 = typeOf - varName = "input" + varName = "input1" -- | Generate test cases for expressions that behave like binary functions. mkTestCase2 :: (Typed a, Typed b, Typed c) @@ -1016,24 +1013,25 @@ testRunCompareArgBluespecProgram proxy inputs outputType = unlines $ , "import Vector" , "" , "import CopilotTest" - , "import CopilotTestIfc" , "import CopilotTestTypes" , "" ] ++ inputVecDecls ++ [ "" - , "copilotTestIfc :: Module CopilotTestIfc" - , "copilotTestIfc =" + , "mkTop :: Module Empty" + , "mkTop =" , " module" + , " copilotTestMod <- mkCopilotTest" ] ++ inputRegs ++ [ " i :: Reg (Bit 64) <- mkReg 0" , " ready :: Reg Bool <- mkReg False" - , " interface" - , " printBack :: " ++ outputType ++ " -> Action" - , " printBack output = $display " ++ printBackDisplayArgs - , " when ready" , "" + , " addCopilotTestRules copilotTestMod $" + , " interface CopilotTestRulesIfc" + , " printBack_action :: " ++ outputType ++ " -> Action" + , " printBack_action output = $display " ++ printBackDisplayArgs + , " when ready" ] ++ inputMethods ++ [ "" @@ -1043,9 +1041,6 @@ testRunCompareArgBluespecProgram proxy inputs outputType = unlines $ ++ inputUpdates ++ [ " i := i + 1" , " ready := True" - , "" - , "mkTop :: Module Empty" - , "mkTop = mkCopilotTest copilotTestIfc" ] where printBackDisplayArgs :: String @@ -1070,11 +1065,9 @@ testRunCompareArgBluespecProgram proxy inputs outputType = unlines $ inputMethods :: [String] inputMethods = - concatMap - (\(bluespecType, varName, regName, _inputVecName, _inputVals) -> - [ " " ++ varName ++ " :: Reg (" ++ bluespecType ++ ")" - , " " ++ varName ++ " = " ++ regName - ]) + map + (\(_bluespecType, varName, regName, _inputVecName, _inputVals) -> + " " ++ varName ++ "_action = return " ++ regName) vars inputUpdates :: [String] From 3114a448fd3837051bfb35ed5a38a7cc7db0a391 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Mon, 3 Nov 2025 06:30:28 -0500 Subject: [PATCH 04/27] copilot-bluespec: Update DESIGN.md to reflect new input/output order. Refs #677. The current Bluespec backend leads to Verilog code that requires manual manipulations in order to work correctly. Specifically, Copilot externs, which are inputs to the Copilot monitoring system, are treated as _outputs_ in Verilog, and Copilot triggers, which can be considered outputs of the monitoring system, are treated as _inputs_. This order of inputs and outputs is the opposite what we would like users to work with, and of what other backends generate (e.g., C99). A prior commit has updated the internals of `copilot-bluespec` to invert the order in which Verilog inputs and outputs are declared. This commit updates the prose in the `DESIGN.md` document to reflect the new design. The new design is just different enough from the old one that it made sense to completely rewrite certain portions of the document. One of the more notable changes is that there are now separate sections about running the generated Verilog code on hardware versus simulating the generated code in software, as these are distinct use cases that require separate discussion. --- copilot-bluespec/DESIGN.md | 799 ++++++++++++++++++++++++------------- 1 file changed, 527 insertions(+), 272 deletions(-) diff --git a/copilot-bluespec/DESIGN.md b/copilot-bluespec/DESIGN.md index dffb607a..b5a07dd3 100644 --- a/copilot-bluespec/DESIGN.md +++ b/copilot-bluespec/DESIGN.md @@ -5,7 +5,7 @@ compiles a Copilot specification to a Bluespec program. We assume that you already have some familiarity with core Copilot concepts such as streams, triggers, externs, etc. -## Bluespec overview +# Bluespec overview Bluespec is a high-level hardware design language (HDL). Bluespec comes with a compiler, `bsc`, as well as its own simulator, which allows users to run @@ -25,7 +25,7 @@ Bluespec SystemVerilog. This is primarily because BH's Haskell-like syntax is a closer fit to how Copilot is structured, which makes the design of the compiler simpler. -## A small example +# A small example To get a sense for how `copilot-bluespec` works, let us compile a simple Copilot specification down to Bluespec. Our specification will declare a stream @@ -67,224 +67,309 @@ are: 2. The call to `compile "Fibs" spec'` in `main`. This will compile the Copilot specification to a Bluespec program named `Fibs.bs`. -Running this program will generate five files[^1]: +Running this program will generate four files[^1]: [^1]: The actual code in these files is machine-generated and somewhat difficult to read. We have cleaned up the code slightly to make it easier to understand. -* `FibsTypes.bs`: If the Copilot specification contains any structs, then this - file will contain the corresponding Bluespec struct definitions. The - specification does not contain any structs, so this file is mostly empty: +### `Fibs.bs` - ```bluespec - package FibsTypes where +This defines the majority of the Bluespec code needed to implement a monitor: - import FloatingPoint - import Vector - ``` +```bluespec +package Fibs where - Later in this document, we will see a different example that makes use of - structs. Note that the syntax used here is much like in Haskell, with a - notable difference being that Bluespec uses the `package` keyword instead of - `module`. +import FloatingPoint +import Vector -* `FibsIfc.bs`: This file defines a _module interface_ `FibsIfc`, whose methods - correspond to the names of the triggers in the Copilot spec: +import FibsTypes +import BluespecFP - ```bluespec - package FibsIfc where +interface FibsIfc {-# always_ready, always_enabled #-} = + even_guard :: Bool + even_arg0 :: UInt 32 + odd_guard :: Bool + odd_arg0 :: UInt 32 - import FloatingPoint - import Vector +{-# properties mkFibs = { verilog } #-} +mkFibs :: Module FibsIfc +mkFibs = + module + s0_0 :: Reg (UInt 32) <- mkReg 1 + s0_1 :: Reg (UInt 32) <- mkReg 1 + let s0 :: Vector.Vector 2 (Reg (UInt 32)) + s0 = update (update newVector 0 s0_0) 1 s0_1 + s0_idx :: Reg (Bit 64) <- mkReg 0 - import FibsTypes + let s0_get :: Bit 64 -> UInt 32 + s0_get x = (select s0 ((s0_idx + x) % 2))._read - interface FibsIfc = - even :: UInt 32 -> Action - odd :: UInt 32 -> Action - ``` + s0_gen :: UInt 32 + s0_gen = s0_get 0 + s0_get 1 - An interface like `FibsIfc` can be thought of as a special form of data type - that describes how a module (a hardware object) interacts with the - surrounding environment. In order for an application to make use of a Copilot - monitor, it must instantiate `FibsIfc`'s methods. Each method takes a `UInt - 32` (an unsigned 32-bit integer) as an argument and return an `Action`, which - is the Bluespec type for expressions that act on the state of the circuit (at - circuit execution time). Possible `Action`s include reading from and writing - to registers, as well as printing messages. + rules + "step": when True ==> + action + select s0 s0_idx := s0_gen + s0_idx := (s0_idx + 1) % 2 - We will see an example of how to instantiate `FibsIfc` later. + interface FibsIfc + even_guard :: Bool + even_guard = + (s0_get 0 % 2) == 0 -* `Fibs.bs`: This file defines a `mkFibs` function, which orchestrates - everything in the generated Bluespec monitor: + even_arg0 :: UInt 32 + even_arg0 = s0_get 0 - ```bluespec - package Fibs where + odd_guard :: Bool + odd_guard = + not (s0_get 0 % 2 == 0) - import FloatingPoint - import Vector + odd_arg0 :: UInt 32 + odd_arg0 = s0_get 0 - import FibsTypes - import FibsIfc - import BluespecFP +interface FibsRulesIfc = + even_action :: UInt 32 -> Action + odd_action :: UInt 32 -> Action - mkFibs :: Module FibsIfc -> Module Empty - mkFibs ifcMod = - module - ifc <- ifcMod +mkFibsRules :: FibsIfc -> FibsRulesIfc -> Rules +mkFibsRules ifc ifcRules = + rules + "even": when ifc.even_guard ==> + ifcRules.even_action ifc.even_arg0 - s0_0 :: Reg (UInt 32) <- mkReg 1 - s0_1 :: Reg (UInt 32) <- mkReg 1 - let s0 :: Vector 2 (Reg (UInt 32)) - s0 = update (update newVector 0 s0_0) 1 s0_1 - s0_idx :: Reg (Bit 64) <- mkReg 0 + "odd": when ifc.odd_guard ==> + ifcRules.odd_action ifc.odd_arg0 - let s0_get :: Bit 64 -> UInt 32 - s0_get x = (select s0 ((s0_idx + x) % 2))._read +addFibsRules :: FibsIfc -> FibsRulesIfc -> Module Empty +addFibsRules ifc ifcRules = addRules (mkFibsRules ifc ifcRules) +``` - s0_gen :: UInt 32 - s0_gen = s0_get 0 + s0_get 1 +Those familiar with Haskell will likely recognize much of the syntax used here, +although it has some minor differences (e.g., using the `package` keyword +instead of `module`, which means something else in Bluespec). We will go into +the parts of the syntax that are unique to Bluespec as they come up. + +The `Fibs.bs` file consists of five definitions: + +1. `FibsIfc`, which is a _module interface_. An interface like `FibsIfc` can be + thought of as a special form of data type that describes how a module (a + hardware object) interacts with the surrounding environment. In order for an + application to make use of a Copilot monitor, it must instantiate + `FibsIfc`'s methods. We will see an example of how to instantiate `FibsIfc` + momentarily. + + The methods of `FibsIfc` correspond to the names of the triggers in the + Copilot spec. Each trigger has a corresponding _guard_ method, which always + has the type `Bool`, and an _argument_ method for each argument that the + trigger accepts, which has a type corresponding to the type of the argument. + We will see how these work in more detail shortly. For now, think of these + methods as being the "outputs" of the monitor program. + +2. `mkFibs`, which returns a module of type `Module FibsIfc`. A module can be + thought of as a generator of hardware objects. The module uses the `FibsIfc` + interface, which indicates that the implementation of the module + instantiates all of the methods in `FibsIfc`. If you squint, you'll + recognize bits and pieces of the original Copilot spec, such as the part + that checks for even stream elements in `even_guard`. We will go over the + individual definitions used in the implementation of `mkFibs` later. + + Note `mkFibs`'s use of the `module` and `action` keywords. These can be + thought of as specialized versions of Haskell's `do`-notation, where + `module` denotes the `Module` monad, and `action` denotes the `ActionValue` + monad. (Note that `Action` is an alias for `ActionValue ()`.) The `Module` + monad describes how to elaborate the structure of a module, whereas the + `ActionValue` monad describes the behavior of a circuit at execution time. + + Another piece of syntax that is unique to Bluespec modules is the `rules` + keyword, which denote rules that may or may not be run on each clock cycle + of the hardware. This particular module only has a single rule, named + `step`, which updates some internal state used by the module. That internal + state is then used to define the values that the interface methods return. + The `when True` part of the rule indicates that it always runs on every + clock cycle. + +3. `FibsRulesIfc` is another module interface, with one method for each of the + Copilot spec's triggers. Each method takes arguments corresponding to the + types of the triggers' arguments and returns a value of type `Action`. As + the name `FibsRulesIfcs` suggests, these methods are intended to be used to + build up rule definitions, and we will see an example of this shortly. + + As an aside, you may be wondering why there are two different interfaces + that each have methods corresponding to the Copilot spec's trigger + functions. Why not just have a single interface instead? The short answer to + this question is that these interfaces are intended for different use cases: + modules that instantiate `FibsRulesIfc` are intended for simulation, whereas + modules that instantiate `FibsIfc` are intended for Verilog code generation. + For a longer answer to this question, see the "Generating Verilog code" + section below. + +4. `mkFibsRules`, a function which takes two values that instantiate the + `FibsIfc` and `FibsRulesIfc` interfaces and returns a `Rules` value. A value + of type `Rules` is just a set of rules, which can be passed around in + Bluespec like any other value. + + `mkFibsRules` defines two rules, one for each trigger function in the + original Copilot spec. Unlike the `step` rule seen earlier, these rules may + not be run on every clock cycle. Specifically, the `even` rule will only run + if the `ifc.even_guard` expression returns `True` on a given clock cycle, + and the `odd` rule will only run if `ifc.odd_guard` returns `True` on a + given clock cycle. If one of these rules are run, then they will invoke the + corresponding method from the `FibsRulesIfc` interface, passing in the + corresponding `*_arg` method(s) from the `FibsIfc`. + +5. `addFibsRules`, a function which is very similar to `mkFibsRules`, except + that it has the return type `Module Empty` instead of `Rules`. All that + `addFibsRules` does is invoke `mkFibsRules` and then pass it to Bluespec's + `addRules` function, which actually adds the rules to a module. This is a + convenience that allows users to quickly define a full Bluespec module that + is suitable for simulation purposes (see the "Simulating Bluespec code" + section below). + + Note that the module that this returns instantiates the `Empty` interface. + `Empty` is a standard interface with no methods at all, and `Empty` is + typically used in top-level Bluespec modules that act as entrypoints to + simulation. + +### `FibsTypes.bs` + +If the Copilot specification contained any structs, then the generated +`FibsTypes.bs` file would contain the corresponding Bluespec struct +definitions. The specification in `Fibs.hs` does not contain any structs, so +this file is mostly empty: - even_guard :: Bool - even_guard = - (s0_get 0 % 2) == 0 +```bluespec +package FibsTypes where - odd_guard :: Bool - odd_guard = - not (s0_get 0 % 2 == 0) +import FloatingPoint +import Vector +``` - rules - "even": when even_guard ==> - ifc.even (s0_get 0) +Later in this document, we will see a different example that makes use of +structs. - "odd:": when odd_guard ==> - ifc.odd (s0_get 0) +### `BluespecFP.bsv` - "step": when True ==> - action - select s0 s0_idx := s0_gen - s0_idx := (s0_idx + 1) % 2 - ``` +This is a collection of floating-point operations that leverage BDPI +(Bluespec's foreign-function interface). We will omit the full contents of this +file for brevity, but it will look something like this: - `mkFibs` returns a module, which can be thought of as a generator of hardware - objects. `mkFibs` takes a `FibsIfc` module as an argument and returns another - module, which is parameterized by `Empty`. `Empty` is a standard interface - with no methods, and `Empty` is typically used in top-level modules that act - as program entrypoints. +```bluespec +import FloatingPoint::*; - Note that the `module` and `action` keywords can be thought of as specialized - versions of Haskell's `do`-notation, where `module` denotes the `Module` - monad, and `action` denotes the `ActionValue` monad. (Note that `Action` is - an alias for `ActionValue ()`.) The `Monad` monad describes how to elaborate - the structure of a module, whereas the `ActionValue` monad describes the - behavior of a circuit at execution time. - -* `BluespecFP.bsv`: A collection of floating-point operations that leverage BDPI - (Bluespec's foreign-function interface). We will omit the full contents of - this file for brevity, but it will look something like this: - - ```bluespec - import FloatingPoint::*; - - import "BDPI" function Float bs_fp_expf (Float x); - import "BDPI" function Double bs_fp_exp (Double x); - import "BDPI" function Float bs_fp_logf (Float x); - import "BDPI" function Double bs_fp_log (Double x); - ... - ``` +import "BDPI" function Float bs_fp_expf (Float x); +import "BDPI" function Double bs_fp_exp (Double x); +import "BDPI" function Float bs_fp_logf (Float x); +import "BDPI" function Double bs_fp_log (Double x); +... +``` - For more information on what this file does, see the "Floating-point numbers" - section below. +For more information on what this file does, see the "Floating-point numbers" +section below. -* `bs_fp.c`: A collection of floating-point operations implemented in C. These - functions are imported via BDPI in `BluespecFP.bsv`. We will omit the full - contents of this file for brevity, but it will look something like this: +### `bs_fp.c` - ```bluespec - #include +A collection of floating-point operations implemented in C. These functions are +imported via BDPI in `BluespecFP.bsv`. We will omit the full contents of this +file for brevity, but it will look something like this: - union ui_float { - unsigned int i; - float f; - }; +```bluespec +#include - union ull_double { - unsigned long long i; - double f; - }; +union ui_float { + unsigned int i; + float f; +}; - unsigned int bs_fp_expf(unsigned int x) { - ... - } +union ull_double { + unsigned long long i; + double f; +}; - unsigned long long bs_fp_exp(unsigned long long x) { - ... - } +unsigned int bs_fp_expf(unsigned int x) { + ... +} - unsigned int bs_fp_logf(unsigned int x) { - ... - } +unsigned long long bs_fp_exp(unsigned long long x) { + ... +} - unsigned long long bs_fp_log(unsigned long long x) { - ... - } +unsigned int bs_fp_logf(unsigned int x) { + ... +} +unsigned long long bs_fp_log(unsigned long long x) { ... - ``` +} + +... +``` + +For more information on what this file does, see the "Floating-point numbers" +section below. + +## Using the generated Bluespec code + +What do we do with the Bluespec code after generating it? The answer to this +question ultimately depends on your intended use case. Sometimes, it can be +useful to just simulate the Bluespec code in software, which we can do with a +variety of hardware simulators. In other use cases, it can be more useful to +directly synthesize code that can be embedded in real hardware. We will review +each of these workflows below. + +### Simulating Bluespec code - For more information on what this file does, see the "Floating-point numbers" - section below. +Hardware simulation allows us to model the behavior of hardware without +actually needing access to physical hardware to do so. There are a number of +different simulators out there, such as Bluespec's own Bluesim simulator, as +well as Verilog-specific simulators such as Verilator and Icarus Verilog +(`iverilog`). We will be using Bluesim throughout this section, as it is +already bundled with each installation of Bluespec. -In a larger application, a Copilot user would instantiate `mkFibs` with a -`FibsIfc` module that describes what should happen when the `even` and `odd` -triggers fire. `FibsIfc` contains everything that the user must supply; -everything else is handled within the module that `mkFibs` returns. +Suppose we have a Bluespec program that we want to monitor with Copilot. This +program will likely have a top-level module (typically of type `Module Empty`), +and it is the role of the program's developer to decide what action the program +should take whenever the monitor fires a trigger. In a full hardware setting, +these actions might constitute something like blinking an LED or displaying a +message on a seven-segment display. For simulation purposes, however, we can +approximate this behavior by doing something simpler (e.g., printing messages +to standard output on the terminal). -Here is an example of a larger application might look like: +Here is an example of a program that uses the Copilot-generated `Fibs.bs` +monitor shown above: ```bluespec package Top where import Fibs -import FibsIfc import FibsTypes -fibsIfc :: Module FibsIfc -fibsIfc = - module - interface - even x = - $display "Even Fibonacci number: %0d" x - - odd x = - $display "Odd Fibonacci number: %0d" x - mkTop :: Module Empty -mkTop = mkFibs fibsIfc +mkTop = + module + fibsMod <- mkFibs + addFibsRules fibsMod $ + interface FibsRulesIfc + even_action x = + $display "Even Fibonacci number: %0d" x + + odd_action x = + $display "Odd Fibonacci number: %0d" x ``` `mkTop` is the top-level module that we will use as a program entrypoint. The -only interesting thing that it does is instantiate `mkFibs` with a custom -`FibsIfc`, where `even` and `odd` are defined to display a custom message -whenever an even or odd Fibonacci number is encountered, respectively. +only interesting thing that it does is create a `FibsIfc` module internally +(using `mkFibs`) and then define the actions to take when the `even` or `odd` +triggers fire. These actions are defined by the implementations of the +`even_action` and `odd_action` methods, respectively, which print custom +messages to standard output. -We can run `mkTop` by using Bluespec's simulator like so: +We can run `mkTop` by using Bluesim like so: ``` $ bsc -sim -g mkTop -u Top.bs -checking package dependencies -compiling Top.bs -code generation for mkTop starts -Elaborated module file created: mkTop.ba -All packages are up to date. - $ bsc -sim -e mkTop -o mkTop.exe bs_fp.c -Bluesim object created: mkTop.{h,o} -Bluesim object created: model_mkTop.{h,o} -Simulation shared library created: mkTop.exe.so -Simulation executable created: mkTop.exe - $ ./mkTop.exe -m 10 Odd Fibonacci number: 1 Odd Fibonacci number: 1 @@ -304,6 +389,94 @@ the values of registers do not become ready until after the reset signal is enabled. Because all of the rules depend on registers, none of them will fire until the second clock cycle or later. +### Generating Verilog code + +Generating code that is suitable for hardware is a somewhat different problem +than generating code that is suitable for simulation. Many types of hardware +(e.g., FPGAs) require specific hardware description languages in order to +synthesize hardware circuits, such as Verilog or VHDL. Bluespec supports +compiling to Verilog, so we will be focusing on that in this section. + +A typical Verilog module has a number of _signals_ that represent the paths +into a circuit (called _inputs_), within a circuit (called _wires_), and +outside of the circuit (called _outputs_). The generated Bluespec code seen +above has been carefully designed such that the triggers in the Copilot spec +compile directly to Verilog outputs. (Copilot also has a notion of external +streams that compile to Verilog inputs; see the "External streams" section for +more on this.) + +Unlike the simulation use case, generating Verilog code does not make use of +the `FibsRulesIfc` interface at all, as this is a convenience that is only +provided to make simulation easier. Instead, we compile the `mkFibs` module +directly to Verilog: + +``` +$ bsc -verilog -g mkFibs -u Fibs.bs +``` + +This generates a Verilog module `mkFibs.v` that looks like the following: + +```verilog +module mkFibs(CLK, + RST_N, + + even_guard, + + even_arg0, + + odd_guard, + + odd_arg0); + input CLK; + input RST_N; + + // value method even_guard + output even_guard; + + // value method even_arg0 + output [31 : 0] even_arg0; + + // value method odd_guard + output odd_guard; + + // value method odd_arg0 + output [31 : 0] odd_arg0; + + ... + +endmodule // mkFibs +``` + +We show only a subset of the generated Verilog code to highlight the inputs and +outputs. There are two inputs corresponding to the `CLK` (clock) and `RST_N` +(reset) signals, which are generated for all Copilot monitors, regardless of +what the underlying spec is. The outputs correspond to the methods of the +`FibsIfc` interface. For instance, the signal in the `even_guard` output +indicates whether the `even` trigger fires on a given clock cycle or not, and +the value in the `even_arg0` output indicates what argument was passed to the +trigger on that clock cycle. These outputs can then be hooked up to another +part of a hardware circuit (e.g., LEDs) that can respond to these values as +needed. + +In general, if a Bluespec interface has a method of type `t` (where `t` is a +non-monadic type), then that method will be compiled to a Verilog output. If a +method has type `t -> Action`, however, then that method will be compiled to a +Verilog input instead. This is a key reason why it is necessary to separate +`FibsIfc` from `FibsRulesIfc`. If we compiled a `Module FibsRulesIfc` to +Verilog, then the triggers would become inputs, not outputs! + +(As a side note: the generated Bluespec code also employs various other tricks +to get the compiled Verilog code to look the way it does. For instance, note +the `{-# properties mkFibs = { verilog } #-}` pragma above `mkFibs`, which +instructs the Bluespec compiler to synthesize Verilog code for it. Also note +the `{-# always_ready, always_enabled #-}` attributes used in `FibsIfc`, which +ensure that the generated Verilog code does not contain unwanted "ready" or +"enabled" signals as inputs.) + +For a more in-depth tutorial on how to use the generated Verilog code on an +actual FPGA, see [this +tutorial](https://github.com/Copilot-Language/copilot/blob/master/copilot/examples/fpga/HelloWorld/README.md). + ## Streams Much like in `copilot-c99`, `copilot-bluespec` translates each stream @@ -352,8 +525,8 @@ In order to access an element of a stream, we make use of the `s0_get` function: ```bluespec - let s0_get :: Bit 64 -> UInt 32 - s0_get x = (select s0 ((s0_idx + x) % 2))._read + let s0_get :: Bit 64 -> UInt 32 + s0_get x = (select s0 ((s0_idx + x) % 2))._read ``` This will use `s0_idx` and an offset `x` to compute which `Reg` in the `Vector` @@ -362,48 +535,43 @@ to read from. ## Rules The _rules_ govern what actions are performed during each cycle. There are -three actions in the `Fibs.hs` example: +three actions in the `Fibs.bs` example above: one in `mkFibs`: ```bluespec rules - "even": when even_guard ==> - ifc.even (s0_get 0) + "step": when True ==> + action + select s0 s0_idx := s0_gen + s0_idx := (s0_idx + 1) % 2 +``` + +And two more in `mkFibsRules`: - "odd:": when odd_guard ==> - ifc.odd (s0_get 0) +```bluespec + rules + "even": when ifc.even_guard ==> + ifcRules.even_action ifc.even_arg0 - "step": when True ==> do - select s0 s0_idx := s0_gen - s0_idx := (s0_idx + 1) % 2 + "odd": when ifc.odd_guard ==> + ifcRules.odd_action ifc.odd_arg0 ``` Each rule consists of three parts: -1. A label (e.g., `"even"`) that uniquely identifies the rule within the +1. A label (e.g., `"step"`) that uniquely identifies the rule within the module. 2. An explicit condition, which is a boolean expression of the form `when ==> ...`. In order for a rule to fire on a given clock cycle, its explicit condition `` must hold. -3. A rule body (e.g., `ifc.even (s0_get 0)`), which describes what action the - rule performs if it fires on a given clock cycle. +3. A rule body (of type `Action`), which describes what action the rule + performs if it fires on a given clock cycle. In the example above, the `"even"` and `"odd"` rules govern the behavior of the triggers in the Copilot specification. These rules will only fire if -`even_guard` or `odd_guard` hold, and if they fire, they will call the `even` -or `odd` method of `FibsIfcs`, respectively. The definitions of `even_guard` -and `odd_guard` are: - -```bluespec - even_guard :: Bool - even_guard = - (s0_get 0 % 2) == 0 - - odd_guard :: Bool - odd_guard = - not (s0_get 0 % 2 == 0) -``` +`even_guard` or `odd_guard` hold, and if they fire, they will call the +`even_action` or `odd_action` method of `FibsRulesIfc`, respectively. The `"step"` rule is the heart of the Copilot specification, and it always runs on each clock cycle. `"step"` does two things: @@ -412,8 +580,8 @@ on each clock cycle. `"step"` does two things: which is defined like so: ```bluespec - s0_gen :: UInt 32 - s0_gen = s0_get 0 + s0_get 1 + s0_gen :: UInt 32 + s0_gen = s0_get 0 + s0_get 1 ``` 2. It increments `s0_idx`, making sure to wrap around to `0` if its value @@ -433,27 +601,28 @@ however. Recall the definitions of the three rules in the example program above: ```bluespec - rules - "even": when even_guard ==> - ifc.even (s0_get 0) +"step": when True ==> + action + select s0 s0_idx := s0_gen + s0_idx := (s0_idx + 1) % 2 - "odd:": when odd_guard ==> - ifc.odd (s0_get 0) +"even": when ifc.even_guard ==> + ifcRules.even_action ifc.even_arg0 - "step": when True ==> do - select s0 s0_idx := s0_gen - s0_idx := (s0_idx + 1) % 2 +"odd": when ifc.odd_guard ==> + ifcRules.odd_action ifc.odd_arg0 ``` If this were a language like C, then the order in which the rules appear would -have an effect on the runtime semantics of the program, as the behavior of -`s0_get` (used in the `"even"` and `"odd"` rules) depends on the current value -of `s0` and `s0_idx`. In Bluespec, however, the order of these rules do _not_ -matter. The `"step"` rule performs side effects of updating the value of `s0` -and `s0_idx`, but these effects are performed in a single, atomic transaction -at the end of the clock cycle. This means that the values of `s0` and `s0_idx` -that `s0_get` sees will always match their values at the start of the clock -cycle, regardless of what order Bluespec uses to invoke the rules. +have an effect on the runtime semantics of the program, as the values that +`even_arg0` and `odd_arg0` return (used in the `"even"` and `"odd"` rules) +depends on the current value of `s0` and `s0_idx`. In Bluespec, however, the +order of these rules do _not_ matter. The `"step"` rule performs side effects +of updating the value of `s0` and `s0_idx`, but these effects are performed in +a single, atomic transaction at the end of the clock cycle. This means that the +values of `s0` and `s0_idx` that `s0_get` sees will always match their values +at the start of the clock cycle, regardless of what order Bluespec uses to +invoke the rules. Because the Bluespec compiler can pick whatever rule order it wishes to, this can impact the order in which `$display` output is presented. This doesn't @@ -466,8 +635,11 @@ specified. ## External streams The example above sampled data from a stream that was defined within the -Copilot specification. To see what happens when a specification uses an -external stream, let's make one small change to the example: +Copilot specification. Copilot also features a notion of _external_ streams, +which sample data from the surrounding environment. (For instance, one could +populate an external stream with data read from a sensor in a real-world +application.) To see what happens when a specification uses an external stream, +let's make one small change to the example above: ```diff fibs :: Stream Word32 @@ -476,68 +648,117 @@ external stream, let's make one small change to the example: ``` Now let's re-run the example and inspect the resulting Bluespec program. There -are two notable changes worth commenting on. The first change is in -`FibsIfc.bs`: +are several notable changes worth commenting on. The first change is in the +definition of the `FibsIfc` interface: ```bluespec -package FibsIfc where +interface FibsIfc {-# always_ready, always_enabled #-} = + even_guard :: Bool + even_arg0 :: UInt 32 + odd_guard :: Bool + odd_arg0 :: UInt 32 + fibs :: UInt 32 -> Action {-# prefixs = "", arg_names = [fibs] #-} +``` -import FloatingPoint -import Vector +This time, there is an additional `fibs` method of type `UInt 32 -> Action`. +This type is carefully chosen such that when `FibsIfc` is compiled to Verilog, +`fibs` will be represented as an input to the Verilog module, which intuitively +matches how external streams are used in Copilot itself. (Also note the +attributes to the right of the type signature, which ensure that the generated +Verilog input has precisely the name "`fibs`".) -import FibsTypes +The next change is in `mkFibs`, which demonstrates how the `fibs` method is +instantiated: + +```bluespec +{-# properties mkFibs = { verilog } #-} +mkFibs :: Module FibsIfc +mkFibs = + module + fibs_wire :: Wire (UInt 32) <- mkBypassWire + + interface FibsIfc + even_guard :: Bool + even_guard = + (fibs_wire._read % 2) == 0 + + even_arg0 :: UInt 32 + even_arg0 = fibs_wire._read -interface FibsIfc = - even :: UInt 32 -> Action - odd :: UInt 32 -> Action - fibs :: Reg (UInt 32) + odd_guard :: Bool + odd_guard = + not (fibs_wire._read % 2 == 0) + + odd_arg0 :: UInt 32 + odd_arg0 = fibs_wire._read + + fibs val = fibs_wire := val ``` -This time, the `FibsIfc` interface has an additional `fibs` method of type `Reg -(UInt 32)`. This register corresponds to the external stream that we just -defined, and it is the responsibility of the application which instantiates -`FibsIfc` to dictate what values should be written to the register. +This looks quite a bit different! Let's go over what has changed: -The second change is in `Fibs.bs`: +* There are no longer any registers to hold internal state, nor is there a + `"step"` rule that updates the registers. These registers were ultimately + used in service of maintaining the ring buffers that comprised the definition + of the `fibs` stream that was defined within Copilot. Now that `fibs` is an + external stream, none of the ring buffer machinery is needed anymore. -```bluespec -package Fibs where + (Note that this is not an all-or-nothing proposition, as it is possible to + have a Copilot spec that combines defined-within-Copilot streams and external + streams.) -import FloatingPoint -import Vector +* There is a new piece of internal state: the `fibs_wire` `Wire`. Moreover, + all places where `s0_get 0` was called before have now been replaced with + `fibs_wire._read`. A `Wire` is essentially a special type of register that + compiles to more compact Verilog code. -import FibsTypes -import FibsIfc +* Finally, there is now an implementation of the `fibs` method, which writes + the supplied value to `fibs_wire`. This is what allows other methods to see + the most recently sampled value in the `fibs` external stream. -mkFibs :: Module FibsIfc -> Module Empty -mkFibs ifcMod = - module - ifc <- ifcMod +The next change is in the definition of `FibsRulesIfc`, which has also gained +another method corresponding to the `fibs` external stream: - let even_guard :: Bool - even_guard = - (ifc.fibs._read % 2) == 0 +```bluespec +interface FibsRulesIfc = + even_action :: UInt 32 -> Action + odd_action :: UInt 32 -> Action + fibs_action :: ActionValue (UInt 32) +``` - odd_guard :: Bool - odd_guard = - not (ifc.fibs._read % 2 == 0) +Unlike `even_action` and `odd_action`, which denote an action for _consuming_ a +value, the type of `fibs_action` (`ActionValue (UInt 32)`) denotes how to +_produce_ a value. This makes sense, since the application being monitored +ultimately has to be the source of the values that populate the external +stream. The implementation of the `fibs_action` method is where this population +happens. - rules - "even": when even_guard ==> - ifc.even ifc.fibs._read +Finally, the definition of `mkFibsRules` now implements a `"fibs"` rule: - "odd:": when odd_guard ==> - ifc.odd ifc.fibs._read +```bluespec +mkFibsRules :: FibsIfc -> FibsRulesIfc -> Rules +mkFibsRules ifc ifcRules = + rules + "even": when ifc.even_guard ==> + ifcRules.even_action ifc.even_arg0 + + "odd": when ifc.odd_guard ==> + ifcRules.odd_action ifc.odd_arg0 + + "fibs": when Prelude.True ==> + action + fibsVal <- ifcRules.fibs_action + ifc.fibs fibsVal ``` -This time, the only stream that is referenced is `ifc.fibs`. As a consequence, -the `s0` stream, the `s0_idx` index, and the `"step"` rule are no longer -necessary, making the code considerably simpler. +This new rule produces a external value using `ifcRules.fibs_action` and then +feeds it to `ifc.fibs` as an input. + +### Simulating Bluespec code involving external streams -The flip side to having the generated code be simpler is that the application -which uses `mkFibs` must now do additional work to specify what the value of -`ifc.fibs` is. For example, we can port the behavior of the previous version -of the program like so: +Let's update our example from the "Simulating Bluespec code" section to +accommodate `fibs` becoming an external stream. Here is an example of what a +`Top.bs` application might look like: ```bluespec package Top where @@ -545,11 +766,10 @@ package Top where import Vector import Fibs -import FibsIfc import FibsTypes -fibsIfc :: Module FibsIfc -fibsIfc = +mkTop :: Module Empty +mkTop = module s0_0 :: Reg (UInt 32) <- mkReg 1 s0_1 :: Reg (UInt 32) <- mkReg 1 @@ -563,38 +783,73 @@ fibsIfc = s0_gen :: UInt 32 s0_gen = s0_get 0 + s0_get 1 - fibs_impl :: Reg (UInt 32) <- mkReg 1 + fibsMod <- mkFibs - interface - even x = - $display "Even Fibonacci number: %0d" x + addFibsRules fibsMod $ + interface FibsRulesIfc + even_action x = + $display "Even Fibonacci number: %0d" x - odd x = - $display "Odd Fibonacci number: %0d" x + odd_action x = + $display "Odd Fibonacci number: %0d" x - fibs = fibs_impl + fibs_action = return (s0_get 0) rules - "fibs": when True ==> - fibs_impl := s0_get 1 - "step": when True ==> action select s0 s0_idx := s0_gen s0_idx := (s0_idx + 1) % 2 +``` -mkTop :: Module Empty -mkTop = mkFibs fibsIfc +Note that all of the code involving registers and the `"step"` rule now lives +in `Top.bs`, as it is now the responsibility of the application to produce the +values for the `fibs` stream. There is also now an implementation of the +`fibs_action` method that returns the most recently computed Fibonacci number +on each clock cycle. + +### Generating Verilog code involving external streams + +Compiling the new version of `mkFibs` to Verilog produces a `mkFibs.v` file +that looks like the following: + +```verilog +module mkFibs(CLK, + RST_N, + + even_guard, + + even_arg0, + + odd_guard, + + odd_arg0, + + fibs); + input CLK; + input RST_N; + + // value method even_guard + output even_guard; + + // value method even_arg0 + output [31 : 0] even_arg0; + + // value method odd_guard + output odd_guard; + + // value method odd_arg0 + output [31 : 0] odd_arg0; + + // action method fibs + input [31 : 0] fibs; + + ... + +endmodule // mkFibs ``` -The code involving `s0`, `s0_idx`, and the `"step"` rule is exactly as before. -The only notable difference is that we create an additional `fibs_impl` -register, declare `fibs = fibs_impl` when instantiating the `FibsIfc` -interface, and declare an additional `"fibs"` rule to update the value of -`fibs_impl` on each clock cycle. Note that we always set the value of -`fibs_impl` to be `s0_get 1`, which corresponds to the most recently computed -Fibonacci number. If we set `fibs_impl` to be `s0_get 0` instead, then -`fibs_impl` would lag behind by one cycle. (Try it.) +As expected, the only notable change is that there is now a `fibs` input. # Notes From dab5669f4459bcea5a624b4357c46552c8f40c49 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Mon, 3 Nov 2025 06:55:48 -0500 Subject: [PATCH 05/27] copilot-bluespec: Document changes in CHANGELOG. Refs #677. --- copilot-bluespec/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot-bluespec/CHANGELOG b/copilot-bluespec/CHANGELOG index e7472493..17c30d99 100644 --- a/copilot-bluespec/CHANGELOG +++ b/copilot-bluespec/CHANGELOG @@ -1,3 +1,6 @@ +2025-11-03 + * Flip direction of interface inputs and outputs in Bluespec. (#677) + 2025-09-07 * Version bump (4.5.1). (#666) From de6c50a5fbad1bf73971c2a77b52073ae94d4077 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Fri, 7 Nov 2025 22:12:29 -0800 Subject: [PATCH 06/27] copilot-core: Version bump (4.6). Refs #679. --- copilot-core/copilot-core.cabal | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/copilot-core/copilot-core.cabal b/copilot-core/copilot-core.cabal index 78e2d580..6c18d6ca 100644 --- a/copilot-core/copilot-core.cabal +++ b/copilot-core/copilot-core.cabal @@ -1,6 +1,6 @@ cabal-version: >=1.10 name: copilot-core -version: 4.5.1 +version: 4.6 synopsis: An intermediate representation for Copilot. description: Intermediate representation for Copilot. From 60779af32db12faec753518a8e266b7ab4874280 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Fri, 7 Nov 2025 22:12:29 -0800 Subject: [PATCH 07/27] copilot-bluespec: Version bump (4.6). Refs #679. --- copilot-bluespec/copilot-bluespec.cabal | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/copilot-bluespec/copilot-bluespec.cabal b/copilot-bluespec/copilot-bluespec.cabal index f62cb243..975868ac 100644 --- a/copilot-bluespec/copilot-bluespec.cabal +++ b/copilot-bluespec/copilot-bluespec.cabal @@ -1,6 +1,6 @@ cabal-version : >= 1.10 name : copilot-bluespec -version : 4.5.1 +version : 4.6 synopsis : A compiler for Copilot targeting FPGAs. description : This package is a back-end from Copilot to FPGAs in Bluespec. @@ -44,8 +44,8 @@ library , filepath >= 1.4 && < 1.6 , pretty >= 1.1.2 && < 1.2 - , copilot-core >= 4.5.1 && < 4.6 - , language-bluespec >= 0.1 && < 0.2 + , copilot-core >= 4.6 && < 4.7 + , language-bluespec >= 0.1 && < 0.2 exposed-modules : Copilot.Compile.Bluespec From 95f3bcc5c5af02d4952033951cfa1610a1b0122d Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Fri, 7 Nov 2025 22:12:29 -0800 Subject: [PATCH 08/27] copilot-c99: Version bump (4.6). Refs #679. --- copilot-c99/copilot-c99.cabal | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/copilot-c99/copilot-c99.cabal b/copilot-c99/copilot-c99.cabal index b33f4e5b..e5efd5f2 100644 --- a/copilot-c99/copilot-c99.cabal +++ b/copilot-c99/copilot-c99.cabal @@ -1,6 +1,6 @@ cabal-version : >= 1.10 name : copilot-c99 -version : 4.5.1 +version : 4.6 synopsis : A compiler for Copilot targeting C99. description : This package is a back-end from Copilot to C. @@ -45,7 +45,7 @@ library , mtl >= 2.2 && < 2.4 , pretty >= 1.1 && < 1.2 - , copilot-core >= 4.5.1 && < 4.6 + , copilot-core >= 4.6 && < 4.7 , language-c99 >= 0.2.0 && < 0.3 , language-c99-simple >= 0.3 && < 0.4 From 19497c5192b9d17c36a2b9ea6e7adec76246e424 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Fri, 7 Nov 2025 22:12:29 -0800 Subject: [PATCH 09/27] copilot-prettyprinter: Version bump (4.6). Refs #679. --- copilot-prettyprinter/copilot-prettyprinter.cabal | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/copilot-prettyprinter/copilot-prettyprinter.cabal b/copilot-prettyprinter/copilot-prettyprinter.cabal index a5acd909..0f413f63 100644 --- a/copilot-prettyprinter/copilot-prettyprinter.cabal +++ b/copilot-prettyprinter/copilot-prettyprinter.cabal @@ -1,6 +1,6 @@ cabal-version: >=1.10 name: copilot-prettyprinter -version: 4.5.1 +version: 4.6 synopsis: A prettyprinter of Copilot Specifications. description: A prettyprinter of Copilot specifications. @@ -45,7 +45,7 @@ library base >= 4.9 && < 5, pretty >= 1.0 && < 1.2, - copilot-core >= 4.5.1 && < 4.6 + copilot-core >= 4.6 && < 4.7 exposed-modules: From 67d4d52610534e3192881fec42d47c241b306e2a Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Fri, 7 Nov 2025 22:12:29 -0800 Subject: [PATCH 10/27] copilot-interpreter: Version bump (4.6). Refs #679. --- copilot-interpreter/copilot-interpreter.cabal | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/copilot-interpreter/copilot-interpreter.cabal b/copilot-interpreter/copilot-interpreter.cabal index b6b2c4fe..e8b9fad4 100644 --- a/copilot-interpreter/copilot-interpreter.cabal +++ b/copilot-interpreter/copilot-interpreter.cabal @@ -1,6 +1,6 @@ cabal-version: >=1.10 name: copilot-interpreter -version: 4.5.1 +version: 4.6 synopsis: Interpreter for Copilot. description: Interpreter for Copilot. @@ -44,7 +44,7 @@ library base >= 4.9 && < 5, pretty >= 1.0 && < 1.2, - copilot-core >= 4.5.1 && < 4.6 + copilot-core >= 4.6 && < 4.7 exposed-modules: From 1b67a69a58ed80b78bfdc0712f1aa094d051bbd2 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Fri, 7 Nov 2025 22:12:29 -0800 Subject: [PATCH 11/27] copilot-theorem: Version bump (4.6). Refs #679. --- copilot-theorem/copilot-theorem.cabal | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/copilot-theorem/copilot-theorem.cabal b/copilot-theorem/copilot-theorem.cabal index 86bb1c68..b830f91a 100644 --- a/copilot-theorem/copilot-theorem.cabal +++ b/copilot-theorem/copilot-theorem.cabal @@ -14,7 +14,7 @@ description: . -version : 4.5.1 +version : 4.6 license : BSD3 license-file : LICENSE maintainer : Ivan Perez @@ -62,8 +62,8 @@ library , xml >= 1.3 && < 1.4 , what4 >= 1.3 && < 1.8 - , copilot-core >= 4.5.1 && < 4.6 - , copilot-prettyprinter >= 4.5.1 && < 4.6 + , copilot-core >= 4.6 && < 4.7 + , copilot-prettyprinter >= 4.6 && < 4.7 exposed-modules : Copilot.Theorem , Copilot.Theorem.Prove From f57879372d0fc41625a30152e452f79ce7eec3eb Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Fri, 7 Nov 2025 22:12:29 -0800 Subject: [PATCH 12/27] copilot-language: Version bump (4.6). Refs #679. --- copilot-language/copilot-language.cabal | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/copilot-language/copilot-language.cabal b/copilot-language/copilot-language.cabal index 7d02c0bf..543a1177 100644 --- a/copilot-language/copilot-language.cabal +++ b/copilot-language/copilot-language.cabal @@ -1,6 +1,6 @@ cabal-version: >=1.10 name: copilot-language -version: 4.5.1 +version: 4.6 synopsis: A Haskell-embedded DSL for monitoring hard real-time distributed systems. description: @@ -42,9 +42,9 @@ library , data-reify >= 0.6 && < 0.7 , mtl >= 2.0 && < 3 - , copilot-core >= 4.5.1 && < 4.6 - , copilot-interpreter >= 4.5.1 && < 4.6 - , copilot-theorem >= 4.5.1 && < 4.6 + , copilot-core >= 4.6 && < 4.7 + , copilot-interpreter >= 4.6 && < 4.7 + , copilot-theorem >= 4.6 && < 4.7 exposed-modules: Copilot.Language , Copilot.Language.Operators.BitWise From 55f945cc71aabdf1d64f01dc2f588e6917ef6d44 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Fri, 7 Nov 2025 22:12:29 -0800 Subject: [PATCH 13/27] copilot-libraries: Version bump (4.6). Refs #679. --- copilot-libraries/copilot-libraries.cabal | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/copilot-libraries/copilot-libraries.cabal b/copilot-libraries/copilot-libraries.cabal index 3402b529..9b17524f 100644 --- a/copilot-libraries/copilot-libraries.cabal +++ b/copilot-libraries/copilot-libraries.cabal @@ -1,6 +1,6 @@ cabal-version: >=1.10 name: copilot-libraries -version: 4.5.1 +version: 4.6 synopsis: Libraries for the Copilot language. description: Libraries for the Copilot language. @@ -41,7 +41,7 @@ library , containers >= 0.4 && < 0.8 , mtl >= 2.0 && < 2.4 , parsec >= 2.0 && < 3.2 - , copilot-language >= 4.5.1 && < 4.6 + , copilot-language >= 4.6 && < 4.7 exposed-modules: Copilot.Library.Libraries From 0233d7ef064bff68a4bca4d29d4df3248739738a Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Fri, 7 Nov 2025 22:12:29 -0800 Subject: [PATCH 14/27] copilot-verifier: Version bump (4.6). Refs #679. --- copilot-verifier/copilot-verifier.cabal | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/copilot-verifier/copilot-verifier.cabal b/copilot-verifier/copilot-verifier.cabal index 808ac382..9c6bed8d 100644 --- a/copilot-verifier/copilot-verifier.cabal +++ b/copilot-verifier/copilot-verifier.cabal @@ -1,6 +1,6 @@ Cabal-version: 2.2 Name: copilot-verifier -Version: 4.5.1 +Version: 4.6 Author: Galois Inc. Maintainer: rscott@galois.com Copyright: (c) Galois, Inc 2021-2024 @@ -45,9 +45,9 @@ common bldflags bv-sized >= 1.0.0 && < 1.1, bytestring, containers >= 0.5.9.0, - copilot-c99 >= 4.5.1 && < 4.6, - copilot-core >= 4.5.1 && < 4.6, - copilot-theorem >= 4.5.1 && < 4.6, + copilot-c99 >= 4.6 && < 4.7, + copilot-core >= 4.6 && < 4.7, + copilot-theorem >= 4.6 && < 4.7, crucible >= 0.7.1 && < 0.8, crucible-llvm >= 0.7 && < 0.8, crux >= 0.7.1 && < 0.8, @@ -80,10 +80,10 @@ library copilot-verifier-examples hs-source-dirs: examples build-depends: case-insensitive, - copilot >= 4.5.1 && < 4.6, - copilot-language >= 4.5.1 && < 4.6, - copilot-libraries >= 4.5.1 && < 4.6, - copilot-prettyprinter >= 4.5.1 && < 4.6, + copilot >= 4.6 && < 4.7, + copilot-language >= 4.6 && < 4.7, + copilot-libraries >= 4.6 && < 4.7, + copilot-prettyprinter >= 4.6 && < 4.7, copilot-verifier exposed-modules: Copilot.Verifier.Examples From e14f76cff149540e9df1d2467b8f47530ac8f19a Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Fri, 7 Nov 2025 22:12:29 -0800 Subject: [PATCH 15/27] copilot-visualizer: Version bump (4.6). Refs #679. --- copilot-visualizer/copilot-visualizer.cabal | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/copilot-visualizer/copilot-visualizer.cabal b/copilot-visualizer/copilot-visualizer.cabal index c88f26f1..6afd9070 100644 --- a/copilot-visualizer/copilot-visualizer.cabal +++ b/copilot-visualizer/copilot-visualizer.cabal @@ -1,6 +1,6 @@ cabal-version: >= 1.10 name: copilot-visualizer -version: 4.5.1 +version: 4.6 synopsis: Visualizer for Copilot. description: Visualizer for Copilot. @@ -65,10 +65,10 @@ library text >= 1.2.3.1 && < 2.2, websockets >= 0.12.7 && < 0.14, - copilot >= 4.5.1 && < 4.6, - copilot-core >= 4.5.1 && < 4.6, - copilot-interpreter >= 4.5.1 && < 4.6, - copilot-language >= 4.5.1 && < 4.6 + copilot >= 4.6 && < 4.7, + copilot-core >= 4.6 && < 4.7, + copilot-interpreter >= 4.6 && < 4.7, + copilot-language >= 4.6 && < 4.7 exposed-modules: @@ -121,7 +121,7 @@ executable tikz-example build-depends: base >= 4.9 && < 5, - copilot >= 4.5.1 && < 4.6, + copilot >= 4.6 && < 4.7, copilot-visualizer if flag(examples) From 46fe80db107aa4267c131e152005ef9ed8f1543c Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Fri, 7 Nov 2025 22:12:29 -0800 Subject: [PATCH 16/27] copilot: Version bump (4.6). Refs #679. --- copilot/copilot.cabal | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/copilot/copilot.cabal b/copilot/copilot.cabal index a15dd5cf..f52eecc4 100644 --- a/copilot/copilot.cabal +++ b/copilot/copilot.cabal @@ -1,5 +1,5 @@ name: copilot -version: 4.5.1 +version: 4.6 cabal-version: >= 1.10 license: BSD3 license-file: LICENSE @@ -52,12 +52,12 @@ library , directory >= 1.3 && < 1.4 , filepath >= 1.4 && < 1.6 - , copilot-core >= 4.5.1 && < 4.6 - , copilot-theorem >= 4.5.1 && < 4.6 - , copilot-language >= 4.5.1 && < 4.6 - , copilot-libraries >= 4.5.1 && < 4.6 - , copilot-c99 >= 4.5.1 && < 4.6 - , copilot-prettyprinter >= 4.5.1 && < 4.6 + , copilot-core >= 4.6 && < 4.7 + , copilot-theorem >= 4.6 && < 4.7 + , copilot-language >= 4.6 && < 4.7 + , copilot-libraries >= 4.6 && < 4.7 + , copilot-c99 >= 4.6 && < 4.7 + , copilot-prettyprinter >= 4.6 && < 4.7 exposed-modules: Language.Copilot, Language.Copilot.Main From c0d4bedeb7facdcaa4c1757f359866b0f5bad900 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Fri, 7 Nov 2025 22:13:01 -0800 Subject: [PATCH 17/27] copilot-core: Document changes in CHANGELOG. Refs #679. --- copilot-core/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot-core/CHANGELOG b/copilot-core/CHANGELOG index 62e89d1e..b0b94a73 100644 --- a/copilot-core/CHANGELOG +++ b/copilot-core/CHANGELOG @@ -1,3 +1,6 @@ +2025-11-07 + * Version bump (4.6). (#679) + 2025-09-07 * Version bump (4.5.1). (#666) From bc9cf505dfd905599628f89db79e701e3085a44b Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Fri, 7 Nov 2025 22:13:01 -0800 Subject: [PATCH 18/27] copilot-bluespec: Document changes in CHANGELOG. Refs #679. --- copilot-bluespec/CHANGELOG | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/copilot-bluespec/CHANGELOG b/copilot-bluespec/CHANGELOG index 17c30d99..5365300c 100644 --- a/copilot-bluespec/CHANGELOG +++ b/copilot-bluespec/CHANGELOG @@ -1,4 +1,5 @@ -2025-11-03 +2025-11-07 + * Version bump (4.6). (#679) * Flip direction of interface inputs and outputs in Bluespec. (#677) 2025-09-07 From d3fd856ebd79436ac7cb22a5c8bbe40e7c307ece Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Fri, 7 Nov 2025 22:13:01 -0800 Subject: [PATCH 19/27] copilot-c99: Document changes in CHANGELOG. Refs #679. --- copilot-c99/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot-c99/CHANGELOG b/copilot-c99/CHANGELOG index e5f0b606..8b7be686 100644 --- a/copilot-c99/CHANGELOG +++ b/copilot-c99/CHANGELOG @@ -1,3 +1,6 @@ +2025-11-07 + * Version bump (4.6). (#679) + 2025-09-07 * Version bump (4.5.1). (#666) From d6a6578c1de9a32bd1f85d99b011e726a3e81976 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Fri, 7 Nov 2025 22:13:01 -0800 Subject: [PATCH 20/27] copilot-prettyprinter: Document changes in CHANGELOG. Refs #679. --- copilot-prettyprinter/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot-prettyprinter/CHANGELOG b/copilot-prettyprinter/CHANGELOG index 73ca7c5b..26b0500a 100644 --- a/copilot-prettyprinter/CHANGELOG +++ b/copilot-prettyprinter/CHANGELOG @@ -1,3 +1,6 @@ +2025-11-07 + * Version bump (4.6). (#679) + 2025-09-07 * Version bump (4.5.1). (#666) From 5fe6665070954cce96796966a0dfaeab8f92cf37 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Fri, 7 Nov 2025 22:13:01 -0800 Subject: [PATCH 21/27] copilot-interpreter: Document changes in CHANGELOG. Refs #679. --- copilot-interpreter/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot-interpreter/CHANGELOG b/copilot-interpreter/CHANGELOG index e819c416..c6f5b6cb 100644 --- a/copilot-interpreter/CHANGELOG +++ b/copilot-interpreter/CHANGELOG @@ -1,3 +1,6 @@ +2025-11-07 + * Version bump (4.6). (#679) + 2025-09-07 * Version bump (4.5.1). (#666) From 43e71617bf485f8c0357a36b1e64474ad9e8e70c Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Fri, 7 Nov 2025 22:13:01 -0800 Subject: [PATCH 22/27] copilot-theorem: Document changes in CHANGELOG. Refs #679. --- copilot-theorem/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot-theorem/CHANGELOG b/copilot-theorem/CHANGELOG index 621417e7..463ef02c 100644 --- a/copilot-theorem/CHANGELOG +++ b/copilot-theorem/CHANGELOG @@ -1,3 +1,6 @@ +2025-11-07 + * Version bump (4.6). (#679) + 2025-09-07 * Version bump (4.5.1). (#666) * Remove unused function Copilot.Theorem.Misc.SExpr.parseSExpr. (#661) From da3de0a79182d300f67df8f34c74ca5c5470efd6 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Fri, 7 Nov 2025 22:13:01 -0800 Subject: [PATCH 23/27] copilot-language: Document changes in CHANGELOG. Refs #679. --- copilot-language/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot-language/CHANGELOG b/copilot-language/CHANGELOG index ed8ebbeb..c2242629 100644 --- a/copilot-language/CHANGELOG +++ b/copilot-language/CHANGELOG @@ -1,3 +1,6 @@ +2025-11-07 + * Version bump (4.6). (#679) + 2025-09-07 * Version bump (4.5.1). (#666) From c3d752f32f6cc5559f0103e59f73c0ed794f66a4 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Fri, 7 Nov 2025 22:13:01 -0800 Subject: [PATCH 24/27] copilot-libraries: Document changes in CHANGELOG. Refs #679. --- copilot-libraries/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot-libraries/CHANGELOG b/copilot-libraries/CHANGELOG index 5d4323d7..6f6a6a6b 100644 --- a/copilot-libraries/CHANGELOG +++ b/copilot-libraries/CHANGELOG @@ -1,3 +1,6 @@ +2025-11-07 + * Version bump (4.6). (#679) + 2025-09-07 * Version bump (4.5.1). (#666) From e09c1b44dfb8accee4aedb5d4505bd9a568503fb Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Fri, 7 Nov 2025 22:13:01 -0800 Subject: [PATCH 25/27] copilot-verifier: Document changes in CHANGELOG. Refs #679. --- copilot-verifier/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot-verifier/CHANGELOG b/copilot-verifier/CHANGELOG index e8b89e27..e4b2f954 100644 --- a/copilot-verifier/CHANGELOG +++ b/copilot-verifier/CHANGELOG @@ -1,3 +1,6 @@ +2025-11-07 + * Version bump (4.6). (#679) + 2025-09-07 * Version bump (4.5.1). (#666) From 17c7ca00d6fc5220e585bf395d238fe84f2a0941 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Fri, 7 Nov 2025 22:13:01 -0800 Subject: [PATCH 26/27] copilot-visualizer: Document changes in CHANGELOG. Refs #679. --- copilot-visualizer/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot-visualizer/CHANGELOG b/copilot-visualizer/CHANGELOG index cf9f151f..2dbe2a7a 100644 --- a/copilot-visualizer/CHANGELOG +++ b/copilot-visualizer/CHANGELOG @@ -1,3 +1,6 @@ +2025-11-07 + * Version bump (4.6). (#679) + 2025-09-07 * Version bump (4.5.1). (#666) * Relax version constraint on `ogma-extra`. (#645) From 0c5e4477c917061b2ff11ffae07467eb725bd5d2 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Fri, 7 Nov 2025 22:13:01 -0800 Subject: [PATCH 27/27] copilot: Document changes in CHANGELOG. Refs #679. --- copilot/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot/CHANGELOG b/copilot/CHANGELOG index 7b69ed04..11069c98 100644 --- a/copilot/CHANGELOG +++ b/copilot/CHANGELOG @@ -1,3 +1,6 @@ +2025-11-07 + * Version bump (4.6). (#679) + 2025-09-07 * Version bump (4.5.1). (#666) * Add hello world example for FPGA. (#657)