Merge pull request #91 from YosysHQ/eddie/verific_rand

Add verific/rand.sv test

verific/sva/Makefile

-TESTS := consrep firstmatch gotorep intersect nonconsrep seq_and seq_or triggered until until_trig within repzero
+TESTS := consrep firstmatch gotorep intersect nonconsrep seq_and seq_or triggered until until_trig within repzero rand
 
 all: $(addsuffix .status,$(TESTS))
 	grep -H . *.status | sed 's,.status:,\t,; s,PASS,pass,;' | expand -t20
@@ -9,6 +9,10 @@ all: $(addsuffix .status,$(TESTS))
 	-bash run.sh $(basename $@) > $(basename $@).log 2>&1
 	test -f $@
 
+rand.status: rand.sv
+	touch .start
+	@(yosys -ql $(<:%.sv=%.log) -p "verific -sv $<" 2>&1 && echo PASS > $(<:%.sv=%.status)) || echo FAIL > $(<:%.sv=%.status)
+
 clean:
 	rm -rf $(addsuffix .pass_??,$(TESTS))
 	rm -rf $(addsuffix .fail_??,$(TESTS))

verific/sva/rand.sv

+module djb2hash (input clock);
+        (* keep *) rand const reg [31:0] magic;
+        (* keep *) rand reg [7:0] inputval;
+        (* keep *) reg [31:0] state = 5381;
+        (* keep *) integer cnt = 0;
+        always @(posedge clock) begin
+                state <= ((state << 5) + state) ^ inputval;
+                if (state == magic) cnt <= cnt + 1;
+                assert (cnt < 2);
+        end
+endmodule