add multi-event support

UnsignedByte · UnsignedByte · commit f27d970c818e · 2025-03-10T15:40:08.000Z
diff --git a/crates/filament/src/ir_passes/schedule/solve.rs b/crates/filament/src/ir_passes/schedule/solve.rs
@@ -1,8 +1,7 @@
 use super::CombDataflow;
 use crate::ir_visitor::{Action, Construct, Visitor, VisitorData};
-use core::time;
 use easy_smt::{self as smt, SExpr, SExprData};
-use fil_ir::{self as ir, AddCtx, Ctx, DisplayCtx, MutCtx, PortOwner};
+use fil_ir::{self as ir, AddCtx, Ctx, DisplayCtx, MutCtx, PortOwner, Subst};
 use fil_utils::{AttrCtx, CompNum};
 use itertools::Itertools;
 use std::{collections::HashMap, fs};
@@ -102,6 +101,128 @@ impl Solve {
             self.sol.assert(self.sol.not(equalities)).unwrap();
         }
     }
+
+    pub fn timesub_to_sexp(
+        &self,
+        ctx: &ir::Component,
+        event_bind: &ir::SparseInfoMap<ir::Event, SExpr>,
+        time_sub: &ir::TimeSub,
+    ) -> SExpr {
+        match time_sub {
+            fil_ir::TimeSub::Unit(idx) => {
+                self.expr_to_sexp(ctx, event_bind, *idx)
+            }
+            fil_ir::TimeSub::Sym { l, r } => {
+                let l = self.time_to_sexp(ctx, event_bind, *l);
+                let r = self.time_to_sexp(ctx, event_bind, *r);
+                self.sol.sub(l, r)
+            }
+        }
+    }
+
+    pub fn time_to_sexp(
+        &self,
+        ctx: &ir::Component,
+        event_bind: &ir::SparseInfoMap<ir::Event, SExpr>,
+        time: ir::TimeIdx,
+    ) -> SExpr {
+        let ir::Time { event, offset } = ctx.get(time);
+
+        let offset = self.expr_to_sexp(ctx, event_bind, *offset);
+        let event = *event_bind.get(*event);
+
+        self.sol.plus(event, offset)
+    }
+
+    /// Fold an expression to an SExpr
+    pub fn expr_to_sexp(
+        &self,
+        ctx: &ir::Component,
+        event_bind: &ir::SparseInfoMap<ir::Event, SExpr>,
+        expr: ir::ExprIdx,
+    ) -> SExpr {
+        match ctx.get(expr) {
+            fil_ir::Expr::Concrete(n) => self.sol.numeral(*n),
+            fil_ir::Expr::Bin { op, lhs, rhs } => {
+                let lhs = self.expr_to_sexp(ctx, event_bind, *lhs);
+                let rhs = self.expr_to_sexp(ctx, event_bind, *rhs);
+                match op {
+                    fil_ast::Op::Add => self.sol.plus(lhs, rhs),
+                    fil_ast::Op::Sub => self.sol.sub(lhs, rhs),
+                    fil_ast::Op::Mul => self.sol.times(lhs, rhs),
+                    fil_ast::Op::Div => self.sol.div(lhs, rhs),
+                    fil_ast::Op::Mod => self.sol.modulo(lhs, rhs),
+                }
+            }
+            fil_ir::Expr::If { cond, then, alt } => {
+                let cond = self.prop_to_sexp(ctx, event_bind, *cond);
+                let then = self.expr_to_sexp(ctx, event_bind, *then);
+                let alt = self.expr_to_sexp(ctx, event_bind, *alt);
+                self.sol.ite(cond, then, alt)
+            }
+            fil_ir::Expr::Fn { .. } => unreachable!(
+                "Constraints on scheduled components do not support custom function calls."
+            ),
+            fil_ir::Expr::Param(_) => {
+                unreachable!("Parameters should have been monomorphized")
+            }
+        }
+    }
+
+    /// Fold a proposition on events to an SExpr
+    pub fn prop_to_sexp(
+        &self,
+        ctx: &ir::Component,
+        event_bind: &ir::SparseInfoMap<ir::Event, SExpr>,
+        prop: ir::PropIdx,
+    ) -> SExpr {
+        match ctx.get(prop) {
+            fil_ir::Prop::True => self.sol.atom("true"),
+            fil_ir::Prop::False => self.sol.atom("false"),
+            fil_ir::Prop::Cmp(ir::CmpOp { op, lhs, rhs }) => {
+                let lhs = self.expr_to_sexp(ctx, event_bind, *lhs);
+                let rhs = self.expr_to_sexp(ctx, event_bind, *rhs);
+                match op {
+                    fil_ir::Cmp::Gt => self.sol.gt(lhs, rhs),
+                    fil_ir::Cmp::Gte => self.sol.gte(lhs, rhs),
+                    fil_ir::Cmp::Eq => self.sol.eq(lhs, rhs),
+                }
+            }
+            fil_ir::Prop::TimeCmp(ir::CmpOp { op, lhs, rhs }) => {
+                let lhs = self.time_to_sexp(ctx, event_bind, *lhs);
+                let rhs = self.time_to_sexp(ctx, event_bind, *rhs);
+                match op {
+                    fil_ir::Cmp::Gt => self.sol.gt(lhs, rhs),
+                    fil_ir::Cmp::Gte => self.sol.gte(lhs, rhs),
+                    fil_ir::Cmp::Eq => self.sol.eq(lhs, rhs),
+                }
+            }
+            fil_ir::Prop::TimeSubCmp(ir::CmpOp { op, lhs, rhs }) => {
+                let lhs = self.timesub_to_sexp(ctx, event_bind, lhs);
+                let rhs = self.timesub_to_sexp(ctx, event_bind, rhs);
+                match op {
+                    fil_ir::Cmp::Gt => self.sol.gt(lhs, rhs),
+                    fil_ir::Cmp::Gte => self.sol.gte(lhs, rhs),
+                    fil_ir::Cmp::Eq => self.sol.eq(lhs, rhs),
+                }
+            }
+            fil_ir::Prop::Not(idx) => {
+                self.sol.not(self.prop_to_sexp(ctx, event_bind, *idx))
+            }
+            fil_ir::Prop::And(idx, idx1) => self.sol.and(
+                self.prop_to_sexp(ctx, event_bind, *idx),
+                self.prop_to_sexp(ctx, event_bind, *idx1),
+            ),
+            fil_ir::Prop::Or(idx, idx1) => self.sol.or(
+                self.prop_to_sexp(ctx, event_bind, *idx),
+                self.prop_to_sexp(ctx, event_bind, *idx1),
+            ),
+            fil_ir::Prop::Implies(idx, idx1) => self.sol.imp(
+                self.prop_to_sexp(ctx, event_bind, *idx),
+                self.prop_to_sexp(ctx, event_bind, *idx1),
+            ),
+        }
+    }
 }
 
 impl Construct for Solve {
@@ -270,7 +391,9 @@ impl Visitor for Solve {
         // Intern all the constraints for the events
         let foreign_comp = data.ctx().get(inv.inst.comp(comp));
         for &constraint in foreign_comp.get_event_asserts() {
-            let prop = foreign_comp.get(constraint);
+            self.sol
+                .assert(self.prop_to_sexp(foreign_comp, &events, constraint))
+                .unwrap();
         }
 
         for pidx in inv.ports.iter() {
@@ -280,32 +403,26 @@ impl Visitor for Solve {
                     ir::PortOwner::Inv {
                         base: foreign_pidx, ..
                     },
-                live:
-                    ir::Liveness {
-                        range: ir::Range { start, end },
-                        ..
-                    },
                 ..
             } = port
             else {
                 unreachable!("Port {} is not owned by an invocation", pidx)
             };
 
-            // Find the events associated with the start and end of the port
-            let start_expr = *events.get(comp.get(*start).event);
-            let end_expr = *events.get(comp.get(*end).event);
-
-            let (start, end) = foreign_pidx.apply(
+            let (start_expr, end_expr, start, end) = foreign_pidx.apply(
                 |p, foreign_comp| {
                     let ir::Range { start, end } =
                         foreign_comp.get(p).live.range;
 
+                    let start_expr = *events.get(foreign_comp.get(start).event);
+                    let end_expr = *events.get(foreign_comp.get(end).event);
+
                     let start =
                         foreign_comp.get(start).offset.concrete(foreign_comp);
                     let end =
                         foreign_comp.get(end).offset.concrete(foreign_comp);
 
-                    (start, end)
+                    (start_expr, end_expr, start, end)
                 },
                 data.ctx(),
             );
diff --git a/crates/ir/src/utils/subst.rs b/crates/ir/src/utils/subst.rs
@@ -81,6 +81,15 @@ where
     }
 }
 
+impl<K, V> FromIterator<(K, V)> for Bind<K, V>
+where
+    K: Eq,
+{
+    fn from_iter<I: IntoIterator<Item = (K, V)>>(iter: I) -> Self {
+        Self(iter.into_iter().collect())
+    }
+}
+
 /// A substitution for a type `T` that contains type `K` inside it.
 /// Substitutions cannot be applied with a type that implements [Ctx].
 pub struct Subst<'a, T, K, V>
diff --git a/fud/filament.py b/fud/filament.py
@@ -7,7 +7,7 @@
 
 from fud import errors
 from fud.stages import Stage, SourceType, Source
-from fud.utils import shell, TmpDir,unwrap_or
+from fud.utils import shell, TmpDir, unwrap_or
 from enum import Enum
 
 
@@ -115,26 +115,32 @@ def transform_data(data_path, dir):
                 for i in range(len(data_dict[key])):
                     val = data_dict[key][i]
                     # if it is a string, check if it is in binary or hex
-                    if isinstance(val,str):
-                        if val.startswith('0b'): # binary format
+                    if isinstance(val, str):
+                        if val.startswith("0b"):  # binary format
                             binary_data = val[2:]
                             try:
-                                conv = int(binary_data,2)
+                                conv = int(binary_data, 2)
                             except ValueError:
-                                raise errors.InvalidNumericType("\"" + str(val) + "\"" + " in " + data)
-                        elif val.startswith('0x'): # hex format
+                                raise errors.InvalidNumericType(
+                                    '"' + str(val) + '"' + " in " + data
+                                )
+                        elif val.startswith("0x"):  # hex format
                             binary_data = val[2:]
                             try:
-                                conv = int(binary_data,16)
+                                conv = int(binary_data, 16)
                             except ValueError:
-                                raise errors.InvalidNumericType("\"" + str(val) + "\"" + " in " + data)
-                        else: # none of the above -> unsupported
-                            raise errors.InvalidNumericType("\"" + str(val) + "\"" + " in " + data)
-                    else: # already in decimal
+                                raise errors.InvalidNumericType(
+                                    '"' + str(val) + '"' + " in " + data
+                                )
+                        else:  # none of the above -> unsupported
+                            raise errors.InvalidNumericType(
+                                '"' + str(val) + '"' + " in " + data
+                            )
+                    else:  # already in decimal
                         conv = val
                     # update info in json
                     data_dict[key][i] = conv
-            json_obj = json.dumps(data_dict,indent=4)
+            json_obj = json.dumps(data_dict, indent=4)
             file_new.write(json_obj)
             return Path(file_new.name).resolve()
 
@@ -164,18 +170,15 @@ def mktmp() -> SourceType.Directory:
             return TmpDir()
 
         @builder.step()
-        def data_gen(file: SourceType.Path, dir: SourceType.Directory) -> SourceType.Stream:
+        def data_gen(
+            file: SourceType.Path, dir: SourceType.Directory
+        ) -> SourceType.Stream:
             """
             Generate data file in dir with binary/hex converted to decimal
             """
             data_transformed = transform_data(file, dir)
-            cmd = " ".join(
-                [
-                    "cat ",
-                    "{path}"
-                ]
-            )
-            return shell(cmd.format(path = data_transformed))
+            cmd = " ".join(["cat ", "{path}"])
+            return shell(cmd.format(path=data_transformed))
 
         @builder.step()
         def interface_gen(file: SourceType.Path) -> SourceType.Stream:
@@ -303,7 +306,7 @@ def read_vcd(dir: SourceType.String) -> SourceType.String:
 
         # Generate modified data file
         data_stream = data_gen(data, dir)
-        data_path = self.save_file(builder,data_stream,dir,"data_1.json")
+        data_path = self.save_file(builder, data_stream, dir, "data_1.json")
 
         # Run the program
         out = run(dir, interface_path, data_path)
diff --git a/tests/schedule/add-tree.expect b/tests/schedule/add-tree.expect
@@ -0,0 +1,2 @@
+{"out": {"0": [36]}, "cycles": 11}
+
diff --git a/tests/schedule/add-tree.fil.data b/tests/schedule/add-tree.fil.data
@@ -1,23 +1,26 @@
 {
     "in0": [
-        1,
+        1
     ],
     "in1": [
-        1,
+        2
+    ],
+    "in2": [
+        3
     ],
     "in3": [
-        1,
+        4
     ],
     "in4": [
-        1,
+        5
     ],
     "in5": [
-        1,
+        6
     ],
     "in6": [
-        1,
+        7
     ],
     "in7": [
-        1,
+        8
     ]
 }

Original file line number	Diff line number	Diff line change
`@@ -0,0 +1,2 @@`
	`1`	`+{"out": {"0": [36]}, "cycles": 11}`
	`2`	`+`