source: vis_dev/vis-2.1/examples/ping_pong/ping_pong.v @ 11

/*
 * This code implements a game of ping pong (table tennis) between 2 players, with
 * a slight twist: each player puts a ball into play at the same time.  There can
 * be an indefinite delay from the time one player hits a ball until the time that 
 * the other player returns it.  If both balls are in play, then both players 
 * always hit each ball at the same instant.
 *
 * While both balls are in play, exactly one player may choose not to return his 
 * ball.  This leaves one ball in play.  If just one ball is in play, the ball 
 * should remain in play forever.
 */

typedef enum {BALL, NO_BALL} player_status;
typedef enum {HIT, NO_HIT} action_type;

module ping_pong(clk); 
input clk; 

/* signal declarations */
action_type wire action_A, action_B;
player_status wire state_A, state_B; 

/* the ping pong players */
player player_A(clk, action_B, action_A, state_A);
player player_B(clk, action_A, action_B, state_B);

never_no_balls nnb(clk, state_A, state_B);
infinitely_often_hit ioh(clk, action_A);

endmodule 
 

/*
 * Two state process.  If the player doesn't have the ball (state NO_BALL) and the 
 * opponent hits the ball, then go to state BALL.  If the player has the ball, then
 * if he doesn't hit the ball, then he remains in state BALL.  If he hits the ball,
 * and the opponent doesn't also hit the ball, then go to state NO_BALL.
 */
module player(clk, opponent, me, state); 
input clk; 
input opponent; 
output me;
output state;

action_type wire opponent, me, random;
player_status reg state;

initial state = BALL;

/* set the value of the output of the player */

assign random = $ND(HIT, NO_HIT);
assign me = (state == BALL) ? random : NO_HIT;

always @(posedge clk) begin
    case(state)
        BALL:
            begin
            if ((me == HIT) && (opponent == NO_HIT))
                state = NO_BALL;
            end

        NO_BALL:
            begin
            if (opponent == HIT) 
                state = BALL;
            end
     
        default:;
        endcase;
end
endmodule

/*
 * If it's ever the case that neither player has a ball, then go to state BAD
 * and stay there.
 */
typedef enum {GOOD, BAD} prop1_status;

module never_no_balls(clk, state_A, state_B); 
input clk; 
input state_A;
input state_B;

player_status wire state_A, state_B;
prop1_status reg state;

initial state = GOOD;

always @(posedge clk) begin
    case(state)
        GOOD:
            begin
            if ((state_A == NO_BALL) && (state_B == NO_BALL))
                state = BAD;
            end

        BAD:
            begin
            state = BAD;
            end

        default:;
        endcase;
end
endmodule


/*
 * If player does not hit the ball now, then he will sometime in the future. 
 */
typedef enum {OKAY, PENDING} prop2_status;

module infinitely_often_hit(clk, player_action); 
input clk; 
input player_action;

action_type wire player_action;
prop2_status reg state;

initial state = OKAY;

always @(posedge clk) begin
    case(state)
        OKAY:
            begin
            if (player_action == NO_HIT)
                state = PENDING;
            end

        PENDING:
            begin
            if (player_action == HIT)
                state = OKAY;
            end

        default:;
        endcase;
end
endmodule