Assert statement in Verilog

问题:

I'm completely new to Verilog, so bear with me.

I'm wondering if there is an assert statement in Verilog. In my testbench, I want to be able to assert that the outputs of modules are equal to certain values.

For example,

mymodule m(in, out);
assert(out == 1'b1);

Googling gave me a few links, but they were either too complex or didn't seem to be what I wanted.

回答1:

There is an open source library for assertions called OVL. However, it's pretty heavy. One trick I nicked from there is creating a module to do assertions.

module assert(input clk, input test);
    always @(posedge clk)
    begin
        if (test !== 1)
        begin
            $display("ASSERTION FAILED in %m");
            $finish;
        end
    end
endmodule

Now, any time you want to check a signal, all you have to do is instantiate an assertion in your module, like this:

module my_cool_module(input clk, ...);

     ...

     assert a0(.clk(clk), .test(some_signal && some_other_signal));

     ...

endmodule

When the assertion fails, you'll get a message like this:

ASSERTION FAILED in my_cool_module.a0

The %m in the display statement will show the entire hierarchy to the offending assertion, which is handy when you have a lot of these in a larger project.

You may wonder why I check on the edge of the clock. This is subtle, but important. If some_signal and some_other_signal in the expression above were assigned in different always blocks, it's possible the expression could be false for a brief period of time depending on the order that your Verilog simulator schedules the blocks (even though the logic was entirely valid). This would give you a false negative.

The other thing to note above is that I use !==, which will cause the assertion to fail if the test value is X or Z. If it used the normal !=, it could silently give a false positive in some cases.

回答2:

you can write like this

if(!(out==1'b1)) $finish;

回答3:

If your simulator supports SystemVerilog syntax, there is an assert keyword which does what you want.

回答4:

Putting the above together with a macro works for me:

`define assert(signal, value) \
        if (signal !== value) begin \
            $display("ASSERTION FAILED in %m: signal != value"); \
            $finish; \
        end

Then later in my test module:

initial begin // assertions
    #32 `assert(q, 16'hF0CB)
end

As an example test fail case:

ASSERTION FAILED in test_shift_register: q != 16'hF0CB

回答5:

Verilog doesn't support assertions. Some tools support PSL, which places the assertions in comments but this is non-standard. You should consider using hierarchical references from a testbench instead otherwise you have to place each assertion in a process which will get messy.

The easiest way to mimic C-like assertions is probably a `define since this will make them global.

`define assert(condition) if(condition) begin $finish(1); end

In order to check signals in a non-procedural context, such as your example, you will need a different macro that builds a condition signal and then triggers a test event for that signal.

`define assert_always(condition) generate if(1) begin wire test = condition; always @(test) `assert(condition) end endgenerate

The generate above will create a new scope for the variable test so multiple instances should work.

A better way in a procedural might be to create a task in a separate file and then include that in any module declaration.

task assert(input condition);
if(!condition)
  $finish(2);
endtask

For non-procedural contexts you'll need to create a module containing a process and instance that module. This will require a unique name for each instance unless you put it in a generate block.