Add operators for DSP48E2 to Churchroad Interpreter (#79)

Closes #74 . --------- Co-authored-by: Gus Smith <[email protected]>
gussmith23 · Jul 15, 2024 · d3df077 · d3df077
1 parent 269416e
commit d3df077
Show file tree

Hide file tree

Showing 17 changed files with 4,320 additions and 77 deletions.
diff --git a/egglog_src/churchroad.egg b/egglog_src/churchroad.egg
@@ -12,14 +12,23 @@
 (datatype Op
   (And)
   (Add)
+  (Sub)
+  (Mul)
   (Or)
   (Xor)
   (Shr)
   ; Returns a bitvector of width 1.
   (Eq)
+  (Ne)
   ; Bitwise not.
   (Not)
+  ; Reduce operations.
+  (ReduceOr)
+  (ReduceAnd)
+  (ReduceXor)
   (LogicNot)
+  (LogicAnd)
+  (LogicOr)
   ; (Mux select-expr expr expr)
   (Mux)
 
@@ -39,7 +48,9 @@
 
   ; (Op1 (ZeroExtend bitwidth) expr)
   (ZeroExtend i64)
-  )
+  ; (Op1 (SignExtend bitwidth) expr)
+  (SignExtend i64)
+)
 
 (datatype Graph 
   ;;; Hole with a bitwidth.
@@ -138,9 +149,13 @@
 (relation AllBitwidthsMatch (Op))
 (AllBitwidthsMatch (And))
 (AllBitwidthsMatch (Add))
+(AllBitwidthsMatch (Sub))
+(AllBitwidthsMatch (Mul))
 (AllBitwidthsMatch (Or))
 (AllBitwidthsMatch (Xor))
 (AllBitwidthsMatch (Shr))
+;;; TODO(@ninehusky): don't we need this here?
+(AllBitwidthsMatch (Not))
 ; Have to write this one as a rule, unfortunately.
 (ruleset core)
 (rule ((Reg n)) ((AllBitwidthsMatch (Reg n))) :ruleset core)
@@ -149,13 +164,15 @@
 ;;; bitwidth is the indicated constant.
 (relation InputBitwidthsMatchOutputBitwidthConst (Op i64))
 (InputBitwidthsMatchOutputBitwidthConst (Eq) 1)
+(InputBitwidthsMatchOutputBitwidthConst (Ne) 1)
 
 ;;; Bitwise: Indicates that an op `(op a b ...)` can be written 
 ;;; `(concat (op a[0] b[0] ...) (op a[1] b[1] ...) ...)`.
 (relation Bitwise (Op))
 (Bitwise (And))
 (Bitwise (Or))
 (Bitwise (Xor))
+;;; (Bitwise (Not)) TODO(@ninehusky): don't we need this here?
 
 
 ;;; Typing judgements.
@@ -230,7 +247,7 @@
 (rule
   ((Op1 (Extract high low) expr)
    (HasType expr (Bitvector n))
-   (>= 0 low)
+   (>= low 0)
    (< high n))
   ((HasType (Op1 (Extract high low) expr) (Bitvector (+ 1 (- high low)))))
   :ruleset typing)
@@ -239,9 +256,34 @@
   ((HasType (Op1 (ZeroExtend bitwidth) expr) (Bitvector bitwidth)))
   :ruleset typing)
 (rule
-  ((Op1 (Reg init) expr)
-   (HasType expr (Bitvector n)))
-  ((HasType (Op1 (Reg init) expr) (Bitvector n)))
+  ((Op1 (LogicNot) expr))
+  ((HasType (Op1 (LogicNot) expr) (Bitvector 1)))
+  :ruleset typing)
+(rule
+  ((Op1 (ReduceOr) expr))
+  ((HasType (Op1 (ReduceOr) expr) (Bitvector 1)))
+  :ruleset typing)
+(rule
+  ((Op1 (ReduceAnd) expr))
+  ((HasType (Op1 (ReduceAnd) expr) (Bitvector 1)))
+  :ruleset typing)
+(rule
+  ((Op1 (ReduceXor) expr))
+  ((HasType (Op1 (ReduceXor) expr) (Bitvector 1)))
+  :ruleset typing)
+; TODO(@gussmith23) We need to decide whether Reg is Op1 or Op2
+(rule
+  ((Op2 (Reg init) clock-expr data-expr)
+   (HasType data-expr (Bitvector n)))
+  ((HasType (Op2 (Reg init) clock-expr data-expr) (Bitvector n)))
+  :ruleset typing)
+(rule
+  ((Op2 (LogicOr) a-expr b-expr))
+  ((HasType (Op2 (LogicOr) a-expr b-expr) (Bitvector 1)))
+  :ruleset typing)
+(rule
+  ((Op2 (LogicAnd) a-expr b-expr))
+  ((HasType (Op2 (LogicAnd) a-expr b-expr) (Bitvector 1)))
   :ruleset typing)
 
 ;;; Rewrites that are likely to expand the egraph.