From 853ab1bbd536e19265e68d4808e9e5b53f247b1c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Orhan=20=C3=9Cn=C3=BCvar?= Date: Wed, 5 Jun 2024 23:03:09 +0200 Subject: [PATCH] init --- AtomicFormula.sv | 6 +++ DisjunctionFormula.sv | 7 +++ InversionFormula.sv | 6 +++ PastAlwaysFormula.sv | 13 +++++ PastEventuallyFormula.sv | 13 +++++ PreviouslyFormula.sv | 13 +++++ SinceFormula.sv | 14 +++++ TimedPastEventuallyFormula.sv | 32 ++++++++++++ command_file | 10 ++++ constants.svh | 2 + run.sh | 3 ++ tb.sv | 97 +++++++++++++++++++++++++++++++++++ 12 files changed, 216 insertions(+) create mode 100644 AtomicFormula.sv create mode 100644 DisjunctionFormula.sv create mode 100644 InversionFormula.sv create mode 100644 PastAlwaysFormula.sv create mode 100644 PastEventuallyFormula.sv create mode 100644 PreviouslyFormula.sv create mode 100644 SinceFormula.sv create mode 100644 TimedPastEventuallyFormula.sv create mode 100644 command_file create mode 100644 constants.svh create mode 100755 run.sh create mode 100644 tb.sv diff --git a/AtomicFormula.sv b/AtomicFormula.sv new file mode 100644 index 0000000..e87e2be --- /dev/null +++ b/AtomicFormula.sv @@ -0,0 +1,6 @@ +module AtomicFormula ( + input logic p, + output logic y +); + assign y = p; +endmodule diff --git a/DisjunctionFormula.sv b/DisjunctionFormula.sv new file mode 100644 index 0000000..e87fb2f --- /dev/null +++ b/DisjunctionFormula.sv @@ -0,0 +1,7 @@ +module DisjunctionFormula ( + input logic phi1, + input logic phi2, + output logic y +); + assign y = phi1 | phi2; +endmodule diff --git a/InversionFormula.sv b/InversionFormula.sv new file mode 100644 index 0000000..5fc6830 --- /dev/null +++ b/InversionFormula.sv @@ -0,0 +1,6 @@ +module InversionFormula ( + input logic phi, + output logic y +); + assign y = ~phi; +endmodule diff --git a/PastAlwaysFormula.sv b/PastAlwaysFormula.sv new file mode 100644 index 0000000..0157b93 --- /dev/null +++ b/PastAlwaysFormula.sv @@ -0,0 +1,13 @@ +module PastAlwaysFormula ( + input logic clk, + input logic phi, + output logic y +); + logic v; + + always_ff @(posedge clk) begin + v <= phi & v; + end + + assign y = v; +endmodule diff --git a/PastEventuallyFormula.sv b/PastEventuallyFormula.sv new file mode 100644 index 0000000..087248f --- /dev/null +++ b/PastEventuallyFormula.sv @@ -0,0 +1,13 @@ +module PastEventuallyFormula ( + input logic clk, + input logic phi, + output logic y +); + logic v; + + always_ff @(posedge clk) begin + v <= phi | v; + end + + assign y = v; +endmodule diff --git a/PreviouslyFormula.sv b/PreviouslyFormula.sv new file mode 100644 index 0000000..52fcd7b --- /dev/null +++ b/PreviouslyFormula.sv @@ -0,0 +1,13 @@ +module PreviouslyFormula ( + input logic clk, + input logic phi, + output logic y +); + logic v; + + always_ff @(posedge clk) begin + v <= phi; + end + + assign y = v; +endmodule diff --git a/SinceFormula.sv b/SinceFormula.sv new file mode 100644 index 0000000..a8f90ec --- /dev/null +++ b/SinceFormula.sv @@ -0,0 +1,14 @@ +module SinceFormula ( + input logic clk, + input logic phi1, + input logic phi2, + output logic y +); + logic v; + + always_ff @(posedge clk) begin + v <= phi2 | (phi1 & v); + end + + assign y = v; +endmodule diff --git a/TimedPastEventuallyFormula.sv b/TimedPastEventuallyFormula.sv new file mode 100644 index 0000000..7bd2eea --- /dev/null +++ b/TimedPastEventuallyFormula.sv @@ -0,0 +1,32 @@ +module TimedPastEventuallyFormula #( + parameter int unsigned a, + parameter int unsigned b, + localparam [0:`MAX_TIME-1] init_a2b = {{a{1'b0}}, {b-a+1{1'b1}}, {`MAX_TIME-b-1{1'b0}}} +) ( + input logic clk, + input logic rst, + input logic [0:`MAX_TIME-1] t, + input logic phi, + output logic y +); + logic [0:`MAX_TIME-1] v_r; + logic [0:`MAX_TIME-1] a2b_r; + + logic [0:`MAX_TIME-1] v_r_next; + logic [0:`MAX_TIME-1] a2b_r_next; + + assign v_r_next = (v_r & ~(t << 1)) | (phi ? a2b_r : `MAX_TIME'b0); + assign a2b_r_next = a2b_r >> 1; + + always_ff @(posedge clk or posedge rst) begin + if (rst) begin + v_r <= `MAX_TIME'b0; + a2b_r <= init_a2b; + end else begin + a2b_r <= a2b_r_next; + v_r <= v_r_next; + end + end + + assign y = |(v_r_next & t); +endmodule diff --git a/command_file b/command_file new file mode 100644 index 0000000..cb24b89 --- /dev/null +++ b/command_file @@ -0,0 +1,10 @@ +constants.svh +AtomicFormula.sv +InversionFormula.sv +DisjunctionFormula.sv +PreviouslyFormula.sv +SinceFormula.sv +PastEventuallyFormula.sv +PastAlwaysFormula.sv +TimedPastEventuallyFormula.sv +tb.sv diff --git a/constants.svh b/constants.svh new file mode 100644 index 0000000..93a25f7 --- /dev/null +++ b/constants.svh @@ -0,0 +1,2 @@ +`define MAX_TIME 16 +`define CLK_PERIOD 10 diff --git a/run.sh b/run.sh new file mode 100755 index 0000000..3baa8db --- /dev/null +++ b/run.sh @@ -0,0 +1,3 @@ +iverilog -g2012 -Wall -o tb.vvp -f command_file +vvp tb.vvp +rm tb.vvp diff --git a/tb.sv b/tb.sv new file mode 100644 index 0000000..e3251d9 --- /dev/null +++ b/tb.sv @@ -0,0 +1,97 @@ +module tb; + logic clk = 1; + initial forever #(`CLK_PERIOD/2) clk = ~clk; + bit rst = 0; + + logic p; + logic q; + logic y_top; + logic [0:`MAX_TIME-1] t; + + logic y_disj; + DisjunctionFormula disj ( + .phi1(p), + .phi2(q), + .y(y_disj) + ); + + logic y_tpe1; + TimedPastEventuallyFormula #( + .a(1), + .b(2) + ) tpe1 ( + .clk(clk), + .rst(rst), + .t(t), + .phi(y_disj), + .y(y_tpe1) + ); + + TimedPastEventuallyFormula #( + .a(1), + .b(2) + ) tpe2 ( + .clk(clk), + .rst(rst), + .t(t), + .phi(y_tpe1), + .y(y_top) + ); + + parameter int unsigned N_CYCLES = 6; + bit [0:N_CYCLES] [1:0] pq = { + {1'b0, 1'b0}, + {1'b1, 1'b0}, + {1'b0, 1'b0}, + {1'b0, 1'b0}, + {1'b0, 1'b0}, + {1'b0, 1'b1}, + {1'b0, 1'b0} + }; + + int signed first; + int signed last; + function string interval_repr(logic [0:`MAX_TIME-1] t); + first = -1; + last = -1; + for (int i = 0; i < `MAX_TIME; i++) begin + if (t[i]) begin + if (first == -1) first = i; + last = i; + end + end + if (first == -1) begin + return "ø"; + end else if (first == last) begin + return $sformatf("{%0d}", first); + end else begin + return $sformatf("[%0d, %0d]", first, last); + end + endfunction + + initial begin + #1; + rst = 1; + #1; + rst = 0; + t = {1'b1, {`MAX_TIME-1{1'b0}}}; + for (int i = 0; i <= N_CYCLES; i++) begin + #1; + if (i != 0) t >>= 1; + {p, q} = pq[i]; + #1; + $display("k: %0d", i); + $display("p: %0s", i == 0 ? "" : p ? "T" : "F"); + $display("q: %0s", i == 0 ? "" : q ? "T" : "F"); + $display("V_ϕ(1): %0s", y_disj ? "T" : "F"); + $display("V_ϕ(2): %0s", interval_repr(tpe1.v_r_next)); + $display("V_ϕ(3): %0s", interval_repr(tpe2.v_r_next)); + $display("Y_ϕ: %0s", i == 0 ? "" : y_top ? "T" : "F"); + $display("--------------------------------"); + #1; + @(posedge clk); + #1; + end + $finish(0); + end +endmodule