Added demo scripts

canal_demo.py

@@ -2,18 +2,21 @@
 
 num_tracks = 5
 
+# Create dictionary of input nodes
 input_nodes = {}
 for side in SwitchBoxSide:
     input_nodes[side] = []
     for track in range(num_tracks):
         input_nodes[side].append(SwitchBoxNode(0, 0, track, 16, side, SwitchBoxIO.SB_IN))
 
+# Create dictionary of output nodes
 output_nodes = {}
 for side in SwitchBoxSide:
     output_nodes[side] = []
     for track in range(num_tracks):
         output_nodes[side].append(SwitchBoxNode(0, 0, track, 16, side, SwitchBoxIO.SB_OUT))
 
+# Wire up input nodes to output nodes
 for track in range(num_tracks):
     for side_from in SwitchBoxSide:
         for side_to in SwitchBoxSide:
@@ -22,4 +25,6 @@
             input_node = input_nodes[side_from][track]
             output_node = output_nodes[side_to][track]
             print(f"Wire {input_node} -> {output_node}")
-            input_node.add_edge(output_node)
+            input_node.add_edge(output_node)
+
+

hwtypes_demo.py

@@ -0,0 +1,30 @@
+from hwtypes import BitVector, SMTBitVector
+
+def add3(a, b, c):
+    return a + b + c
+
+#'''
+# Python bitvector types
+x = BitVector[8](2)
+y = BitVector[8](5)
+z = BitVector[8](11)
+
+print(add3(x,y,z))
+#'''
+'''
+# SMT bitvector types
+x = SMTBitVector[8](2)
+y = SMTBitVector[8](5)
+z = SMTBitVector[8](11)
+
+print(add3(x,y,z))
+'''
+'''
+# SMT symbolic bitvector types
+x = SMTBitVector[8](name="a")
+y = SMTBitVector[8](name="b")
+z = SMTBitVector[8](name="c")
+
+print(add3(x,y,z))
+'''
+

peak_demo.py

@@ -0,0 +1,40 @@
+from peak import Peak
+import hwtypes as ht
+
+
+class Opcode(ht.Enum):
+    Add = 0
+    Sub = 1
+    Neg = 2
+
+Word = ht.BitVector[8]
+
+class ALU(Peak):
+    def __call__(self, inst: Opcode, i0: Word, i1: Word) -> Word:
+        if inst == Opcode.Add:
+            return i0 + i1
+        elif inst == Opcode.Sub:
+            return i0 - i1
+        else:
+            return -i0
+
+alu = ALU()
+
+i0 = Word(54) 
+i1 = Word(88)
+
+out = alu(Opcode.Add, i0, i1)
+
+assert out == i0 + i1
+
+'''
+import pysmt
+from pysmt import shortcuts as sc
+
+with sc.Solver('z3') as s:
+    s.add_assertion((out != i0 + i1).value)
+    if s.solve():
+        print("Counter example found")
+    else:
+        print("Verified add")
+'''