About the result of `main.py vscale reads path`

[DehengYang]

Hi,

Sorry for disturbing you here. I am quite interested in this project, and when I reproduce the pipesynth project by running main.py vscale reads path, the output of ./benchmark is as follows:

out/Vscale-reads-path.sy ( (define-fun path18-unary-545 ((i Microop)) Bool true) (define-fun path18-unary-546 ((i Microop)) Bool true) (define-fun path18-unary-547 ((i Microop)) Bool true) (define-fun path18-edge-548 ((i Microop) (j Microop)) Bool true) (define-fun path18-edge-549 ((i Microop) (j Microop)) Bool true) ) 3.18user 0.19system 0:03.37elapsed 100%CPU (0avgtext+0avgdata 48760maxresident)k 0inputs+0outputs (0major+9715minor)pagefaults 0swaps

Seemingly the pipesynth fail to synthesize the expected axiom. It would be much appreciated if any guidance could be provided.

I have made some attempts to figure out the underlying reason for the failure of pipesynth in this case. I debugged the project and observed that the grammer of edge_conjuncts in path_axiom of synth.py do not include the edge_exists (decode_execute i) (writeback i) and edge_exists (fetch i) (decode_execute i) template... Therefore, it fails to synthesize the reads axiom:

Axiom "Reads":
forall microops "i",
OnCore c i =>
IsAnyRead i =>
AddEdges [((i, (c, Fetch)),      (i, (c, DecodeExecute)),     "path");
          ((i, (c, DecodeExecute)),     (i, (c, Writeback)),    "path")].

I modified the synth.py file as follows:

(pipesynth) apr@apr:~/tools/PipeSynth-AEC$ git diff synth.py
diff --git a/synth.py b/synth.py
index 6f109df..55f103d 100644
--- a/synth.py
+++ b/synth.py
@@ -94,12 +94,12 @@ def conjunct(f, microop_t, arity, name):
     if arity == 1:
         def grammar(i: microop_t) -> bool:
             def non_terminals(b: bool):
-                return {b: [True] + [ff(i) for ff in f]}
+                return {b: [ff(i) for ff in f]}
             return non_terminals
     if arity == 2:
         def grammar(i: microop_t, j: microop_t) -> bool:
             def non_terminals(b: bool):
-                return {b: [True] + [ff(i, j) for ff in f]}
+                return {b: [ff(i, j) for ff in f]}
             return non_terminals
     if arity == 3:
         def grammar(i: microop_t, j: microop_t, k: microop_t) -> bool:
@@ -126,7 +126,7 @@ def edge_conjuncts(microop_t, allowed_edges, name, negated=False, unary=False):
                       {(lambda n, m: lambda i, j: ~add_edge(n(i), m(j)))(n, m), (lambda n, m: lambda i, j: ~add_edge(n(j), m(i
)))(n, m), (lambda n, m: lambda i, j: add_edge(n(i), m(j)))(n, m), (lambda n, m: lambda i, j: add_edge(n(j), m(i)))(n, m)}for n
, m in allowed_edges]]
     else:
         conjuncts = [conjunct(f, microop_t, 2, name) for f in
-                 [{(lambda n, m: lambda i, j: add_edge(n(i), m(j)))(n, m)}
+                 [{(lambda n, m: lambda i, j: add_edge(n(i), m(j)))(n, m), (lambda n, m: lambda i, j: add_edge(n(i), m(i)))(n, m), (lambda n, m: lambda i, j: add_edge(n(j), m(j)))(n, m)}
                   if unary else {(lambda n, m: lambda i, j: add_edge(n(i), m(j)))(n, m), (lambda n, m: lambda i, j: add_edge(n(j), m(i)))(n, m)} for n, m in allowed_edges]]
     return lambda a, b: forall(conjuncts, lambda i: i(a, b))

and the output turns into:

out/Vscale-reads-path.sy ( (define-fun path18-unary-545 ((i Microop)) Bool (is_read i)) (define-fun path18-unary-546 ((i Microop)) Bool (data_from_init_at_pa i)) (define-fun path18-unary-547 ((i Microop)) Bool (rmw_access i)) (define-fun path18-edge-548 ((i Microop) (j Microop)) Bool (edge_exists (fetch i) (decode_execute j))) (define-fun path18-edge-549 ((i Microop) (j Microop)) Bool (edge_exists (decode_execute i) (writeback i))) ) 3.04user 0.08system 0:03.12elapsed 100%CPU (0avgtext+0avgdata 50888maxresident)k 0inputs+0outputs (0major+10246minor)pagefaults 0swaps

which is more similar to the reads axiom.

Please kindly advise. Many thanks and wish you a great week.

Yours sincerely,

Deheng