Formal verification

counter/.gitignore

@@ -0,0 +1 @@
+counter/

counter/counter.sby

@@ -0,0 +1,16 @@
+[options]
+mode prove
+depth 15
+
+[engines]
+smtbmc
+# abc pdr
+# aiger avy
+# aiger suprove
+
+[script]
+read -formal counter.v
+prep -top counter
+
+[files]
+counter.v

counter/counter.v

@@ -1,3 +1,7 @@
+`ifdef FORMAL
+`default_nettype none
+`endif
+
 module counter
 (
     input clk,
@@ -17,4 +21,50 @@ always @(posedge clk) begin
 end
 
 assign led = ~ledCounter;
+
+//
+// FORMAL VERIFICATION
+//
+`ifdef FORMAL
+
+    // f_past_valid
+	reg	f_past_valid;
+	initial	f_past_valid = 1'b0;
+	always @(posedge clk)
+		f_past_valid <= 1'b1;
+
+    //
+    // clockCounter
+    //
+
+    // Prove that counter can't be higher than WAIT_TIME
+    always @(*)
+        assert(clockCounter <= WAIT_TIME);
+
+    // Prove that counter counts up
+    always @(posedge clk)
+    if((f_past_valid)&&($past(f_past_valid))) begin
+        if(clockCounter == 0)
+            assert($past(clockCounter)==WAIT_TIME);
+        else
+            assert(clockCounter == ($past(clockCounter)+1));
+    end
+
+    //
+    // ledCounter
+    //
+
+    // Prove that counter counts up
+    always @(posedge clk)
+    if((f_past_valid)&&($past(f_past_valid))) begin
+        if(clockCounter == 0) begin
+            if(ledCounter == 0)
+                assert($past(ledCounter) == 6'b11_1111);
+            else
+                assert(ledCounter == ($past(ledCounter)+1));
+        end
+    end
+
+`endif // FORMAL
+
 endmodule

counter/run_formal_verification.sh

@@ -0,0 +1,4 @@
+#!/bin/bash
+
+# Run SymbiYosis
+sby -f counter.sby

screen/.gitignore

@@ -0,0 +1,4 @@
+*.gprj.user
+*.user
+impl/
+screen/

screen/screen.gprj

@@ -0,0 +1,11 @@
+<?xml version="1" encoding="UTF-8"?>
+<!DOCTYPE gowin-fpga-project>
+<Project>
+    <Template>FPGA</Template>
+    <Version>5</Version>
+    <Device name="GW1NR-9C" pn="GW1NR-LV9QN88PC6/I5">gw1nr9c-004</Device>
+    <FileList>
+        <File path="screen.v" type="file.verilog" enable="1"/>
+        <File path="tangNano9k.cst" type="file.cst" enable="1"/>
+    </FileList>
+</Project>

screen/screen.sby

@@ -0,0 +1,17 @@
+[options]
+mode prove
+depth 25
+
+[engines]
+smtbmc
+# abc pdr
+# aiger avy
+# aiger suprove
+
+[script]
+read_verilog -DSCREEN -formal screen.v
+prep -top screen
+
+[files]
+screen.v
+image.hex