PSL usage in Formal Verification, assertion problem

Question

I am investigating the usability of formal verification in FPGA designs using VHDL, PSL, SymbiYosys, and GHDL. I've watched several webinars, read a PSL book, and gone through tutorials. Currently, I am attempting to create test assertions, but I'm facing numerous challenges, especially with what I believe are basic constructs.

I've created sample design:

I would like to test following cases:

1. Sequence: req_i (when reset is not asserted) -> data_en_o* -> eot_o** -> ack_i
   * (1)data_en_o should be raised exactly 2 clks later
   (2)data_en_o should be raised at some undefined point in the future, but it must occur
   ** (1)eot_o should be raised next clk after data_en_o is deasserted
   (2)eot_o should be raised precisely on the last clock cycle when data_en_o is asserted.

During my tests I was trying this approach:

f_seq : assert always (rst_n_i -> req_i -> next[2](data_en_o) -> eventually! eot_o);

Symbiyosys complained about:

• "next[2](data_en_o) -> eventually! eot_o : left-hand side operand of logical '->' must be a boolean". I don't understand why it is not correct as next2out_data_en_o is also check for specific condition (output should be boolean)
  
• when I removed " -> next[2](data_en_o) " the assertion is passing even without eot_o asserted. Eventually! is 'strong' so assertion of eot_o should occur before end of the test.

Additionally, I am also interested in how to formulate these assertions using SERE.

Answer 1

assert directives are used for checking outputs or internal states of the DUT, modeling input behavior is done using assume directives.

This: always (rst_n_i -> req_i -> ... means that if your design is out of reset, req_i has to be '1' every cycle. That's not the case. What you probably want to write is something like:

assume always (not rst_n_i -> not req_i);
assume always req_i -> next not not req_i);

That would model the behavior of req_i input. It has to be '0' during reset, can be set 1 at any other cycle, and has to be '1' for one cycle only.

Another hint is to better split your properties in simple ones. They're better readable for the user and mostly easier to proof for the tool. Here are some examples to check the output behavior you probably want.

Beware that these checks aren't complete. They only check exactly the behavior they specify, nothing more.

(1)data_en_o should be raised exactly 2 clks later

assert always (rst_n_i and req_i -> next[2](data_en_o));

(2)data_en_o should be raised at some undefined point in the future, but it must occur

That's not that easy, at least with GHDL and SymbiYosys. SymbiYosys supports liveness proofs, but not really with GHDL and the eventually! PSL operator (see ghdl/ghdl#1345 and ghdl/ghdl-yosys-plugin#152). Other thing is, that unbounded liveness proofs can be very hard to prove.

What you could do is to restrict the length of your proof by choosing an upper cycle count. For example:

data_en_o should be raised at some undefined point in the future, but it must occur at least 50 cycles after req_i

Of course, your DUT has to fulfill this. If it does, you can use following assertion for example:

assert always (rst_n_i and req_i -> next_e[2 to 50](data_en_o));

(1)eot_o should be raised next clk after data_en_o is deasserted

assert always (fell(data_en_o) -> eot_o);
assert always ({data_en_o; not data_en_o} |-> eot_o);  -- Using a SERE

(2)eot_o should be raised precisely on the last clock cycle when data_en_o is asserted

assert always (fell(data_en_o) -> prev(eot_o));
assert always ({data_en_o; not data_en_o} |-> prev(eot_o));  -- Using a SERE

Additional checks

You probably want to check some other things too, like

data_o is stable during data_en_o is '1':

assert always (data_en_o -> next(stable(data_o) until not data_en_o));

eot_o is '1' for one cycle only:

assert always (eot_o -> next(not eot_o));

The behavior of ack_i can be modeled by assume directives:

assume always (eot_o -> next(ack_i));
assume always (ack_i -> next(not ack_i));

As mentioned earlier, these examples don't say anything about behavior of the DUT outputs in other design states. For example, eot_i could be high at many other cycles, there is no assert that proves the reverse.

Answer 2

I struggled the similar paradigm problem few years ago, when starting to study PSL for symbiyosys.

What really helped me, was to understand what part GHDL has to do in the process.

PSL (the subset what GHDL supports) is really another synthesizable language, which in the end generates a netlist with registers and logic. Main difference being that it doesn't produce any outputs, but is driving special cells, like $assert and $assume, which then are processed by yosys to convert to SMT/SAT format (description of logical problem to SMT/SAT solver).

Whenever you write assert always ... , the synthesizer generates a schematic wich outputs zero to $assert cell if the property in assert is false. The formal tool is only searching a way to make the input of $assert cell to be zero.

Similar way as VHDL is not interpreted or "executed" during synthesis (except for elaboration purposes), PSL is not executed - never. It is only synthesized to a netlist, which is then used to test the property.