From dbd1e7f6ea93150f446ab5b3656ce15e76fb85d5 Mon Sep 17 00:00:00 2001 From: Shashank V M Date: Sat, 15 Nov 2025 20:54:05 +0530 Subject: [PATCH 1/2] Make the counter synthesizable, update comment - Use nonblocking assignment for counter. Sequential design use nonblockgin assignments. - Add reset and remove initial block as initial block is not synthesizable - Add counter output port --- regression/ebmc/ranking-function/counter2.sv | 22 +++++++++++--------- 1 file changed, 12 insertions(+), 10 deletions(-) diff --git a/regression/ebmc/ranking-function/counter2.sv b/regression/ebmc/ranking-function/counter2.sv index df2be4f13..4faece715 100644 --- a/regression/ebmc/ranking-function/counter2.sv +++ b/regression/ebmc/ranking-function/counter2.sv @@ -1,16 +1,18 @@ -// count down from 10 to 0 +// count up from 0 to 10 -module main(input clk); +module main( + input logic clk, + input logic reset + output logic [3:0] counter, + ); - reg [3:0] counter; - - initial counter = 0; - - always @(posedge clk) - if(counter != 10) - counter = counter + 1; + always_ff @(posedge clk or posedge reset) + if (reset) + counter <= 'b0; + else if (counter != 10) + counter <= counter + 1; // expected to pass - p0: assert property (s_eventually counter == 10); + ASSERT_COUNTER_EVENTUALLY_10: assert property (@(posedge clk) disable iff (reset) s_eventually (counter == 10)); endmodule From a0b312bb298b8a2f5ebb947c5547201bdc269a75 Mon Sep 17 00:00:00 2001 From: Shashank V M Date: Sat, 15 Nov 2025 23:57:33 +0530 Subject: [PATCH 2/2] Fix syntax for module declaration in counter2.sv --- regression/ebmc/ranking-function/counter2.sv | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/regression/ebmc/ranking-function/counter2.sv b/regression/ebmc/ranking-function/counter2.sv index 4faece715..e1d200a29 100644 --- a/regression/ebmc/ranking-function/counter2.sv +++ b/regression/ebmc/ranking-function/counter2.sv @@ -2,9 +2,8 @@ module main( input logic clk, - input logic reset - output logic [3:0] counter, - ); + input logic reset, + output logic [3:0] counter); always_ff @(posedge clk or posedge reset) if (reset)