Added files for verification

Makefile

@@ -0,0 +1,28 @@
+### Nosyn User Receiver ###
+# ANVIL_FILE := /home/daoen/anvil_new/examples/verification/example_sender.anvil
+# SV_ANVIL   := /home/daoen/anvil_new/examples/verification/example_sender.sv
+# SV_USER    := /home/daoen/anvil_new/examples/verification/example_receiver.sv
+
+### Sender Dynamic user Sender ###
+# ANVIL_FILE := /home/daoen/anvil_new/examples/verification/syn1_example_receiver.anvil
+# SV_ANVIL   := /home/daoen/anvil_new/examples/verification/syn1_example_receiver.sv
+# SV_USER    := /home/daoen/anvil_new/examples/verification/syn1_example_sender.sv
+
+### Sender Dynamic user Receiver ###
+# ANVIL_FILE := /home/daoen/anvil_new/examples/verification/syn1_example1_sender.anvil
+# SV_ANVIL   := /home/daoen/anvil_new/examples/verification/syn1_example1_sender.sv
+# SV_USER    := /home/daoen/anvil_new/examples/verification/syn1_example1_receiver.sv
+
+### Recv Dynamic user Sender ###
+ANVIL_FILE := /home/daoen/anvil_new/examples/verification/syn2_example_receiver.anvil
+SV_ANVIL   := /home/daoen/anvil_new/examples/verification/syn2_example_receiver.sv
+SV_USER    := /home/daoen/anvil_new/examples/verification/syn2_example_sender.sv
+
+### Recv Dynamic user Receiver ###
+# ANVIL_FILE := /home/daoen/anvil_new/examples/verification/syn2_example1_sender.anvil
+# SV_ANVIL   := /home/daoen/anvil_new/examples/verification/syn2_example1_sender.sv
+# SV_USER    := /home/daoen/anvil_new/examples/verification/syn2_example1_receiver.sv
+
+.PHONY: assert
+assert:
+	dune exec ./bin/main.exe -- assert $(ANVIL_FILE) $(SV_ANVIL) $(SV_USER)

bin/main.ml

@@ -66,9 +66,15 @@ let compile_with_normal_output config =
       exit 1
   end
 
+
 let () =
-  let config = Anvil.Config.parse_args() in
-  if config.json_output then
-    compile_with_json_output config
-  else
-    compile_with_normal_output config
+  (* match --assert command *)
+  match Array.to_list Sys.argv with
+  | _ :: "assert" :: _ ->
+    Anvil.CompileDriver.verification_run Sys.argv
+  | _ ->
+      let config = Anvil.Config.parse_args () in
+      if config.json_output then
+        compile_with_json_output config
+      else
+        compile_with_normal_output config

examples/verification/Makefile

@@ -0,0 +1,35 @@
+MODULE_NAME ?= top
+TOP_MODULE ?= $(MODULE_NAME)
+
+ifdef TRACE_ON
+	VERILATOR_FLAGS ?= --top $(MODULE_NAME) -j 1 --trace --trace-structs
+else
+	VERILATOR_FLAGS ?= --top $(MODULE_NAME) -j 1
+endif
+
+TEST_DRIVER = sim_main.cpp
+
+all: obj_dir/V$(MODULE_NAME)
+
+.PHONY: run clean
+
+ifdef LTOFF
+    ANVIL_FLAGS = -- -disable-lt-checks
+else
+    ANVIL_FLAGS = -- -O 0 -verbose
+endif
+
+$(MODULE_NAME).anvil.sv: $(MODULE_NAME).anvil
+	dune exec anvil $(ANVIL_FLAGS) $< > $@
+
+obj_dir/V$(MODULE_NAME): $(MODULE_NAME)_driver.cpp $(MODULE_NAME).anvil.sv
+	verilator --cc --exe --build $(VERILATOR_FLAGS) $^
+
+$(MODULE_NAME)_driver.cpp: $(TEST_DRIVER)
+	sed "s/Vtop/V$(MODULE_NAME)/g" $< > $@
+
+run: obj_dir/V$(MODULE_NAME)
+	@ $< $(TIMEOUT)
+
+clean:
+	rm -rf *obj_dir *.anvil.sv *_driver.cpp

examples/verification/example_sender.anvil

@@ -0,0 +1,13 @@
+chan ch {
+    left req: (logic[8]@#2)
+}
+
+proc example_sender(ep: right ch) {
+    reg r : logic[8];
+    loop {
+        set r := *r + 8'b1 >>
+        dprint "Data Send = %d" (*r);
+        send ep.req (*r) >>
+        cycle 2
+    }
+}

examples/verification/syn1_example1_sender.anvil

@@ -0,0 +1,13 @@
+chan ch {
+    left req: (logic[8]@#2) @#3 - @dyn
+}
+
+proc syn1_example1_sender(ep: right ch) {
+    reg r : logic[8];
+    loop {
+        cycle 2 >>
+        set r := *r + 8'b1 >>
+        dprint "Data Send = %d" (*r);
+        send ep.req (*r)
+    }
+}

examples/verification/syn1_example_receiver.anvil

@@ -0,0 +1,15 @@
+// Sender: dynamic, Receiver: static → Valid signal required from the sender
+
+chan ch {
+    left res : (logic[8]@#3) @#1 - @dyn
+}
+
+proc syn1_example_receiver (endp : left ch) {
+    reg data : logic[8];
+    loop {
+        let data = recv endp.res >>
+        dprint "Data Receive: %d" (data) >>
+        cycle 1 
+    }
+}
+

examples/verification/syn2_example1_sender.anvil

@@ -0,0 +1,14 @@
+
+chan ch {
+    left req : (logic[8]@#2) @dyn - @#3
+}
+
+proc syn2_example1_sender (endp : right ch) {
+    reg r : logic[8];
+    loop {
+        cycle 1 >>
+        set r := *r + 8'b1 >>
+        dprint "Data Send = %d" (*r);
+        send endp.req (*r)
+    }
+}

examples/verification/syn2_example_receiver.anvil

@@ -0,0 +1,13 @@
+
+chan ch {
+    left req : (logic[8]@#1) @dyn - @#2
+}
+
+proc syn2_example_receiver (endp : left ch) {
+    loop {
+        cycle 2 >>
+        let r = recv endp.req >>
+        dprint "Value = %d" (r)
+    }
+}
+

lib/assertName.ml

@@ -0,0 +1,21 @@
+(* lib/assertName.ml *)
+
+let anvil_sv_ref : string option ref = ref None
+let user_sv_ref : string option ref = ref None
+
+let generate (anvil_sv:string) (user_sv:string) : unit =
+  anvil_sv_ref := Some anvil_sv;
+  user_sv_ref := Some user_sv
+
+let strip_sv_name (path : string) : string =
+  path |> Filename.basename |> Filename.remove_extension
+
+let user_sv () : string =
+  match !user_sv_ref with
+  | Some s -> strip_sv_name s
+  | None -> failwith "AssertName.sender: not initialised (call AssertName.generate first)"
+
+let anvil_sv () : string =
+  match !anvil_sv_ref with
+  | Some s -> s
+  | None -> failwith "AssertName.receiver: not initialised (call AssertName.generate first)"

lib/assertName.mli

@@ -0,0 +1,9 @@
+
+
+val generate : string -> string -> unit
+
+val strip_sv_name : string -> string
+
+val user_sv : unit -> string
+
+val anvil_sv : unit -> string