Add examples for formal attributes anyconst & anyseq

README.md

@@ -74,6 +74,12 @@ The next lists will grow during further development
 * Partial support of PSL `endpoint` (simulation only, in PSL comments)
 
 
+### Yosys formal extensions (reference to [Symbiyosys docs](https://symbiyosys.readthedocs.io/en/latest/verilog.html#unconstrained-variables))
+
+* `anyconst` attribute (synthesis only)
+* `anyseq` attribute (synthesis only)
+
+
 ## Not yet supported by GHDL:
 
 * `forall` operator

formal/tests.mk

@@ -31,4 +31,6 @@ psl_stable \
 psl_rose \
 psl_fell \
 psl_logical_iff \
-psl_vunit
+psl_vunit \
+yosys_anyconst \
+yosys_anyseq

formal/yosys_anyconst.sby

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

formal/yosys_anyseq.sby

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

src/yosys_anyconst.vhd

@@ -0,0 +1,43 @@
+library ieee;
+  use ieee.std_logic_1164.all;
+
+use work.pkg.all;
+
+
+entity yosys_anyconst is
+  port (
+    clk : in std_logic
+  );
+end entity yosys_anyconst;
+
+
+architecture psl of yosys_anyconst is
+
+  attribute anyconst : boolean;
+
+  signal a: std_logic;
+  signal b: natural;
+
+  attribute anyconst of a : signal is true;
+  attribute anyconst of b : signal is true;
+
+begin
+
+
+  -- All is sensitive to rising edge of clk
+  default clock is rising_edge(clk);
+
+  -- a should always be high 
+  ANY_ASSUME_0_a : assume always a;
+
+  -- This assertion holds
+  ANY_ASSERT_0_a : assert always a;
+
+  -- a should always be high 
+  ANY_ASSUME_1_a : assume always b = 42;
+
+  -- This assertion holds
+  ANY_ASSERT_1_a : assert always b = 42;
+
+
+end architecture psl;

src/yosys_anyseq.vhd

@@ -0,0 +1,47 @@
+library ieee;
+  use ieee.std_logic_1164.all;
+
+use work.pkg.all;
+
+
+entity yosys_anyseq is
+  port (
+    clk : in std_logic
+  );
+end entity yosys_anyseq;
+
+
+architecture psl of yosys_anyseq is
+
+  attribute anyseq : boolean;
+
+  signal a: std_logic;
+  signal b: natural;
+
+  attribute anyseq of a : signal is true;
+  attribute anyseq of b : signal is true;
+
+begin
+
+
+  -- All is sensitive to rising edge of clk
+  default clock is rising_edge(clk);
+
+  -- a should always be high 
+  ANY_ASSUME_0_a : assume always a;
+
+  -- This assertion holds
+  ANY_ASSERT_0_a : assert always a;
+
+  -- b should always be in range 23...42 
+  ANY_ASSUME_1_a : assume always b >= 23 and b <= 42;
+
+  -- This assertion holds
+  ANY_ASSERT_1_a : assert always b >= 23 and b <= 42;
+
+  -- This assertion fails in cycle 1
+  -- Solver chosen value can change from one to next cycle
+  ANY_ASSERT_2_a : assert b >= 23 -> next b = prev(b);
+
+
+end architecture psl;