Add scripts/rtl for formal verification

coverage/GPIOCoverageReport.txt

@@ -0,0 +1,36 @@
+Coverage Report Summary Data by file
+
+=================================================================================
+=== File: rtl/AHB_GPIO/AHBGPIO.sv
+=================================================================================
+    Enabled Coverage            Active      Hits    Misses % Covered
+    ----------------            ------      ----    ------ ---------
+    Stmts                           19        19         0    100.00
+    Branches                        12        11         1     91.66
+    FEC Condition Terms             11         8         3     72.72
+    Toggle Bins                    486       381       105     78.39
+
+=================================================================================
+=== File: rtl/AHB_GPIO/ahb_gpio_checker.sv
+=================================================================================
+    Enabled Coverage            Active      Hits    Misses % Covered
+    ----------------            ------      ----    ------ ---------
+    Stmts                            4         3         1     75.00
+    Branches                         4         3         1     75.00
+    Toggle Bins                    282       241        41     85.46
+
+=================================================================================
+=== File: tbench/ahb_gpio_tb.sv
+=================================================================================
+    Enabled Coverage            Active      Hits    Misses % Covered
+    ----------------            ------      ----    ------ ---------
+    Stmts                           33        33         0    100.00
+    Toggle Bins                    342       260        82     76.02
+
+
+TOTAL COVERGROUP COVERAGE: 95.36%  COVERGROUP TYPES: 5
+
+TOTAL ASSERTION COVERAGE: 50.00%  ASSERTIONS: 4
+
+Total Coverage By File (code coverage only, filtered view): 84.47%
+

coverage/VGACoverageReport.txt

@@ -0,0 +1,106 @@
+Coverage Report Summary Data by file
+
+=================================================================================
+=== File: rtl/AHB_VGA/AHBVGASYS.sv
+=================================================================================
+    Enabled Coverage            Active      Hits    Misses % Covered
+    ----------------            ------      ----    ------ ---------
+    Stmts                           25        23         2     92.00
+    Branches                        11        10         1     90.90
+    FEC Condition Terms             11         2         9     18.18
+    FEC Expression Terms             2         0         2      0.00
+    Toggle Bins                    430       102       328     23.72
+
+=================================================================================
+=== File: rtl/AHB_VGA/ahb_vgasys_checker.sv
+=================================================================================
+    Enabled Coverage            Active      Hits    Misses % Covered
+    ----------------            ------      ----    ------ ---------
+    Stmts                           30        30         0    100.00
+    Branches                        25        25         0    100.00
+    FEC Condition Terms             11        11         0    100.00
+    Toggle Bins                    724       282       442     38.95
+
+=================================================================================
+=== File: rtl/AHB_VGA/counter.sv
+=================================================================================
+    Enabled Coverage            Active      Hits    Misses % Covered
+    ----------------            ------      ----    ------ ---------
+    Stmts                            8         8         0    100.00
+    Branches                        10        10         0    100.00
+    FEC Condition Terms              3         3         0    100.00
+    Toggle Bins                     50        49         1     98.00
+
+=================================================================================
+=== File: rtl/AHB_VGA/dual_port_ram_sync.sv
+=================================================================================
+    Enabled Coverage            Active      Hits    Misses % Covered
+    ----------------            ------      ----    ------ ---------
+    Stmts                            6         6         0    100.00
+    Branches                         2         2         0    100.00
+    Toggle Bins                    172       124        48     72.09
+
+=================================================================================
+=== File: rtl/AHB_VGA/font_rom.sv
+=================================================================================
+    Enabled Coverage            Active      Hits    Misses % Covered
+    ----------------            ------      ----    ------ ---------
+    Stmts                         2051       483      1568     23.54
+    Branches                      2049       481      1568     23.47
+    Toggle Bins                     62        62         0    100.00
+
+=================================================================================
+=== File: rtl/AHB_VGA/vga_console.sv
+=================================================================================
+    Enabled Coverage            Active      Hits    Misses % Covered
+    ----------------            ------      ----    ------ ---------
+    Stmts                           48        39         9     81.25
+    Branches                        33        21        12     63.63
+    FEC Condition Terms              9         1         8     11.11
+    FEC Expression Terms             9         3         6     33.33
+    Toggle Bins                    446       308       138     69.05
+
+=================================================================================
+=== File: rtl/AHB_VGA/vga_image.sv
+=================================================================================
+    Enabled Coverage            Active      Hits    Misses % Covered
+    ----------------            ------      ----    ------ ---------
+    Stmts                            5         5         0    100.00
+    Toggle Bins                    276       107       169     38.76
+
+=================================================================================
+=== File: rtl/AHB_VGA/vga_sync.sv
+=================================================================================
+    Enabled Coverage            Active      Hits    Misses % Covered
+    ----------------            ------      ----    ------ ---------
+    Stmts                           14        14         0    100.00
+    Branches                        10        10         0    100.00
+    FEC Condition Terms             10        10         0    100.00
+    Toggle Bins                    126       102        24     80.95
+
+=================================================================================
+=== File: tbench/ahb_vga_font_map.sv
+=================================================================================
+    Enabled Coverage            Active      Hits    Misses % Covered
+    ----------------            ------      ----    ------ ---------
+    Stmts                         2048       496      1552     24.21
+    Branches                      2049       496      1553     24.20
+
+=================================================================================
+=== File: tbench/ahb_vga_tb.sv
+=================================================================================
+    Enabled Coverage            Active      Hits    Misses % Covered
+    ----------------            ------      ----    ------ ---------
+    Stmts                           48        48         0    100.00
+    Branches                         7         7         0    100.00
+    FEC Condition Terms              3         3         0    100.00
+    FEC Expression Terms             2         2         0    100.00
+    Toggle Bins                    378        54       324     14.28
+
+
+TOTAL COVERGROUP COVERAGE: 100.00%  COVERGROUP TYPES: 1
+
+TOTAL ASSERTION COVERAGE: 100.00%  ASSERTIONS: 6
+
+Total Coverage By File (code coverage only, filtered view): 39.83%
+

gpio.tcl

@@ -0,0 +1,11 @@
+clear -all
+analyze -clear
+analyze -sv rtl/AHB_GPIO/AHBGPIO_SVA.sv
+elaborate -bbox_mul 64 -top AHBGPIO_SVA
+
+clock HCLK
+reset -expression !(HRESETn)
+
+task -set <embedded>
+set_proofgrid_max_jobs 4
+set_proofgrid_max_local_jobs 4

rtl/AHB_GPIO/AHBGPIO.sv

@@ -92,7 +92,7 @@ module AHBGPIO
       {gpio_parityout, gpio_dataout} <= 17'd0;
     else if ((gpio_dir == 16'h0001) & (last_HADDR[7:0] == gpio_data_addr) & last_HSEL & last_HWRITE & last_HTRANS[1]) begin
       gpio_dataout <= HWDATA[15:0];
-      gpio_parityout <= ~^{HWDATA[15:0],PARITYSEL,INJECT_FAULT};
+      gpio_parityout <= ~^{HWDATA[15:0],~PARITYSEL,INJECT_FAULT};
     end
 
   // Update input value
@@ -103,7 +103,7 @@ module AHBGPIO
     end
     else if (gpio_dir == 16'h0000) begin
       gpio_datain <= GPIOIN[15:0];
-      gpio_parityerr <= ~^{GPIOIN,PARITYSEL,INJECT_FAULT};
+      gpio_parityerr <= ~^{GPIOIN,~PARITYSEL,INJECT_FAULT};
     end
     else if (gpio_dir == 16'h0001)
       gpio_datain <= GPIOOUT;

rtl/AHB_GPIO/AHBGPIO_SVA.sv

@@ -0,0 +1,164 @@
+//////////////////////////////////////////////////////////////////////////////////
+//END USER LICENCE AGREEMENT                                                    //
+//                                                                              //
+//Copyright (c) 2012, ARM All rights reserved.                                  //
+//                                                                              //
+//THIS END USER LICENCE AGREEMENT (<28>LICENCE<43>) IS A LEGAL AGREEMENT BETWEEN      //
+//YOU AND ARM LIMITED ("ARM") FOR THE USE OF THE SOFTWARE EXAMPLE ACCOMPANYING  //
+//THIS LICENCE. ARM IS ONLY WILLING TO LICENSE THE SOFTWARE EXAMPLE TO YOU ON   //
+//CONDITION THAT YOU ACCEPT ALL OF THE TERMS IN THIS LICENCE. BY INSTALLING OR  //
+//OTHERWISE USING OR COPYING THE SOFTWARE EXAMPLE YOU INDICATE THAT YOU AGREE   //
+//TO BE BOUND BY ALL OF THE TERMS OF THIS LICENCE. IF YOU DO NOT AGREE TO THE   //
+//TERMS OF THIS LICENCE, ARM IS UNWILLING TO LICENSE THE SOFTWARE EXAMPLE TO    //
+//YOU AND YOU MAY NOT INSTALL, USE OR COPY THE SOFTWARE EXAMPLE.                //
+//                                                                              //
+//ARM hereby grants to you, subject to the terms and conditions of this Licence,//
+//a non-exclusive, worldwide, non-transferable, copyright licence only to       //
+//redistribute and use in source and binary forms, with or without modification,//
+//for academic purposes provided the following conditions are met:              //
+//a) Redistributions of source code must retain the above copyright notice, this//
+//list of conditions and the following disclaimer.                              //
+//b) Redistributions in binary form must reproduce the above copyright notice,  //
+//this list of conditions and the following disclaimer in the documentation     //
+//and/or other materials provided with the distribution.                        //
+//                                                                              //
+//THIS SOFTWARE EXAMPLE IS PROVIDED BY THE COPYRIGHT HOLDER "AS IS" AND ARM     //
+//EXPRESSLY DISCLAIMS ANY AND ALL WARRANTIES, EXPRESS OR IMPLIED, INCLUDING     //
+//WITHOUT LIMITATION WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR //
+//PURPOSE, WITH RESPECT TO THIS SOFTWARE EXAMPLE. IN NO EVENT SHALL ARM BE LIABLE/
+//FOR ANY DIRECT, INDIRECT, INCIDENTAL, PUNITIVE, OR CONSEQUENTIAL DAMAGES OF ANY/
+//KIND WHATSOEVER WITH RESPECT TO THE SOFTWARE EXAMPLE. ARM SHALL NOT BE LIABLE //
+//FOR ANY CLAIMS, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, //
+//TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE    //
+//EXAMPLE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE EXAMPLE. FOR THE AVOIDANCE/
+// OF DOUBT, NO PATENT LICENSES ARE BEING LICENSED UNDER THIS LICENSE AGREEMENT.//
+//////////////////////////////////////////////////////////////////////////////////
+
+
+module AHBGPIO_SVA
+( input  wire        HCLK
+, input  wire        HRESETn
+, input  wire [31:0] HADDR
+, input  wire [ 1:0] HTRANS
+, input  wire [31:0] HWDATA
+, input  wire        HWRITE
+, input  wire        HSEL
+, input  wire        HREADY
+, input  wire [16:0] GPIOIN
+, input  wire        PARITYSEL
+, input  wire        INJECT_FAULT
+	//Output
+, output wire        HREADYOUT
+, output wire [31:0] HRDATA
+, output wire [16:0] GPIOOUT
+, output wire        PARITYERR
+);
+
+  localparam [7:0] gpio_data_addr = 8'h00;
+  localparam [7:0] gpio_dir_addr = 8'h04;
+
+  reg [15:0] gpio_dataout;
+  reg        gpio_parityout;
+  reg [15:0] gpio_datain;
+  reg        gpio_parityerr;
+  reg [15:0] gpio_dir;
+  reg [15:0] gpio_data_next;
+  reg [31:0] last_HADDR;
+  reg [ 1:0] last_HTRANS;
+  reg        last_HWRITE;
+  reg        last_HSEL;
+
+  assign HREADYOUT = 1'b1;
+
+// Set Registers from address phase
+  always_ff @(posedge HCLK)
+    if(HREADY) begin
+      last_HADDR <= HADDR;
+      last_HTRANS <= HTRANS;
+      last_HWRITE <= HWRITE;
+      last_HSEL <= HSEL;
+    end
+
+  // Update in/out switch
+  always_ff @(posedge HCLK, negedge HRESETn)
+    if(!HRESETn)
+      gpio_dir <= 16'h0000;
+    else if ((last_HADDR[7:0] == gpio_dir_addr) & last_HSEL & last_HWRITE & last_HTRANS[1])
+      gpio_dir <= HWDATA[15:0];
+
+  // Update output value
+  always_ff @(posedge HCLK, negedge HRESETn)
+    if(!HRESETn)
+      {gpio_parityout, gpio_dataout} <= 17'd0;
+    else if ((gpio_dir == 16'h0001) & (last_HADDR[7:0] == gpio_data_addr) & last_HSEL & last_HWRITE & last_HTRANS[1]) begin
+      gpio_dataout <= HWDATA[15:0];
+      gpio_parityout <= ^{HWDATA[15:0],PARITYSEL,INJECT_FAULT};
+    end
+
+  // Update input value
+  always_ff @(posedge HCLK, negedge HRESETn)
+    if(!HRESETn) begin
+      gpio_datain <= 16'h0000;
+      gpio_parityerr <= '0;
+    end
+    else if (gpio_dir == 16'h0000) begin
+      gpio_datain <= GPIOIN[15:0];
+      gpio_parityerr <= ^{GPIOIN,PARITYSEL,INJECT_FAULT};
+    end
+    else if (gpio_dir == 16'h0001)
+      gpio_datain <= GPIOOUT;
+
+  assign HRDATA[15:0] = gpio_datain;
+  assign GPIOOUT = {gpio_parityout, gpio_dataout};
+  assign PARITYERR = gpio_parityerr;
+
+  //check behaviour
+
+  // assert_parity: assert property
+  // ( @(posedge HCLK) disable iff (!HRESETn)
+  //   !PARITYERR
+  // );
+
+  assert_gpio_write: assert property
+  ( @(posedge HCLK) disable iff (!HRESETn)
+    ((HADDR[7:0] == gpio_data_addr)
+      && HSEL
+      && HWRITE
+      && HTRANS[1]
+      && HREADY) |-> ##1
+      (gpio_dir == 16'h0001) |-> ##1
+    (GPIOOUT[15:0] == $past(HWDATA[15:0], 1) && (!$past(INJECT_FAULT,1) -> (^GPIOOUT == $past(PARITYSEL, 1))))
+  );
+  assert_gpio_read: assert property
+  ( @(posedge HCLK) disable iff (!HRESETn)
+    ((gpio_dir == 16'h0000)
+      && (HADDR[7:0] == gpio_data_addr)
+      // && HSEL // HSEL not used in Read always_ff
+      && !HWRITE
+      && HTRANS[1]
+      && HREADY) |-> ##1
+     ((HRDATA[15:0]==$past(GPIOIN[15:0],1)) && HREADYOUT && (!$past(INJECT_FAULT,1) -> !PARITYERR))
+  );
+
+  assert_gpio_dir: assert property
+  ( @(posedge HCLK) disable iff (!HRESETn)
+    ((HADDR[7:0] == gpio_dir_addr)
+      && HSEL
+      && HWRITE
+      && HTRANS[1]
+      && HREADY) |-> ##1
+    ((HWDATA[7:0] == 8'h00 || HWDATA[7:0] == 8'h01)) |-> ##1 (gpio_dir == $past(HWDATA[15:0], 1))
+  );
+
+  assume_initial_valid: assume property
+  ( @(posedge HCLK)
+    gpio_dir == 16'h0000
+    || gpio_dir == 16'h0001
+  );
+
+  assume_gpio_in_valid_parity: assume property
+  ( @(posedge HCLK)
+      (^GPIOIN == PARITYSEL)
+  );
+
+endmodule

rtl/AHB_GPIO/ahb_gpio_checker.sv

@@ -12,6 +12,7 @@ module ahb_gpio_checker
 , input wire [31:0] HRDATA
 , input wire [16:0] GPIOOUT
 , input wire        PARITYERR
+, input wire        PARITYSEL
 );
 
   logic             gpio_cmd =  HSEL && HREADY && HTRANS[1];
@@ -27,7 +28,7 @@ module ahb_gpio_checker
     ##1
     (gpio_dir=='1) |->
     ##1
-    (GPIOOUT[15:0] == $past(HWDATA[15:0],1));
+    (GPIOOUT[15:0] == $past(HWDATA[15:0],1)) && (^GPIOOUT == $past(PARITYSEL, 1));
   endproperty
 
   property gpio_read;
@@ -35,7 +36,7 @@ module ahb_gpio_checker
     (HADDR[7:0] == gpio_data_addr) && gpio_cmd
     && (gpio_dir=='0) |->
     ##1
-    ((HRDATA[15:0]==$past(GPIOIN[15:0],1)) && HREADYOUT);
+    ((HRDATA[15:0]==$past(GPIOIN[15:0],1)) && HREADYOUT && !PARITYERR);
   endproperty
 
   always_ff @(posedge HCLK)
@@ -54,10 +55,6 @@ module ahb_gpio_checker
   end
 
 // check behaviour
-  assert_parity: assert property
-  ( @(posedge HCLK) disable iff (!HRESETn)
-    !PARITYERR
-  );
 
   assert_gpio_write: assert property (gpio_write);
   assert_gpio_read:  assert property (gpio_read);

rtl/AHB_VGA/AHBVGASYS_SVA.sv

@@ -0,0 +1,246 @@
+//////////////////////////////////////////////////////////////////////////////////
+//END USER LICENCE AGREEMENT                                                    //
+//                                                                              //
+//Copyright (c) 2012, ARM All rights reserved.                                  //
+//                                                                              //
+//THIS END USER LICENCE AGREEMENT (“LICENCE”) IS A LEGAL AGREEMENT BETWEEN      //
+//YOU AND ARM LIMITED ("ARM") FOR THE USE OF THE SOFTWARE EXAMPLE ACCOMPANYING  //
+//THIS LICENCE. ARM IS ONLY WILLING TO LICENSE THE SOFTWARE EXAMPLE TO YOU ON   //
+//CONDITION THAT YOU ACCEPT ALL OF THE TERMS IN THIS LICENCE. BY INSTALLING OR  //
+//OTHERWISE USING OR COPYING THE SOFTWARE EXAMPLE YOU INDICATE THAT YOU AGREE   //
+//TO BE BOUND BY ALL OF THE TERMS OF THIS LICENCE. IF YOU DO NOT AGREE TO THE   //
+//TERMS OF THIS LICENCE, ARM IS UNWILLING TO LICENSE THE SOFTWARE EXAMPLE TO    //
+//YOU AND YOU MAY NOT INSTALL, USE OR COPY THE SOFTWARE EXAMPLE.                //
+//                                                                              //
+//ARM hereby grants to you, subject to the terms and conditions of this Licence,//
+//a non-exclusive, worldwide, non-transferable, copyright licence only to       //
+//redistribute and use in source and binary forms, with or without modification,//
+//for academic purposes provided the following conditions are met:              //
+//a) Redistributions of source code must retain the above copyright notice, this//
+//list of conditions and the following disclaimer.                              //
+//b) Redistributions in binary form must reproduce the above copyright notice,  //
+//this list of conditions and the following disclaimer in the documentation     //
+//and/or other materials provided with the distribution.                        //
+//                                                                              //
+//THIS SOFTWARE EXAMPLE IS PROVIDED BY THE COPYRIGHT HOLDER "AS IS" AND ARM     //
+//EXPRESSLY DISCLAIMS ANY AND ALL WARRANTIES, EXPRESS OR IMPLIED, INCLUDING     //
+//WITHOUT LIMITATION WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR //
+//PURPOSE, WITH RESPECT TO THIS SOFTWARE EXAMPLE. IN NO EVENT SHALL ARM BE LIABLE/
+//FOR ANY DIRECT, INDIRECT, INCIDENTAL, PUNITIVE, OR CONSEQUENTIAL DAMAGES OF ANY/
+//KIND WHATSOEVER WITH RESPECT TO THE SOFTWARE EXAMPLE. ARM SHALL NOT BE LIABLE //
+//FOR ANY CLAIMS, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, //
+//TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE    //
+//EXAMPLE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE EXAMPLE. FOR THE AVOIDANCE/
+// OF DOUBT, NO PATENT LICENSES ARE BEING LICENSED UNDER THIS LICENSE AGREEMENT.//
+//////////////////////////////////////////////////////////////////////////////////
+
+
+module AHBVGA_SVA(
+  input wire HCLK,
+  input wire HRESETn,
+  input wire [31:0] HADDR,
+  input wire [31:0] HWDATA,
+  input wire HREADY,
+  input wire HWRITE,
+  input wire [1:0] HTRANS,
+  input wire HSEL,
+
+  output wire [31:0] HRDATA,
+  output wire HREADYOUT,
+
+  output wire HSYNC,
+  output wire VSYNC,
+  output wire [7:0] RGB
+);
+  //Register locations
+  localparam IMAGEADDR = 4'hA;
+  localparam CONSOLEADDR = 4'h0;
+
+  //Internal AHB signals
+  reg last_HWRITE;
+  reg last_HSEL;
+  reg [1:0] last_HTRANS;
+  reg [31:0] last_HADDR;
+
+  wire [7:0] console_rgb; //console rgb signal
+  wire [9:0] pixel_x;     //current x pixel
+  wire [9:0] pixel_y;     //current y pixel
+
+  reg console_write;      //write to console
+  reg [7:0] console_wdata;//data to write to console
+  reg image_write;        //write to image
+  reg [7:0] image_wdata;  //data to write to image
+
+  wire [7:0] image_rgb;   //image color
+
+  wire scroll;            //scrolling signal
+
+  wire sel_console;
+  wire sel_image;
+  reg [7:0] cin;
+
+
+  always @(posedge HCLK)
+  if(HREADY)
+    begin
+      last_HADDR <= HADDR;
+      last_HWRITE <= HWRITE;
+      last_HSEL <= HSEL;
+      last_HTRANS <= HTRANS;
+    end
+
+  //Give time for the screen to refresh before writing
+  assign HREADYOUT = ~scroll;
+
+  //VGA interface: control the synchronization and color signals for a particular resolution
+  VGAInterface uVGAInterface (
+    .CLK(HCLK),
+    .resetn(HRESETn),
+    .COLOUR_IN(cin),
+    .cout(RGB),
+    .hs(HSYNC),
+    .vs(VSYNC),
+    .addrh(pixel_x),
+    .addrv(pixel_y)
+    );
+
+  //VGA console module: output the pixels in the text region
+  vga_console uvga_console(
+    .clk(HCLK),
+    .resetn(HRESETn),
+    .pixel_x(pixel_x),
+    .pixel_y(pixel_y),
+    .text_rgb(console_rgb),
+    .font_we(console_write),
+    .font_data(console_wdata),
+    .scroll(scroll)
+    );
+
+  //VGA image buffer: output the pixels in the image region
+  vga_image uvga_image(
+    .clk(HCLK),
+    .resetn(HRESETn),
+    .address(last_HADDR[15:2]),
+    .pixel_x(pixel_x),
+    .pixel_y(pixel_y),
+    .image_we(image_write),
+    .image_data(image_wdata),
+    .image_rgb(image_rgb)
+    );
+
+  assign sel_console = (last_HADDR[23:0]== 12'h000000000000);
+  assign sel_image = (last_HADDR[23:0] != 12'h000000000000);
+
+  //Set console write and write data
+  always @(posedge HCLK, negedge HRESETn)
+  begin
+    if(!HRESETn)
+      begin
+        console_write <= 0;
+        console_wdata <= 0;
+      end
+    else if(last_HWRITE & last_HSEL & last_HTRANS[1] & HREADYOUT & sel_console)
+      begin
+        console_write <= 1'b1;
+        console_wdata <= HWDATA[7:0];
+      end
+    else
+      begin
+        console_write <= 1'b0;
+        console_wdata <= 0;
+      end
+  end
+
+  //Set image write and image write data
+  always @(posedge HCLK, negedge HRESETn)
+  begin
+    if(!HRESETn)
+      begin
+        image_write <= 0;
+        image_wdata <= 0;
+      end
+    else if(last_HWRITE & last_HSEL & last_HTRANS[1] & HREADYOUT & sel_image)
+      begin
+        image_write <= 1'b1;
+        image_wdata <= HWDATA[7:0];
+      end
+    else
+      begin
+        image_write <= 1'b0;
+        image_wdata <= 0;
+      end
+  end
+
+  //Select the rgb color for a particular region
+  always @*
+  begin
+    if(!HRESETn)
+      cin <= 8'h00;
+    else
+      if(pixel_x[9:0]< 240 )
+        cin <= console_rgb ;
+      else
+        cin <= image_rgb;
+  end
+
+  //Assertions and verification
+  int           hcounter;
+  int           vcounter;
+
+  always_ff @(posedge HCLK)
+  begin
+    if(!HRESETn)
+    begin
+      hcounter <= 0;
+      vcounter <= 0;
+    end
+    else
+    begin
+      if($fell(VSYNC))
+        vcounter <= 0;
+      else
+        if($fell(HSYNC))
+          vcounter <= vcounter + 1;
+      if($fell(HSYNC))
+        hcounter <= 0;
+      else
+        hcounter <= hcounter + 1;
+    end
+  end
+
+  assert_display_range_x: assert property
+  ( @(posedge HCLK) disable iff(!HRESETn)
+      0 <= pixel_x <= 640
+  );
+  assert_display_range_y: assert property
+  ( @(posedge HCLK) disable iff(!HRESETn)
+      0 <= pixel_y <= 480
+  );
+
+  assert_vsync_pulse_timer: assert property
+  (
+    @(posedge HCLK) disable iff (!HRESETn)
+    $rose(VSYNC) -> (($past(vcounter,1) == 8'h1) || (vcounter == '0))
+  );
+
+  assert_hsync_pulse_timer: assert property
+  (
+    @(posedge HCLK) disable iff (!HRESETn)
+    ($rose(HSYNC) && !$rose(VSYNC) && VSYNC) -> ($past(hcounter,1)/2 == 8'd95)
+  );
+
+  assert_line_timer: assert property
+  (
+    @(posedge HCLK) disable iff (!HRESETn)
+    ($fell(HSYNC) && !$rose(VSYNC) && VSYNC) -> ($past(hcounter,1)/2 == 800)
+  );
+
+  assert_frame_timer: assert property
+  (
+    @(posedge HCLK) disable iff (!HRESETn)
+    $fell(VSYNC) -> (($past(vcounter,1) == (32'd480 + 32'd10 + 32'd2 + 32'd29)) || (vcounter == '0))
+  );
+
+endmodule
+
+

tbench/ahb_gpio_tb.sv

@@ -74,7 +74,8 @@ module ahb_gpio_tb;
       .HREADYOUT    (gpioif.HREADYOUT),
       .HRDATA       (gpioif.HRDATA),
       .GPIOOUT      (gpioif.GPIOOUT),
-      .PARITYERR    (parity_err)
+      .PARITYERR    (parity_err),
+      .PARITYSEL    (parity_sel)
   );
 
   class gpio_stimulus;

vga.tcl

@@ -0,0 +1,11 @@
+clear -all
+analyze -clear
+analyze -sv rtl/AHB_VGA/AHBVGASYS_SVA.sv rtl/AHB_VGA/counter.sv rtl/AHB_VGA/dual_port_ram_sync.sv rtl/AHB_VGA/font_rom.sv rtl/AHB_VGA/vga_console.sv rtl/AHB_VGA/vga_image.sv rtl/AHB_VGA/vga_sync.sv
+elaborate -bbox_mul 64 -top AHBVGA_SVA
+
+clock HCLK
+reset -expression !(HRESETn)
+
+task -set <embedded>
+set_proofgrid_max_jobs 4
+set_proofgrid_max_local_jobs 4