diff --git a/assertion.sv b/assertion.sv new file mode 100644 index 0000000..7f2b49b --- /dev/null +++ b/assertion.sv @@ -0,0 +1,23 @@ +module axi_asserttions; + + +////// handshaking for awvalid & awready + +property pro; + +@(posedge clk) +disable iff(reset) + +(awvalid && !awready) |=> (awvalid && awready) ##1 (!awvalid && !awready); + + +endproperty + + +property pro_n; +disable iff(reset) + +!($isunknown({awaddr,awlen,awsize,awburst,awvalid})& awburst=2'b 10) |-> (awaddr%(2**awsize)==0) + + +endproperty