Lines Matching refs:i2
18 let mux = new_definition (`mux`,"mux (cntl,i1:*,i2:*) = cntl => i1 | i2");;
22 "CMUX_IMP (cntl:^wire,cntlbar:^wire,i1:^wire,i2:^wire,o:^wire) =
29 Ptran (cntl,i2,w5) /\
30 Ntran (cntlbar,i2,w6)");;
34 "CMUXn_IMP n (cntl:^wire,cntlbar:^wire,i1:^bus,i2:^bus,o:^bus) =
37 (cntl,cntlbar,DEST_BUS i1 m,DEST_BUS i2 m,DEST_BUS o m)");;
41 "MUXn_IMP n (cntl:^wire,i1:^bus,i2:^bus,o:^bus) =
43 INV_IMP (cntl,cntlbar) /\ CMUXn_IMP n (cntl,cntlbar,i1,i2,o)");;
77 "!cntl cntlbar i1 i2 o.
78 CMUX_IMP (cntl,cntlbar,i1,i2,o)
83 (o t = mux (BoolAbs (cntl t),i1 t,i2 t))",
91 "!n cntl cntlbar i1 i2 o.
92 CMUXn_IMP n (cntl,cntlbar,i1,i2,o) /\
94 isBus n i2 /\
100 (o t = mux (BoolAbs (cntl t),i1 t,i2 t))",
123 "!n cntl i1 i2 o.
124 MUXn_IMP n (cntl,i1,i2,o) /\
126 isBus n i2 /\
129 !t. Def (cntl t) ==> (o t = mux (BoolAbs (cntl t),i1 t,i2 t))",