init

AtomicFormula.sv

@@ -0,0 +1,6 @@
+module AtomicFormula (
+    input logic p,
+    output logic y
+);
+    assign y = p;
+endmodule

DisjunctionFormula.sv

@@ -0,0 +1,7 @@
+module DisjunctionFormula (
+    input logic phi1,
+    input logic phi2,
+    output logic y
+);
+    assign y = phi1 | phi2;
+endmodule

InversionFormula.sv

@@ -0,0 +1,6 @@
+module InversionFormula (
+    input logic phi,
+    output logic y
+);
+    assign y = ~phi;
+endmodule

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

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

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

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

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

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

constants.svh

@@ -0,0 +1,2 @@
+`define MAX_TIME 16
+`define CLK_PERIOD 10

run.sh

@@ -0,0 +1,3 @@
+iverilog -g2012 -Wall -o tb.vvp -f command_file
+vvp tb.vvp
+rm tb.vvp

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