diff --git a/circuits.ml b/circuits.ml index 408bd57119363596edf9abe9829fe2d632e7d819..6326b6cf63103f2760385b1d7f4aac568ab5368d 100644 --- a/circuits.ml +++ b/circuits.ml @@ -151,6 +151,8 @@ let convert_label = function | "PMOS" -> Gate Pmos | "WAIT" -> Gate Wait | "DISC" -> Disconnect + | "OR" -> Gate Or + | "AND" -> Gate And | "FORK" -> Gate Fork | "JOIN" -> Gate Join | x -> Gate (Box x) @@ -300,6 +302,7 @@ let rewrite_local rules ptg = while not (!inter == !older) do (* test physical equality in constant time *) older := !inter; inter := apply_local_rules rules !inter; + report "LOCAL REWRITE RULE APPLY" !inter; done; !inter;; diff --git a/lines.txt b/lines.txt index c8720c38eda82f8c452d63d260a0ac890fd64481..a9aa221d3ad505acb7d9eefea86a1ff3b39efe60 100644 --- a/lines.txt +++ b/lines.txt @@ -1,10 +1,6 @@ -let NAND1 = (2 | LOW) . (1 | NMOS) . NMOS in -let NAND2 = (HIGH | 1 | HIGH | 1) . (NMOS | NMOS) . JOIN in -let NAND = - link a0:a1 b0:b1 c1:c0 for - PAR - (a0: | b0:) . :c0 - (:a1 | :b1) . NAND1 . c1: - (:a1 | :b1) . NAND2 . c1: - END in -(HIGH | LOW) . NAND +link xO:xI yO:yI for +PAR + xO: + (:xI | :yI) . AND + (:yI | :xI) . OR . yO: +END diff --git a/parser.ml b/parser.ml index f01445c575927389c2e47922bc403aeb26b3a912..f883055606629120e75e87743b3d97fd57cc6850 100644 --- a/parser.ml +++ b/parser.ml @@ -166,6 +166,8 @@ let circuit_of_name = function | "DISC" -> const "DISC" 1 0 | "FORK" -> const "FORK" 1 2 | "JOIN" -> const "JOIN" 2 1 + | "AND" -> const "AND" 2 1 + | "OR" -> const "OR" 2 1 | x -> const x 1 1;; (**** THE GRAMMAR diff --git a/ptg.ml b/ptg.ml index 8af798afb6062c17dd6ce45be9469a979d39fc5d..f456da2afd52b611b61d3aa57c11e07d9cc3a753 100644 --- a/ptg.ml +++ b/ptg.ml @@ -97,6 +97,8 @@ type gate = | Join | Nmos | Pmos + | And + | Or | Box of string | Wait | Mux;; @@ -189,6 +191,8 @@ let string_of_gate = function | Pmos -> "P" | Box s -> "B " ^ s | Wait -> "W" + | And -> "AND" + | Or -> "OR" | Mux -> "M";; let rec string_of_value = function diff --git a/rewriting.ml b/rewriting.ml index 6ab264f1b17b79661531664dae921844b8a24d05..55ccb15c6e2e7e45eea7a96b65daf01a4055f3b4 100644 --- a/rewriting.ml +++ b/rewriting.ml @@ -220,7 +220,34 @@ let reduce_pmos inputs = with Match_failure _ -> NoOP;; -(* A small function that gives the lowest common + +(* The gate function for the AND gate *) +let reduce_and inputs = + try + let [a;b] = inputs in + match (a,b) with + | Some (Value Low), _ -> Result Low + | _, Some (Value Low) -> Result Low + | Some (Value High), Some (Value High) -> Result High + | _ -> NoOP + with + Match_failure _ -> NoOP;; + +(* The gate function for the OR gate *) +let reduce_or inputs = + try + let [a;b] = inputs in + match (a,b) with + | Some (Value High), _ -> Result High + | _ , Some (Value High) -> Result High + | Some (Value Low), Some (Value Low) -> Result Low + | _ -> NoOP + with + Match_failure _ -> NoOP;; + + +(* + * A small function that gives the lowest common * ancestor for two values of the lattice *) let combine_values v1 v2 = match (v1,v2) with @@ -264,6 +291,8 @@ let fun_of_gate = function | Nmos -> reduce_nmos | Pmos -> reduce_pmos | Join -> reduce_join + | And -> reduce_and + | Or -> reduce_or | _ -> (fun _ -> NoOP);; (**