diff --git a/socs/soc2_test6.soc b/socs/soc2_test6.soc new file mode 100644 index 0000000000..71fbb91c7a --- /dev/null +++ b/socs/soc2_test6.soc @@ -0,0 +1,33 @@ +module DRAM { + input memory (0 bits 40) GDDR0 + output memory (0 bits 40) RAMOUT + GDDR0 accepts [(0x000000000 to 0x0fedfffff)] + + memory (0 bits 40) DRAMMAP + DRAMMAP maps [ + (0x000000000 to 0x0fedfffff) to RAMOUT at (0x000000000 to 0x0fedfffff) + ] +} + +module SOCKET { + instance RAM[1 to 2; 10 to 11] of DRAM + + memory (0 bits 40) LOCAL + LOCAL accepts [(0x000000000 to 0x0fedfffff)] + + memory (0 bits 40) LOCAL_SRC + + forall x in (1 to 2, 10 to 11) { + forall y in (10 to 11) { + RAM[x; y] instantiates DRAM + RAM[x; y] binds [ + RAMOUT to LOCAL + ] + + LOCAL_SRC maps [ + (0x1000 to 0x2000) to RAM[x; y].GDDR0 at (0x1000 to 0x2000) + ] + } + } + +} diff --git a/tools/sockeye/SockeyeBackendProlog.hs b/tools/sockeye/SockeyeBackendProlog.hs index 0709c0e560..8b0dd1a519 100644 --- a/tools/sockeye/SockeyeBackendProlog.hs +++ b/tools/sockeye/SockeyeBackendProlog.hs @@ -19,11 +19,20 @@ module SockeyeBackendProlog import qualified Data.Map as Map import Data.Char import Data.List +import Text.Printf +import Control.Exception (throw, Exception) import qualified SockeyeSymbolTable as ST import qualified SockeyeAST as SAST import qualified SockeyeParserAST as AST +data PrologBackendException + = MultiDimensionalQuantifierException + | NYIException String + deriving(Show) + +instance Exception PrologBackendException + {- The structure of the code generator should be very similar to the old Prolog Backend -} compile :: ST.Sockeye -> SAST.Sockeye -> String compile symTable ast = "Prolog backend not yet implemented" @@ -52,11 +61,12 @@ gen_nat_param_list pp = map AST.paramName pp instance PrologGenerator AST.Module where generate m = let name = "add_" ++ AST.moduleName m + mi = gen_module_info m p1 = gen_nat_param_list (AST.parameters m) bodyChecks = ["is_list(Id)"] nodeDecls = map gen_node_decls (AST.nodeDecls m) instDecls = map gen_inst_decls (AST.instDecls m) - bodyDefs = concat $ map gen_body_defs (AST.definitions m) + bodyDefs = concat $ map (gen_body_defs mi) (AST.definitions m) body = intercalate ",\n " $ bodyChecks ++ nodeDecls ++ instDecls ++ bodyDefs in name ++ stringify (["Id"] ++ p1) ++ " :- \n " ++ body ++ ".\n\n" @@ -72,6 +82,9 @@ instance PrologGenerator AST.Module where local_nodeid_name :: String -> String local_nodeid_name x = "ID_" ++ x +local_inst_name :: String -> String +local_inst_name x = "ID_" ++ x + -- Prefix tat as well? local_param_name :: String -> String local_param_name x = x @@ -139,21 +152,141 @@ map_spec_flatten def = case def of | map_spec <- maps, map_target <- (AST.mapTargets map_spec)] _ -> [] -gen_body_defs :: AST.Definition -> [String] -gen_body_defs x = case x of +data IterationState = IterationState + { + -- Map a sockeye name to a prolog variable + vars :: Map.Map String String + } + +data ModuleInfo = ModuleInfo + { + params :: [String] + } + +gen_module_info :: AST.Module -> ModuleInfo +gen_module_info x = + ModuleInfo { params = ["Id"] ++ params ++ nodes ++ insts} + where + insts = [local_inst_name $ AST.instName d | d <- AST.instDecls x] + params = (gen_nat_param_list $ AST.parameters x) + nodes = [local_nodeid_name $ AST.nodeName d | d <- AST.nodeDecls x] + +add_param :: ModuleInfo -> String -> ModuleInfo +add_param mi s = ModuleInfo { params = (params mi) ++ [s]} + +param_str :: ModuleInfo -> String +param_str mi = case params mi of + [] -> "" + li -> "," ++ intercalate "," [predicate "param" [p] | p <- li] + + +generate_conj :: ModuleInfo -> [AST.Definition] -> String +generate_conj mi li = + intercalate ",\n" $ concat [gen_body_defs mi inn | inn <- li] + +-- generate forall with a explicit variable name +forall_qual :: ModuleInfo -> String -> AST.NaturalSet -> [AST.Definition] -> String +forall_qual mi varName ns body = + "(" ++ + predicate "block_values" [generate ns, it_list] ++ "," ++ + "(" ++ + predicate "foreach" [it_var, it_list] + ++ param_str mi + ++ " do \n" ++ + body_str ++ "\n))" + where + id_var = "ID_" ++ varName + it_var = "IDT_" ++ varName + it_list = "IDL_" ++ varName + body_str = generate_conj (add_param mi it_var) body + +forall_uqr :: ModuleInfo -> AST.UnqualifiedRef -> String -> String +forall_uqr mi ref body_str = case (AST.refIndex ref) of + Nothing -> printf "(%s = %s, %s)" it_var id_var body_str + Just ai -> "(" ++ + predicate "block_values" [generate ai, it_list] ++ "," ++ + "(" ++ + predicate "foreach" [it_var, it_list] + ++ param_str mi + ++ " do " ++ + itid_var ++ " = " ++ list_prepend it_var id_var ++ "," ++ + body_str ++ "))" + where + id_var = "ID_" ++ (AST.refName ref) + it_var = "IDT_" ++ (AST.refName ref) + itid_var = "IDI_" ++ (AST.refName ref) + it_list = "IDL_" ++ (AST.refName ref) + +gen_bind_defs :: String -> [AST.PortBinding] -> String +gen_bind_defs uql_var binds = + let + dest bind = generate $ AST.boundNode bind + src bind = list_prepend (doublequotes $ AST.refName $ AST.boundPort $ bind) uql_var + pb bind = assert $ predicate "node_overlay" [src bind, dest bind] + preds = [pb bind | bind <- binds] + in intercalate "," preds + +gen_index :: AST.UnqualifiedRef -> String +gen_index uqr = + case (AST.refIndex uqr) of + Nothing -> local_nodeid_name $ AST.refName uqr + Just ai -> list_prepend (gen_ai ai) (local_nodeid_name $ AST.refName uqr) + where + gen_ai (AST.ArrayIndex _ ws) = list [gen_wildcard_simple w | w <- ws] + gen_wildcard_simple (AST.ExplicitSet _ ns) = gen_natural_set ns + gen_natural_set (ST.NaturalSet _ nrs) = gen_natural_ranges nrs + gen_natural_ranges [nr] = gen_ns_simple nr + gen_ns_simple (ST.SingletonRange _ base) = gen_exp_simple base + gen_exp_simple (AST.Variable _ vn) = "IDT_" ++ vn + gen_exp_simple (AST.Literal _ int) = show int + + + +gen_body_defs :: ModuleInfo -> AST.Definition -> [String] +gen_body_defs mi x = case x of (AST.Accepts _ n accepts) -> [(assert $ predicate "node_accept" [generate n, generate acc]) | acc <- accepts] (AST.Maps _ _ _) -> [(assert $ predicate "node_translate" [generate $ srcNode om, generate $ srcAddr om, generate $ targetNode om, generate $ targetAddr om]) | om <- map_spec_flatten x] (AST.Overlays _ src dest) -> [assert $ predicate "node_overlay" [generate src, generate dest]] - (AST.Instantiates _ i im args) -> [predicate ("add_" ++ im) [generate i]] - (AST.Binds _ inst binds) -> [assert $ predicate "node_overlay" [paramId, - (generate $ AST.boundNode bind)] | bind <- binds, let paramId = list_prepend (doublequotes $ AST.refName $ AST.boundPort bind) (generate inst)] - _ -> [] + -- (AST.Instantiates _ i im args) -> [forall_uqr mi i (predicate ("add_" ++ im) ["IDT_" ++ (AST.refName i)])] + (AST.Instantiates _ i im args) -> [ predicate ("add_" ++ im) [gen_index i] ] + -- (AST.Binds _ i binds) -> [forall_uqr mi i $ gen_bind_defs ("IDT_" ++ (AST.refName i)) binds] + (AST.Binds _ i binds) -> [gen_bind_defs (gen_index i) binds] + (AST.Forall _ varName varRange body) -> [forall_qual mi varName varRange body] + (AST.Converts _ _ _ ) -> throw $ NYIException "Converts" instance PrologGenerator AST.UnqualifiedRef where - generate uq = local_nodeid_name $ AST.refName uq + generate uq = case (AST.refIndex uq) of + Nothing -> local_nodeid_name $ AST.refName uq + Just ai -> list_prepend (generate ai) (local_nodeid_name $ AST.refName uq) + +-- Different modes of generating the wildcard set, either as block spec, or +-- to be used in array index generate_index +{- +generate_block :: AST.WildcardSet -> String +generate_block a = case a of + AST.ExplicitSet _ ns -> generate ns + AST.Wildcard _ -> "_" + + +generate_index_ns :: AST.NaturalSet -> String +generate_index_ns ns = "" + +generate_index :: AST.WildcardSet -> String +generate_index a = case a of + AST.ExplicitSet _ ns -> generate ns + AST.Wildcard _ -> "NYI!?" + -} + +instance PrologGenerator AST.WildcardSet where + generate a = case a of + AST.ExplicitSet _ ns -> generate ns + AST.Wildcard _ -> "NYI!?" + +instance PrologGenerator AST.ArrayIndex where + generate (AST.ArrayIndex _ wcs) = brackets $ intercalate "," [generate x | x <- wcs] instance PrologGenerator AST.MapSpec where generate ms = struct "map" [("src_block", generate (AST.mapAddr ms)), @@ -165,8 +298,8 @@ instance PrologGenerator AST.MapTarget where instance PrologGenerator AST.NodeReference where generate nr = case nr of - AST.InternalNodeRef _ nn -> local_nodeid_name $ AST.refName nn - AST.InputPortRef _ inst node -> list_prepend (doublequotes $ AST.refName node) (local_nodeid_name $ AST.refName inst) + AST.InternalNodeRef _ nn -> gen_index nn + AST.InputPortRef _ inst node -> list_prepend (doublequotes $ AST.refName node) (gen_index inst) instance PrologGenerator AST.AddressBlock where -- TODO: add properties @@ -176,14 +309,11 @@ instance PrologGenerator AST.Address where generate a = case a of AST.Address _ ws -> tuple $ map generate ws -instance PrologGenerator AST.WildcardSet where - generate a = case a of - AST.ExplicitSet _ ns -> generate ns - AST.Wildcard _ -> "_" + instance PrologGenerator AST.NaturalSet where generate a = case a of - AST.NaturalSet _ nrs -> intercalate "::" $ map generate nrs {- horribly wrong -} + AST.NaturalSet _ nrs -> list $ map generate nrs instance PrologGenerator AST.NaturalRange where generate nr = case nr of @@ -197,6 +327,7 @@ instance PrologGenerator AST.NaturalRange where instance PrologGenerator AST.NaturalExpr where generate nr = case nr of SAST.Constant _ v -> local_const_name v + SAST.Variable _ v -> "IDT_" ++ v SAST.Parameter _ v -> local_param_name v SAST.Literal _ n -> show n SAST.Addition _ a b -> "(" ++ generate a ++ ")+(" ++ generate b ++ ")" @@ -250,5 +381,41 @@ quotes = enclose "'" "'" doublequotes :: String -> String doublequotes = enclose "\"" "\"" + +nat_range_from :: AST.NaturalRange -> String +nat_range_from nr = case nr of + AST.SingletonRange _ b -> generate b + AST.LimitRange _ b _ -> generate b + AST.BitsRange _ _ _ -> "BitsRange NOT IMPLEMENTED" + +nat_range_to :: AST.NaturalRange -> String +nat_range_to nr = case nr of + AST.SingletonRange _ b -> generate b + AST.LimitRange _ _ l -> generate l + AST.BitsRange _ _ _ -> "BitsRange NOT IMPLEMENTED" + +-- Params are variables passed into the for body +for_body_inner :: [String] -> String -> String -> (Int, AST.NaturalRange) -> String +for_body_inner params itvar body itrange = + let + itvar_local = itvar ++ (show $ fst itrange) + from = nat_range_from $ (snd itrange) + to = nat_range_to $ (snd itrange) + for = printf "for(%s,%s,%s)" itvar_local from to :: String + paramf x = printf "param(%s)" x :: String + header = intercalate "," ([for] ++ map paramf params) + in printf "(%s \ndo\n %s \n)" header body + +enumerate = zip [0..] + +for_body :: [String] -> String -> AST.NaturalSet -> String -> String +for_body params itvar (AST.NaturalSet _ ranges) body = + foldl fbi body (enumerate ranges) + where + fbi = for_body_inner params itvar + + + + assert :: String -> String assert x = "assert" ++ parens x diff --git a/usr/skb/programs/decoding_net2.pl b/usr/skb/programs/decoding_net2.pl index 9098fb202d..441afa637e 100644 --- a/usr/skb/programs/decoding_net2.pl +++ b/usr/skb/programs/decoding_net2.pl @@ -10,8 +10,6 @@ :- module(decoding_net2). -:- export node_accept/2. -:- export node_translate/4. %% node_accept(InNodeId, InAddr :: block). @@ -23,6 +21,52 @@ %% node_overlay(InNodeId, OutNodeId). :- dynamic node_overlay/2. +:- export node_accept/2. +:- export node_translate/4. :- export struct(block(base,limit,props)). :- lib(ic). + +block_match(A, block{base: B, limit: L}) :- + B #=< A, + A #=< L. + +blocks_match_any(A, [B | Bs]) :- + block_match(A, B) ; blocks_match_any(A, Bs). + +blocks_match_any_ic(A, B) :- + blocks_match_any(A,B), + labeling([A]). + +:- export block_values/2. +% Union of blocks. [block{base:0,limit:5},block{base:33,limit:35}] -> 0,1,..,5,33,..,35 +block_values(Blocks, Values) :- + findall(X, blocks_match_any_ic(X, Blocks), Values). + + +blocks_match([], []). +blocks_match([A|As], [B|Bs]) :- + block_match(A,B), + blocks_match(As, Bs). + + +% For a ic constrained variable +blocks_match_ic(X,Bs) :- + length(Bs,LiLe), + length(X,LiLe), + blocks_match(X, Bs), + labeling(X). + +:- export block_crossp/2. +% Cross product of blocks +block_crossp(Blocks, Values) :- + findall(X, blocks_match_ic(X, Blocks), Values). + +%test :- +% addr_match( (0,0), (block{base:0, limit:0})). + + +% Ideas for the address thingy: +% findall(X, addr_match(X, Constraints), XLi), +% (forall(X,XLi) do .... ) +%