3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-08-07 03:31:24 +00:00

Add some simple SVA test cases for future Verific work

This commit is contained in:
Clifford Wolf 2017-07-22 12:31:08 +02:00
parent 2785aaffeb
commit 024ba310ec
4 changed files with 45 additions and 0 deletions

10
tests/sva/basic03.sv Normal file
View file

@ -0,0 +1,10 @@
module top (input logic clk, input logic selA, selB, QA, QB, output logic Q);
always @(posedge clk) begin
if (selA) Q <= QA;
if (selB) Q <= QB;
end
check_selA: assert property ( @(posedge clk) selA|=> Q == $past(QA) );
check_selB: assert property ( @(posedge clk) selB|=> Q == $past(QB) );
assume_not_11: assume property ( @(posedge clk) !(selA& selB) );
endmodule