Add tests for formal verification; optimizations; fixes #3

* Minor optimization in sequencer unit
* Add Makefile & SymbiYosys command files for formal
  verification tests

README.md

@@ -16,7 +16,7 @@ The next two lists will grow during furter development
 * implication operator
 * next operator
 * next[i] operator
-* next_event operator
+* next_event() operator
 
 ## PSL features currently unsupported by GHDL:
 

formal/Makefile

@@ -0,0 +1,15 @@
+include tests.mk
+
+
+.PHONY: all clean
+
+all: ${psl_tests}
+
+
+%: ../src/%.vhd ../src/pkg.vhd ../src/sequencer.vhd ../src/hex_sequencer.vhd %.sby
+	mkdir -p work
+	-sby --yosys "yosys -m ghdl" -f -d work/$@ $@.sby prove
+
+
+clean:
+	rm -rf work

formal/psl_always.sby

@@ -0,0 +1,18 @@
+[tasks]
+prove
+
+[options]
+depth 25
+prove: mode bmc
+
+[engines]
+prove: smtbmc z3
+
+[script]
+prove: ghdl --std=08 pkg.vhd sequencer.vhd psl_always.vhd -e psl_always
+prep -top psl_always
+
+[files]
+../src/pkg.vhd
+../src/sequencer.vhd
+../src/psl_always.vhd

formal/psl_never.sby

@@ -0,0 +1,18 @@
+[tasks]
+prove
+
+[options]
+depth 25
+prove: mode bmc
+
+[engines]
+prove: smtbmc z3
+
+[script]
+prove: ghdl --std=08 pkg.vhd sequencer.vhd psl_never.vhd -e psl_never
+prep -top psl_never
+
+[files]
+../src/pkg.vhd
+../src/sequencer.vhd
+../src/psl_never.vhd

formal/psl_next.sby

@@ -0,0 +1,18 @@
+[tasks]
+prove
+
+[options]
+depth 25
+prove: mode bmc
+
+[engines]
+prove: smtbmc z3
+
+[script]
+prove: ghdl --std=08 pkg.vhd sequencer.vhd psl_next.vhd -e psl_next
+prep -top psl_next
+
+[files]
+../src/pkg.vhd
+../src/sequencer.vhd
+../src/psl_next.vhd

formal/psl_next_3.sby

@@ -0,0 +1,18 @@
+[tasks]
+prove
+
+[options]
+depth 25
+prove: mode bmc
+
+[engines]
+prove: smtbmc z3
+
+[script]
+prove: ghdl --std=08 pkg.vhd sequencer.vhd psl_next_3.vhd -e psl_next_3
+prep -top psl_next_3
+
+[files]
+../src/pkg.vhd
+../src/sequencer.vhd
+../src/psl_next_3.vhd

formal/psl_next_event.sby

@@ -0,0 +1,18 @@
+[tasks]
+prove
+
+[options]
+depth 25
+prove: mode bmc
+
+[engines]
+prove: smtbmc z3
+
+[script]
+prove: ghdl --std=08 pkg.vhd sequencer.vhd psl_next_event.vhd -e psl_next_event
+prep -top psl_next_event
+
+[files]
+../src/pkg.vhd
+../src/sequencer.vhd
+../src/psl_next_event.vhd

formal/tests.mk

@@ -0,0 +1,6 @@
+psl_tests := \
+psl_always \
+psl_never \
+psl_next \
+psl_next_3 \
+psl_next_event

src/psl_always.vhd

@@ -18,16 +18,17 @@ architecture psl of psl_always is
 begin
 
 
-  SEQ : sequencer generic map ("_-_-_") port map (clk, a);
+  --                            012345
+  SEQ : sequencer generic map ("--____") port map (clk, a);
 
 
   -- All is sensitive to rising edge of clk
   default clock is rising_edge(clk);
 
-  -- Signal a has to be low at cycle 0 only
+  -- This assertion holds
   WITHOUT_ALWAYS_a : assert a;
 
-  -- Signal a has to be low forever
+  -- This assertion doesn't hold at cycle 2
   WITH_ALWAYS_a : assert always a;
 
 

src/psl_never.vhd

@@ -13,22 +13,28 @@ end entity psl_never;
 
 architecture psl of psl_never is
 
-  signal a : std_logic;
+  signal a, b : std_logic;
 
 begin
 
 
-  SEQ : sequencer generic map ("_-_-_") port map (clk, a);
+  --                              0123
+  SEQ_A : sequencer generic map ("____") port map (clk, a);
+  SEQ_B : sequencer generic map ("__-_") port map (clk, b);
 
 
   -- All is sensitive to rising edge of clk
   default clock is rising_edge(clk);
 
-  -- Signal a has to be low forever
-  NEVER_a : assert never a;
+  -- This assertion holds
+  NEVER_0_a : assert never a;
 
   -- Equivalent assert with always and negation
+  -- This assertion holds
   ALWAYS_a : assert always not a;
 
+  -- This assertion doesn't hold at cycle 2
+  NEVER_1_a : assert never b;
+
 
 end architecture psl;

src/psl_next.vhd

@@ -19,9 +19,11 @@ architecture psl of psl_next is
 begin
 
 
+  --                              012345678901
   SEQ_A : sequencer generic map ("_-__--__-__") port map (clk, a);
   SEQ_B : sequencer generic map ("_--__--__--") port map (clk, b);
 
+  --                              012345678901
   SEQ_C : sequencer generic map ("_-__--__-__") port map (clk, c);
   SEQ_D : sequencer generic map ("_--__-___--") port map (clk, d);
 

src/psl_next_3.vhd

@@ -20,12 +20,15 @@ architecture psl of psl_next_3 is
 begin
 
 
+  --                              01234567890
   SEQ_A : sequencer generic map ("__-_-______") port map (clk, a);
   SEQ_B : sequencer generic map ("_____-_-___") port map (clk, b);
 
+  --                              01234567890
   SEQ_C : sequencer generic map ("__-_-______") port map (clk, c);
   SEQ_D : sequencer generic map ("_____-_____") port map (clk, d);
 
+  --                              01234567890
   SEQ_E : sequencer generic map ("__-_-______") port map (clk, e);
   SEQ_F : sequencer generic map ("_____-----_") port map (clk, f);
 
@@ -36,7 +39,7 @@ begin
   -- This assertion holds
   NEXT_0_a : assert always (a -> next[3] (b));
 
-  -- This assertion doesn't hold at cycle 8
+  -- This assertion doesn't hold at cycle 7
   NEXT_1_a : assert always (c -> next[3] (d));
 
   -- This assertion holds

src/sequencer.vhd

@@ -21,7 +21,7 @@ end entity sequencer;
 
 architecture rtl of sequencer is
 
-  signal cycle : natural := 0;
+  signal index : natural := seq'low;
   signal ch    : character;
 
 begin
@@ -30,13 +30,13 @@ begin
   process (clk) is
   begin
     if rising_edge(clk) then
-      if (cycle < seq'length) then
-        cycle <= cycle + 1;
+      if (index < seq'high) then
+        index <= index + 1;
       end if;
     end if;
   end process;
 
-  ch <= seq(cycle+1);
+  ch <= seq(index);
 
   data <= to_bit(ch);