From cd08955899278d1ae056baf9ce93c3255d1058a7 Mon Sep 17 00:00:00 2001 From: Dao En Date: Fri, 20 Feb 2026 03:21:38 +0800 Subject: [PATCH] Added files for verification --- Makefile | 28 ++ bin/main.ml | 16 +- examples/verification/Makefile | 35 ++ examples/verification/example_sender.anvil | 13 + .../verification/syn1_example1_sender.anvil | 13 + .../verification/syn1_example_receiver.anvil | 15 + .../verification/syn2_example1_sender.anvil | 14 + .../verification/syn2_example_receiver.anvil | 13 + lib/assertName.ml | 21 + lib/assertName.mli | 9 + lib/codegen.ml | 418 ++++++++++++++++++ lib/codegen.mli | 6 + lib/codegenPort.ml | 74 +++- lib/codegenPort.mli | 14 + lib/compileDriver.ml | 133 ++++++ lib/compileDriver.mli | 2 + properties/nosyn_user_receiver.svh | 16 + properties/nosyn_user_sender.svh | 20 + properties/syn_recv_dynamic_user_receiver.svh | 8 + properties/syn_recv_dynamic_user_sender.svh | 3 + properties/syn_send_dynamic_user_receiver.svh | 3 + properties/syn_send_dynamic_user_sender.svh | 8 + 22 files changed, 876 insertions(+), 6 deletions(-) create mode 100644 Makefile create mode 100644 examples/verification/Makefile create mode 100644 examples/verification/example_sender.anvil create mode 100644 examples/verification/syn1_example1_sender.anvil create mode 100644 examples/verification/syn1_example_receiver.anvil create mode 100644 examples/verification/syn2_example1_sender.anvil create mode 100644 examples/verification/syn2_example_receiver.anvil create mode 100644 lib/assertName.ml create mode 100644 lib/assertName.mli create mode 100644 properties/nosyn_user_receiver.svh create mode 100644 properties/nosyn_user_sender.svh create mode 100644 properties/syn_recv_dynamic_user_receiver.svh create mode 100644 properties/syn_recv_dynamic_user_sender.svh create mode 100644 properties/syn_send_dynamic_user_receiver.svh create mode 100644 properties/syn_send_dynamic_user_sender.svh diff --git a/Makefile b/Makefile new file mode 100644 index 0000000..50b76cd --- /dev/null +++ b/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) \ No newline at end of file diff --git a/bin/main.ml b/bin/main.ml index 19aef72..2644d77 100644 --- a/bin/main.ml +++ b/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 \ No newline at end of file diff --git a/examples/verification/Makefile b/examples/verification/Makefile new file mode 100644 index 0000000..b44f3cf --- /dev/null +++ b/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 diff --git a/examples/verification/example_sender.anvil b/examples/verification/example_sender.anvil new file mode 100644 index 0000000..d232599 --- /dev/null +++ b/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 + } +} diff --git a/examples/verification/syn1_example1_sender.anvil b/examples/verification/syn1_example1_sender.anvil new file mode 100644 index 0000000..9213022 --- /dev/null +++ b/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) + } +} diff --git a/examples/verification/syn1_example_receiver.anvil b/examples/verification/syn1_example_receiver.anvil new file mode 100644 index 0000000..424dacf --- /dev/null +++ b/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 + } +} + diff --git a/examples/verification/syn2_example1_sender.anvil b/examples/verification/syn2_example1_sender.anvil new file mode 100644 index 0000000..fc46d77 --- /dev/null +++ b/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) + } +} diff --git a/examples/verification/syn2_example_receiver.anvil b/examples/verification/syn2_example_receiver.anvil new file mode 100644 index 0000000..9ad3927 --- /dev/null +++ b/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) + } +} + diff --git a/lib/assertName.ml b/lib/assertName.ml new file mode 100644 index 0000000..696a33f --- /dev/null +++ b/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)" diff --git a/lib/assertName.mli b/lib/assertName.mli new file mode 100644 index 0000000..ab4886f --- /dev/null +++ b/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 \ No newline at end of file diff --git a/lib/codegen.ml b/lib/codegen.ml index ec46199..da54437 100644 --- a/lib/codegen.ml +++ b/lib/codegen.ml @@ -428,3 +428,421 @@ let generate (out : out_channel) let printer = CodegenPrinter.create out 2 in List.iter (codegen_proc printer graphs) graphs.event_graphs + +(*Add for Verification Run*) +let verification_codegen_ports printer (graphs : event_graph_collection) + (endpoints : endpoint_def list) = + let port_list = CodegenPort.gather_ports graphs.channel_classes endpoints in + let rec print_port_list port_list = + match port_list with + | [] -> () + | port :: [] -> + CodegenPort.assertformat graphs.typedefs graphs.macro_defs port |> Printf.sprintf "%s;" |> CodegenPrinter.print_line printer + | port :: port_list' -> + CodegenPort.assertformat graphs.typedefs graphs.macro_defs port |> Printf.sprintf "%s;" |> CodegenPrinter.print_line printer; + print_port_list port_list' + in + print_port_list port_list; + port_list + +let verification_codegen_instantiations printer (graphs : event_graph_collection) + (endpoints : endpoint_def list) = + let port_list = CodegenPort.gather_ports graphs.channel_classes endpoints in + CodegenPrinter.print_line printer ".clk_i(clk_i),"; + CodegenPrinter.print_line printer ".rst_ni(rst_ni),"; + let rec print_port_list port_list = + match port_list with + | [] -> () + | port :: [] -> + let s = CodegenPort.instanformat port in + Printf.sprintf ".%s (%s)" s s |> CodegenPrinter.print_line printer + | port :: port_list' -> + let s = CodegenPort.instanformat port in + Printf.sprintf ".%s (%s)," s s |> CodegenPrinter.print_line printer; + print_port_list port_list' + in + print_port_list port_list; + port_list + +let verification_codegen_proc printer (graphs : EventGraph.event_graph_collection) (g : proc_graph) = + + (* Match synchronisation and module direction *) + let assertion_declare_states (msg : message_def) (d : Lang.endpoint_direction) : string = + match (msg.send_sync, msg.recv_sync) with + | (Dynamic, Dynamic) -> + (match d with + | Left -> "typedef enum logic [1:0] {WAIT_REQ, WAIT_ACK, DROP_VALID} state_t;" + | Right -> "typedef enum logic [1:0] {WAIT_ACK, DROP_VALID} state_t;") + | (_, Dynamic) -> "typedef enum logic [1:0] {WAIT_ACK, DROP_ACK} state_t;" + | (Dynamic, _) -> "typedef enum logic [1:0] {WAIT_REQ, DROP_VALID} state_t;" + | _ -> "None" + in + + (* Print the input, output ports *) + let name_assert = g.name ^ "_assert" in + Printf.sprintf "module %s (\n input clk_i, \n input rst_ni \n);" name_assert |> CodegenPrinter.print_line printer ~lvl_delta_post:1; + + (* Check the lifetime contract *) + let number_of_lifetime_cycles (d : Lang.delay_pat_chan_local) : int option = + match d with + | `Cycles n -> Some n + | _ -> None + in + + (* Print the lifetime contract *) + let print_declared_cycle_bound (ep : Lang.endpoint_def) = + let cc = MessageCollection.lookup_channel_class graphs.channel_classes ep.channel_class |> Option.get in + let msg_def = List.hd cc.messages in + let msg_def = ParamConcretise.concretise_message cc.params ep.channel_params msg_def in + match msg_def.sig_types with + | [] -> Printf.printf "parameter int counter = #;\n" + | stype0 :: _ -> + match number_of_lifetime_cycles stype0.lifetime.e with + | Some n -> Printf.printf "parameter int counter = %d;\n" n + | None -> Printf.printf "parameter int counter = #;\n" in + List.iter print_declared_cycle_bound g.messages.args; + + (* Print declaration of the FSM states *) + List.iter (fun (ep : Lang.endpoint_def) -> + let cc = MessageCollection.lookup_channel_class graphs.channel_classes ep.channel_class |> Option.get in + let msg_def = List.hd cc.messages in + let msg_def = ParamConcretise.concretise_message cc.params ep.channel_params msg_def in + CodegenPrinter.print_line printer (assertion_declare_states msg_def ep.dir) + ) g.messages.args; + + (* Print the shadow logics *) + Printf.sprintf "state_t state_prev, state_curr, state_next;" |> CodegenPrinter.print_line printer; + Printf.sprintf "int counter;" |> CodegenPrinter.print_line printer; + + (* Print the declarations of ports, ack, valid, data ... *) + let _ = verification_codegen_ports printer graphs g.messages.args in + ( + match g.extern_module, g.proc_body with + | _ -> + let initEvents = fst @@ List.hd g.threads in + codegen_endpoints printer graphs initEvents; + ); + + (* Retreive the user module name *) + let s = AssertName.user_sv () in + (* Print user module instantiation *) + Printf.sprintf "%s user_sv (" s |> CodegenPrinter.print_line printer; + let _ = verification_codegen_instantiations printer graphs g.messages.args in + ( + match g.extern_module, g.proc_body with + | _ -> + let initEvents = fst @@ List.hd g.threads in + codegen_endpoints printer graphs initEvents; + ); + CodegenPrinter.print_line printer ~lvl_delta_pre:(-1) ~lvl_delta_post:1 ");"; + + (* Print anvil module instantiation *) + Printf.sprintf "%s anvil_sv (" g.name |> CodegenPrinter.print_line printer; + let _ = verification_codegen_instantiations printer graphs g.messages.args in + ( + match g.extern_module, g.proc_body with + | _ -> + let initEvents = fst @@ List.hd g.threads in + codegen_endpoints printer graphs initEvents; + ); + CodegenPrinter.print_line printer ~lvl_delta_pre:(-1) ~lvl_delta_post:1 ");"; + + (* to check if there is only one signal, will modify this *) + let only_one default = function + | x :: _ -> x + | [] -> default + in + let valid_name = only_one "" (CodegenPort.valid_port_names graphs.channel_classes g.messages.args) in + let ack_name = only_one "" (CodegenPort.ack_port_names graphs.channel_classes g.messages.args) in + let datas = only_one "" (CodegenPort.data_port_names graphs.channel_classes g.messages.args) in + + (* Fixed FSM always_ff block *) + let ff_block (state1 : string) (state2 : string): string = + String.concat "\n" [ + Printf.sprintf "always_ff @(posedge clk_i or negedge rst_ni) begin"; + Printf.sprintf " if (!rst_ni) begin"; + Printf.sprintf " state_curr <= %s;" state1; + Printf.sprintf " counter <= 0;"; + Printf.sprintf " end else begin"; + Printf.sprintf " state_prev <= state_curr;"; + Printf.sprintf " state_curr <= state_next;"; + Printf.sprintf ""; + Printf.sprintf " if (state_curr == %s || counter != 0) begin" state2; + Printf.sprintf " counter <= counter + 1;"; + Printf.sprintf " end"; + Printf.sprintf ""; + Printf.sprintf " if (counter == N-1) begin"; + Printf.sprintf " counter <= 0;"; + Printf.sprintf " end"; + Printf.sprintf " end"; + Printf.sprintf "end"; + ] + in + + (* FSM always_comb block for sender *) + let comb_block_nosyn_sender (valid_name : string) (ack_name : string) : string = + String.concat "\n" [ + Printf.sprintf "always_comb begin"; + Printf.sprintf " case (state_curr)"; + Printf.sprintf ""; + Printf.sprintf " WAIT_REQ: begin"; + Printf.sprintf " if (%s) begin" valid_name; + Printf.sprintf " state_next = WAIT_ACK;"; + Printf.sprintf " end else begin"; + Printf.sprintf " state_next = WAIT_REQ;"; + Printf.sprintf " end"; + Printf.sprintf " end"; + Printf.sprintf ""; + Printf.sprintf " WAIT_ACK: begin"; + Printf.sprintf " if (%s) begin" ack_name; + Printf.sprintf " state_next = DROP_VALID;"; + Printf.sprintf " end else begin"; + Printf.sprintf " state_next = WAIT_ACK;"; + Printf.sprintf " end"; + Printf.sprintf " end"; + Printf.sprintf ""; + Printf.sprintf " DROP_VALID: begin"; + Printf.sprintf " state_next = WAIT_REQ;"; + Printf.sprintf " end"; + Printf.sprintf ""; + Printf.sprintf " default: state_next = WAIT_REQ;"; + Printf.sprintf " endcase"; + Printf.sprintf "end"; + ] + in + + (* FSM always_comb block for receiver *) + let comb_block_nosyn_receiver (ack_name : string) : string = + String.concat "\n" [ + Printf.sprintf "always_comb begin"; + Printf.sprintf " case (state_curr)"; + Printf.sprintf ""; + + Printf.sprintf " WAIT_ACK: begin"; + Printf.sprintf " if (%s) begin" ack_name; + Printf.sprintf " state_next = DROP_VALID;"; + Printf.sprintf " end else begin"; + Printf.sprintf " state_next = WAIT_ACK;"; + Printf.sprintf " end"; + Printf.sprintf " end"; + Printf.sprintf ""; + + Printf.sprintf " DROP_VALID: begin"; + Printf.sprintf " state_next = WAIT_ACK;"; + Printf.sprintf " end"; + Printf.sprintf ""; + + Printf.sprintf " default: state_next = WAIT_ACK;"; + + Printf.sprintf " endcase"; + Printf.sprintf "end"; + ] + in + + let comb_block_syn (state1 : string) (state2 : string) (signal : string) : string = + String.concat "\n" [ + Printf.sprintf "always_comb begin"; + Printf.sprintf " case (state_curr)"; + Printf.sprintf ""; + + Printf.sprintf " %s: begin" state1; + Printf.sprintf " if (%s) begin" signal; + Printf.sprintf " state_next = %s;" state2; + Printf.sprintf " end else begin"; + Printf.sprintf " state_next = %s;" state1; + Printf.sprintf " end"; + Printf.sprintf " end"; + Printf.sprintf ""; + + Printf.sprintf " %s: begin" state2; + Printf.sprintf " state_next = %s;" state1; + Printf.sprintf " end"; + Printf.sprintf ""; + + Printf.sprintf " default: state_next = %s;" state1; + + Printf.sprintf " endcase"; + Printf.sprintf "end"; + ] + in + + (* match the synchronisation and direction to print the correct fsm and assertion properties *) + let print_fsm_assertion (msg : message_def) (d : Lang.endpoint_direction) (valid_name : string) (ack_name : string) (data : string): string = + match (msg.send_sync, msg.recv_sync) with + | (Dynamic, Dynamic) -> + (match d with + | Left -> + let block = ff_block "WAIT_REQ" "DROP_VALID" in + block + |> String.split_on_char '\n' + |> List.iter (fun line -> + CodegenPrinter.print_line printer line ~lvl_delta_post:0 + ); + + let block = comb_block_nosyn_sender valid_name ack_name in + block + |> String.split_on_char '\n' + |> List.iter (fun line -> + CodegenPrinter.print_line printer line ~lvl_delta_post:0 + ); + String.concat "\n" [ + Printf.sprintf "`include \"./properties/nosyn_user_sender.svh\"\n"; + Printf.sprintf "assert property (data_stable_valid_high(%s, state_curr, %s))" valid_name data; + Printf.sprintf "else $error(\"Assertion Failed: data_stable_valid_high\");\n"; + Printf.sprintf "assert property (valid_high_until_ack_high(%s, state_curr))" valid_name; + Printf.sprintf "else $error(\"Assertion Failed: valid_high_until_ack_high\");\n"; + Printf.sprintf "assert property (ack_high_valid_low(%s, state_curr, %s))" valid_name ack_name; + Printf.sprintf "else $error(\"Assertion Failed: ack_high_valid_low\");\n"; + Printf.sprintf "assert property (data_stable_N_cycles_after_ack_high(state_curr, counter, %s))" data; + Printf.sprintf "else $error(\"Assertion Failed: data_stable_N_cycles_after_ack_high\");\n"; + Printf.sprintf "assert property (wait_req_ack_low(state_curr, %s))" ack_name; + Printf.sprintf "else $error(\"Assertion Failed: wait_req_ack_low\');\n"; + ] + | Right -> + let block = ff_block "WAIT_ACK" "DROP_VALID" in + block + |> String.split_on_char '\n' + |> List.iter (fun line -> + CodegenPrinter.print_line printer line ~lvl_delta_post:0 + ); + + let block = comb_block_nosyn_receiver ack_name in + block + |> String.split_on_char '\n' + |> List.iter (fun line -> + CodegenPrinter.print_line printer line ~lvl_delta_post:0 + ); + String.concat "\n" [ + Printf.sprintf "`include \"./properties/nosyn_user_receiver.svh\"\n"; + Printf.sprintf "assert property (ack_low_when_valid_high(state_curr, %s, %s))" valid_name ack_name; + Printf.sprintf "else $error(\"Assertion Failed: ack_low_when_valid_high\");\n"; + Printf.sprintf "assert property (ack_high_valid_low(state_curr, %s, %s))" valid_name ack_name; + Printf.sprintf "else $error(\"Assertion Failed: ack_high_valid_low\");\n"; + Printf.sprintf "assert property (ack_low_after_handshake(state_prev, %s))" ack_name; + Printf.sprintf "else $error(\"Assertion Failed: ack_low_after_handshake\");\n"; + Printf.sprintf "assert property (property data_stable_N_cycles_after_ack_high (state_curr, counter, %s))" data; + Printf.sprintf "else $error(\"Assertion Failed: property data_stable_N_cycles_after_ack_high\");\n"; + ] ) + | (_, Dynamic) -> + (match d with + | Left -> + let block = ff_block "WAIT_ACK" "DROP_ACK" in + block + |> String.split_on_char '\n' + |> List.iter (fun line -> + CodegenPrinter.print_line printer line ~lvl_delta_post:0 + ); + + let block = comb_block_syn "WAIT_ACK" "DROP_ACK" ack_name in + block + |> String.split_on_char '\n' + |> List.iter (fun line -> + CodegenPrinter.print_line printer line ~lvl_delta_post:0 + ); + String.concat "\n" [ + Printf.sprintf "`include \"./properties/syn_recv_dynamic_user_sender.svh\"\n"; + Printf.sprintf "assert property (data_stable_N_cycles (state_curr, counter, %s))" data; + Printf.sprintf "else $error(\"Assertion Failed: data_stable_N_cycles\");\n"; + ] + | Right -> + let block = ff_block "WAIT_ACK" "DROP_ACK" in + block + |> String.split_on_char '\n' + |> List.iter (fun line -> + CodegenPrinter.print_line printer line ~lvl_delta_post:0 + ); + + let block = comb_block_syn "WAIT_ACK" "DROP_ACK" ack_name in + block + |> String.split_on_char '\n' + |> List.iter (fun line -> + CodegenPrinter.print_line printer line ~lvl_delta_post:0 + ); + String.concat "\n" [ + Printf.sprintf "`include \"syn_recv_dynamic_user_receiver.svh\"\n"; + Printf.sprintf "assert property (ack_low_during_DROP_ACK (state_curr, %s))" ack_name; + Printf.sprintf "else $error(\"Assertion Failed: ack_low_during_DROP_ACK\");\n"; + Printf.sprintf "assert property (data_stable_N_cycles (state_curr, counter, %s))" data; + Printf.sprintf "else $error(\"Assertion Failed: data_stable_N_cycles\");\n"; + ]) + | (Dynamic, _) -> + (match d with + | Left -> + let block = ff_block "WAIT_REQ" "DROP_VALID" in + block + |> String.split_on_char '\n' + |> List.iter (fun line -> + CodegenPrinter.print_line printer line ~lvl_delta_post:0 + ); + + let block = comb_block_syn "WAIT_REQ" "DROP_VALID" valid_name in + block + |> String.split_on_char '\n' + |> List.iter (fun line -> + CodegenPrinter.print_line printer line ~lvl_delta_post:0 + ); + String.concat "\n" [ + Printf.sprintf "`include \"./properties/syn_send_dynamic_user_sender.svh\"\n"; + Printf.sprintf "assert property (data_stable_N_cycles (state_curr, counter, %s))" data; + Printf.sprintf "else $error(\"Assertion Failed: data_stable_N_cycles\");\n"; + Printf.sprintf "assert property (valid_low_during_DROP_VALID (state_curr, %s)" valid_name; + Printf.sprintf "else $error(\"Assertion Failed: data_stable_N_cycles\");\n"; + ] + | Right -> + let block = ff_block "WAIT_REQ" "DROP_VALID" in + block + |> String.split_on_char '\n' + |> List.iter (fun line -> + CodegenPrinter.print_line printer line ~lvl_delta_post:0 + ); + + let block = comb_block_syn "WAIT_REQ" "DROP_VALID" valid_name in + block + |> String.split_on_char '\n' + |> List.iter (fun line -> + CodegenPrinter.print_line printer line ~lvl_delta_post:0 + ); + String.concat "\n" [ + Printf.sprintf "`include \"./properties/syn_send_dynamic_user_receiver.svh\"\n"; + Printf.sprintf "assert property (data_stable_N_cycles (state_curr, counter, %s))" data; + Printf.sprintf "else $error(\"Assertion Failed: data_stable_N_cycles\");\n"; + ]) + | _ -> "None" + in + List.iter (fun (ep : Lang.endpoint_def) -> + let cc = MessageCollection.lookup_channel_class graphs.channel_classes ep.channel_class |> Option.get in + let msg_def = List.hd cc.messages in + let msg_def = ParamConcretise.concretise_message cc.params ep.channel_params msg_def in + CodegenPrinter.print_line printer (print_fsm_assertion msg_def ep.dir valid_name ack_name datas) + ) g.messages.args; + + + CodegenPrinter.print_line printer ~lvl_delta_pre:(-1) "endmodule" + +let verification_generate_extern_import out file_name = + In_channel.with_open_text file_name + (fun in_channel -> + let eof = ref false in + while not !eof do + match In_channel.input_line in_channel with + | Some line -> + Out_channel.output_string out line; + Out_channel.output_char out '\n' + | None -> eof := true + done + ) + +let verification_generate (out : out_channel) + (config : Config.compile_config) + (graphs : EventGraph.event_graph_collection) : unit = + if config.verbose then ( + Printf.eprintf "==== CodeGen Details ====\n"; + List.iter (fun (pg : proc_graph) -> + List.iter (fun (g, _) -> + EventGraphOps.print_dot_graph g Out_channel.stderr + ) pg.threads + ) graphs.event_graphs; + ); + let printer = CodegenPrinter.create out 2 in + List.iter (verification_codegen_proc printer graphs) graphs.event_graphs + diff --git a/lib/codegen.mli b/lib/codegen.mli index 8569b1d..fc7c8ff 100644 --- a/lib/codegen.mli +++ b/lib/codegen.mli @@ -10,3 +10,9 @@ val generate_preamble : out_channel -> unit (** Generate code for a {!type:EventGraph.event_graph_collection} to a specified output channel. *) val generate : out_channel -> Config.compile_config -> EventGraph.event_graph_collection -> unit + + +val verification_generate_extern_import : out_channel -> string -> unit + +val verification_generate : out_channel -> Config.compile_config -> EventGraph.event_graph_collection -> unit + diff --git a/lib/codegenPort.ml b/lib/codegenPort.ml index 5c0d945..24e1954 100644 --- a/lib/codegenPort.ml +++ b/lib/codegenPort.ml @@ -45,4 +45,76 @@ let format (typedefs : TypedefMap.t) (macro_defs: macro_def list) port = let inout = match port.dir with | Inp -> "input" | Out -> "output" - in Printf.sprintf "%s %s %s" inout (CodegenFormat.format_dtype typedefs macro_defs port.dtype) ep_name_formatted \ No newline at end of file + in Printf.sprintf "%s %s %s" inout (CodegenFormat.format_dtype typedefs macro_defs port.dtype) ep_name_formatted + + +let assertformat (typedefs : TypedefMap.t) (macro_defs: macro_def list) port = + let ep_name_formatted = CodegenFormat.sanitize_identifier port.name in + Printf.sprintf "%s %s" (CodegenFormat.format_dtype typedefs macro_defs port.dtype) ep_name_formatted + +let instanformat port = + let ep_name_formatted = CodegenFormat.sanitize_identifier port.name in + Printf.sprintf "%s" ep_name_formatted + +let valid_port_names_from_endpoint + (channel_classes : channel_class_def list) + (endpoint : endpoint_def) + : identifier list = + let cc = + Option.get (MessageCollection.lookup_channel_class channel_classes endpoint.channel_class) + in + cc.messages + |> List.filter (fun msg -> + let msg = ParamConcretise.concretise_message cc.params endpoint.channel_params msg in + message_has_valid_port msg + ) + |> List.map (fun msg -> + let msg = ParamConcretise.concretise_message cc.params endpoint.channel_params msg in + CodegenFormat.format_msg_valid_signal_name endpoint.name msg.name + ) + +let valid_port_names + (channel_classes : channel_class_def list) + (endpoints : endpoint_def list) + : identifier list = + List.concat_map (valid_port_names_from_endpoint channel_classes) endpoints + +let ack_port_names_from_endpoint + (channel_classes : channel_class_def list) + (endpoint : endpoint_def) + : identifier list = + let cc = + Option.get (MessageCollection.lookup_channel_class channel_classes endpoint.channel_class) + in + cc.messages + |> List.filter (fun msg -> + let msg = ParamConcretise.concretise_message cc.params endpoint.channel_params msg in + message_has_ack_port msg + ) + |> List.map (fun msg -> + let msg = ParamConcretise.concretise_message cc.params endpoint.channel_params msg in + CodegenFormat.format_msg_ack_signal_name endpoint.name msg.name + ) + +let ack_port_names + (channel_classes : channel_class_def list) + (endpoints : endpoint_def list) + : identifier list = + List.concat_map (ack_port_names_from_endpoint channel_classes) endpoints + +let data_port_names (channel_classes : channel_class_def list) + (endpoints : endpoint_def list) + : identifier list = + let data_names_from_endpoint (endpoint : endpoint_def) = + let cc = + Option.get (MessageCollection.lookup_channel_class channel_classes endpoint.channel_class) + in + List.concat_map (fun (msg : message_def) -> + let msg = ParamConcretise.concretise_message cc.params endpoint.channel_params msg in + List.mapi (fun i (_stype : sig_type_chan_local) -> + CodegenFormat.format_msg_data_signal_name endpoint.name msg.name i + ) msg.sig_types + ) cc.messages + in + List.concat_map data_names_from_endpoint endpoints + diff --git a/lib/codegenPort.mli b/lib/codegenPort.mli index 2f8baa4..7c2160b 100644 --- a/lib/codegenPort.mli +++ b/lib/codegenPort.mli @@ -26,3 +26,17 @@ val rst : t (** Format the definition of a port. This involves translating the type and direction into their equivalents in Verilog. *) val format : TypedefMap.t -> Lang.macro_def list -> t -> string + +val assertformat : TypedefMap.t -> Lang.macro_def list -> t -> string + +val instanformat : t -> string + +val valid_port_names_from_endpoint : Lang.channel_class_def list -> Lang.endpoint_def -> string list + +val valid_port_names : Lang.channel_class_def list -> Lang.endpoint_def list -> string list + +val ack_port_names_from_endpoint : Lang.channel_class_def list -> Lang.endpoint_def -> string list + +val ack_port_names : Lang.channel_class_def list -> Lang.endpoint_def list -> string list + +val data_port_names : Lang.channel_class_def list -> Lang.endpoint_def list -> string list diff --git a/lib/compileDriver.ml b/lib/compileDriver.ml index 8e79d66..9b83a23 100644 --- a/lib/compileDriver.ml +++ b/lib/compileDriver.ml @@ -172,3 +172,136 @@ let compile out config = {graphs with EventGraph.external_event_graphs = all_event_graphs}) all_collections end + +let verification_compile out config = + let open Config in + let toplevel_filename = List.hd config.input_filenames in + let cunits = ref [] in + ( + try parse_recursive cunits (ref Utils.StringSet.empty) config toplevel_filename + with + | Except.TypeError msg -> + (Except.Text "Type error:")::msg + |> raise_compile_error None + ); + (* collect all channel class and type definitions *) + let all_channel_classes = List.concat_map (fun (_, cunit) -> let open Lang in cunit.channel_classes) !cunits in + let all_type_defs = List.concat_map (fun (_, cunit) -> let open Lang in cunit.type_defs) !cunits in + let all_procs = List.concat_map (fun (file_name, cunit) -> let open Lang in List.map (fun p -> (file_name, p)) cunit.procs) !cunits in + let all_func_defs = List.concat_map (fun (_, cunit) -> let open Lang in cunit.func_defs) !cunits in + let all_macro_defs = List.concat_map (fun (_, cunit) -> let open Lang in cunit.macro_defs) !cunits in + let proc_map = List.map (fun (file_name, proc) -> (let open Lang in (proc:proc_def).name, (proc, file_name))) all_procs + |> Utils.StringMap.of_list in + let sched = BuildScheduler.create () in + (* add processes that are concrete *) + List.iter (fun (file_name, proc) -> + let open Lang in + if proc.params = [] then + let _ = BuildScheduler.add_proc_task sched file_name Lang.code_span_dummy proc.name [] in () + ) all_procs; + let modules_visited = ref Utils.StringSet.empty in + let event_graph_complete = ref false in + let graph_collection_queue = Queue.create () in + while not !event_graph_complete do + match BuildScheduler.next sched with + | None -> event_graph_complete := true + | Some task -> ( + if Utils.StringSet.mem task.module_name !modules_visited |> not then ( + modules_visited := Utils.StringSet.add task.module_name !modules_visited; + let proc_file_opt = Utils.StringMap.find_opt + (let open BuildScheduler in task.proc_name) + proc_map in + let open Except in + match proc_file_opt with + | None -> + let msg_text = Printf.sprintf "Process '%s' not found!" task.proc_name in + raise_compile_error None + [ + Text msg_text; + codespan_in task.file_name task.codespan + ] + | Some (proc, file_name) -> + let cunit = let open Lang in + (* hacky *) + {cunit_file_name = Some file_name; + channel_classes = all_channel_classes; type_defs = all_type_defs; + procs = [proc]; imports = []; _extern_procs = []; + func_defs = all_func_defs; + macro_defs = all_macro_defs} in + let graph_collection = + match GraphBuilder.build config sched task.module_name task.param_values cunit + with + | res -> res + | exception exc -> + ( + let msg = + match exc with + | EventGraph.LifetimeCheckError msg -> + (Text "Borrow checking failed:")::msg + | Except.TypeError msg -> + (Text "Type error:")::msg + | Except.UnimplementedError msg -> + (Text "Unimplemented error:")::msg + | EventGraph.EventGraphError msg -> + (Text "Event graph error:")::msg + | Except.UnknownError msg -> + (Text "Unknown error:")::msg + | _ -> raise exc + in + raise_compile_error (Some file_name) msg + ) + in + Queue.add graph_collection graph_collection_queue + ) + ) + done; + if config.just_check then + () + else begin + let visited_extern_files = ref Utils.StringSet.empty in + let open Lang in + List.iter (fun (file_name, cunit) -> + List.iter (fun {is_extern; file_name = imp_file_name} -> + if is_extern then + let imp_file_name_canonical = canonicalise_file_name file_name imp_file_name in + if Utils.StringSet.mem imp_file_name_canonical !visited_extern_files |> not then ( + visited_extern_files := Utils.StringSet.add imp_file_name_canonical !visited_extern_files; + (* Run verification *) + try Codegen.verification_generate_extern_import out imp_file_name_canonical + with Sys_error msg -> raise_compile_error (Some file_name) [Except.Text msg] + ) + ) cunit.imports + ) !cunits; + (* generate the code from event graphs *) + let all_collections = Queue.to_seq graph_collection_queue |> List.of_seq in + let all_event_graphs = List.concat_map (fun collection -> let open EventGraph in collection.event_graphs) all_collections in + List.iter (fun graphs -> + (* Run verification *) + Codegen.verification_generate out config + {graphs with EventGraph.external_event_graphs = all_event_graphs}) all_collections + end + + +let make_config (anvil_path : string) : Config.compile_config = + { + verbose = false; + disable_lt_checks = false; + weak_typecasts = true; + opt_level = 2; + output_filename = None; + just_check = false; + two_round_graph = false; + json_output = false; + input_filenames = [anvil_path]; + } + +let verification_run (argv : string array) : unit = + (* args *) + let anvil_file_path = argv.(2) in + let anvil_generated_sv_path = argv.(3) in + let user_sv_file = argv.(4) in + + AssertName.generate anvil_generated_sv_path user_sv_file; + + let config = make_config anvil_file_path in + verification_compile stdout config; diff --git a/lib/compileDriver.mli b/lib/compileDriver.mli index 60153db..63afdbe 100644 --- a/lib/compileDriver.mli +++ b/lib/compileDriver.mli @@ -4,3 +4,5 @@ exception CompileError of Except.error_message val compile : out_channel -> Config.compile_config -> unit + +val verification_run : string array -> unit diff --git a/properties/nosyn_user_receiver.svh b/properties/nosyn_user_receiver.svh new file mode 100644 index 0000000..fb11e49 --- /dev/null +++ b/properties/nosyn_user_receiver.svh @@ -0,0 +1,16 @@ + +property ack_low_when_valid_high (state_curr_0, valid_0, ack_0); + @(posedge clk_i) ((state_curr_0==WAIT_ACK) |-> valid_0 && !ack_0); +endproperty + +property ack_high_valid_low (state_curr_0, valid_0, ack_0); + @(posedge clk_i) (state_curr_0==DROP_VALID) |-> (!_ep_req_valid && $past(ack_0)); +endproperty + +property ack_low_after_handshake (state_prev_0, ack_0); + @(posedge clk_i) (state_prev_0==DROP_VALID) |-> !ack_0; +endproperty + +property data_stable_N_cycles_after_ack_high (state_curr_0, counter_0, data_0); + @(posedge clk_i) ((state_curr_0==DROP_VALID || counter_0!=0) |-> (data_0 == $past(data_0))); +endproperty diff --git a/properties/nosyn_user_sender.svh b/properties/nosyn_user_sender.svh new file mode 100644 index 0000000..37cd6f1 --- /dev/null +++ b/properties/nosyn_user_sender.svh @@ -0,0 +1,20 @@ + +property data_stable_valid_high (_endp_res_valid_0, state_curr_0, _endp_res_0_0); + @(posedge clk_i) ((_endp_res_valid_0 && !$rose(_endp_res_valid_0)) && (state_curr_0 inside {WAIT_REQ, WAIT_ACK})) |-> _endp_res_0_0 == $past(_endp_res_0_0); +endproperty + +property valid_high_until_ack_high (_endp_res_valid_0, state_curr_0); + @(posedge clk_i) ((_endp_res_valid_0 || $rose(_endp_res_valid_0)) && (state_curr_0 inside {WAIT_REQ, WAIT_ACK}) |-> _endp_res_valid_0); +endproperty + +property ack_high_valid_low(_endp_res_valid_0, state_curr_0, _endp_res_ack_0); + @(posedge clk_i) (state_curr_0==DROP_VALID) |-> (!_endp_res_valid_0 && $past(_endp_res_ack_0)); +endproperty + +property data_stable_N_cycles_after_ack_high (state_curr_0, counter_0, _endp_res_0_0); + @(posedge clk_i) ((state_curr_0==DROP_VALID || counter_0!=0) |-> (_endp_res_0 == $past(_endp_res_0_0))); +endproperty + +property wait_req_ack_low (state_curr_0, _endp_res_ack_0); + @(posedge clk_i) ((state_curr_0==WAIT_REQ) |-> !_endp_res_ack_0); +endproperty diff --git a/properties/syn_recv_dynamic_user_receiver.svh b/properties/syn_recv_dynamic_user_receiver.svh new file mode 100644 index 0000000..dc2785d --- /dev/null +++ b/properties/syn_recv_dynamic_user_receiver.svh @@ -0,0 +1,8 @@ + +property ack_low_during_DROP_ACK (state_curr_0, ack_0); + @(posedge clk_i) (state_curr_0==DROP_ACK) |-> !ack_0; +endproperty + +property data_stable_N_cycles (state_curr_0, counter_0, data_0); + @(posedge clk_i) ((state_curr_0==DROP_ACK || counter_0!=0) |-> (data_0 == $past(data_0))); +endproperty \ No newline at end of file diff --git a/properties/syn_recv_dynamic_user_sender.svh b/properties/syn_recv_dynamic_user_sender.svh new file mode 100644 index 0000000..400be3a --- /dev/null +++ b/properties/syn_recv_dynamic_user_sender.svh @@ -0,0 +1,3 @@ +property data_stable_N_cycles (state_curr_0, counter_0, data_0); + @(posedge clk_i) ((state_curr_0==DROP_ACK || counter_0!=0) |-> (data_0 == $past(data_0))); +endproperty \ No newline at end of file diff --git a/properties/syn_send_dynamic_user_receiver.svh b/properties/syn_send_dynamic_user_receiver.svh new file mode 100644 index 0000000..5812e66 --- /dev/null +++ b/properties/syn_send_dynamic_user_receiver.svh @@ -0,0 +1,3 @@ +property data_stable_N_cycles (state_curr_0, counter_0, data_0); + @(posedge clk_i) ((state_curr_0==DROP_VALID || counter_0!=0) |-> (data_0 == $past(data_0))); +endproperty \ No newline at end of file diff --git a/properties/syn_send_dynamic_user_sender.svh b/properties/syn_send_dynamic_user_sender.svh new file mode 100644 index 0000000..4958c1d --- /dev/null +++ b/properties/syn_send_dynamic_user_sender.svh @@ -0,0 +1,8 @@ + +property data_stable_N_cycles (state_curr_0, counter_0, data_0); + @(posedge clk_i) ((state_curr_0==DROP_VALID || counter_0!=0) |-> (data_0 == $past(data_0))); +endproperty + +property valid_low_during_DROP_VALID (state_curr_0, valid_0); + @(posedge clk_i) (state_curr_0==DROP_VALID) |-> !valid_0; +endproperty \ No newline at end of file