/* Commands for implementing Brent-Kung adder verification */
#include "driver.h"

/* Vectors of nodes to set high and low at start of every cycle */
static vec_ptr inv_vec = NULL;
static pat_rec inv_pat;
/* For output messages */
static char msg[256];

/* Evaluation limit */
int evallimit = 1 << 30;

static int min(x,y)
int x, y;
{
    if (x < y)
	return (x);
    else
	return (y);
}

/* Exhaustively test adder function */
/* Arguments: in1vec, in2vec, outvec; */
bool doadd(cmdline)
string cmdline;
{
    vec_ptr         in1_vec, in2_vec, out_vec;
    string          token, scmd;
    pat_rec         in1_pat, in2_pat, out_pat;
    int             val1, val2, val_out;
    int             max1, max2;
    int             evalcount;
    scmd = cmdline;
    token = gettoken(&scmd, "");
    in1_vec = find_vec(token);
    if (in1_vec == NULL) {
	sprintf(msg, "Invalid vector: %s\n", token);
	error(msg);
	return (FALSE);
    }
    token = gettoken(&scmd, "");
    in2_vec = find_vec(token);
    if (in2_vec == NULL) {
	sprintf(msg, "Invalid vector: %s\n", token);
	error(msg);
	return (FALSE);
    }
    token = gettoken(&scmd, "");
    out_vec = find_vec(token);
    if (out_vec == NULL) {
	sprintf(msg, "Invalid vector: %s\n", token);
	error(msg);
	return (FALSE);
    }
    new_pat(&in1_pat, 1, width_vec(in1_vec));
    new_pat(&in2_pat, 1, width_vec(in2_vec));
    new_pat(&out_pat, 1, width_vec(out_vec));
    max1 = 1 << width_vec(in1_vec);
    max2 = 1 << width_vec(in2_vec);
    /* Test sequentially */
    evalcount = 0;
    for (val1 = 0; val1 < max1 && evalcount < evallimit; val1++) {
	int_pat(&in1_pat, 0, val1);
	for (val2 = 0; val2 < max2 && evalcount < evallimit; val2++) {
		int_pat(&in2_pat, 0, val2);
		initialize(1);
		set_vec(in1_vec, &in1_pat);
		set_vec(in2_vec, &in2_pat);
		simulate(1, 0, 0);
		get_vec(out_vec, &out_pat);
		val_out = val_pat(&out_pat, 0);
		if (val1 + val2 != val_out) {
		    char            s1[32], s2[32], sout[32];
		    unparse_pat(&in1_pat, s1, BINARY);
		    unparse_pat(&in2_pat, s2, BINARY);
		    unparse_pat(&out_pat, sout, BINARY);
		    sprintf(msg, "%s + %s <> %s\n", s1, s2, sout);
		    error(msg);
		}
		evalcount++;
	}
    }
    free_pat(&in1_pat);
    free_pat(&in2_pat);
    free_pat(&out_pat);
    if (evalcount == evallimit) {
	sprintf(msg, "Evaluation limit of %d reached\n", evallimit);
	output(msg);
    }
    return (TRUE);
}

/* Exhaustively test adder function */
/* Arguments: in1vec, in2vec, outvec; */
/* Uses parallel evaluation */
bool doparadd(cmdline)
string cmdline;
{
    vec_ptr         in1_vec, in2_vec, out_vec;
    string          token, scmd;
    pat_rec         in1_pat, in2_pat, out_pat;
    int             index_set[2], dimension_set[2], val_out;
    register int    nblock, block, ntest, test;
    register int    limit;
    scmd = cmdline;
    token = gettoken(&scmd, "");
    in1_vec = find_vec(token);
    if (in1_vec == NULL) {
	sprintf(msg, "Invalid vector: %s\n", token);
	error(msg);
	return (FALSE);
    }
    token = gettoken(&scmd, "");
    in2_vec = find_vec(token);
    if (in2_vec == NULL) {
	sprintf(msg, "Invalid vector: %s\n", token);
	error(msg);
	return (FALSE);
    }
    token = gettoken(&scmd, "");
    out_vec = find_vec(token);
    if (out_vec == NULL) {
	sprintf(msg, "Invalid vector: %s\n", token);
	error(msg);
	return (FALSE);
    }
    new_pat(&in1_pat, MAXparallel, width_vec(in1_vec));
    new_pat(&in2_pat, MAXparallel, width_vec(in2_vec));
    new_pat(&out_pat, MAXparallel, width_vec(out_vec));
    limit = evallimit;
    dimension_set[0] = min(1 << width_vec(in1_vec), limit);
    limit /= dimension_set[0];
    dimension_set[1] = min(1 << width_vec(in2_vec), limit);
    /* Test in parallel */
	nblock = block_cnt(dimension_set, 2);
    for (block = 0; block < nblock; block++) {
	ntest = test_cnt(dimension_set, 2, block);
	resize_pat(&in1_pat, ntest, M_WIDTH_PAT(&in1_pat));
	resize_pat(&in2_pat, ntest, M_WIDTH_PAT(&in2_pat));
	resize_pat(&out_pat, ntest, M_WIDTH_PAT(&out_pat));
	initialize(ntest);
	for (test = 0; test < ntest; test++) {
	    find_index(dimension_set, index_set, 2, block, test);
	    int_pat(&in1_pat, test, index_set[0]);
	    int_pat(&in2_pat, test, index_set[1]);
	}
	set_vec(in1_vec, &in1_pat);
	set_vec(in2_vec, &in2_pat);
	simulate(1, 0, 0);
	get_vec(out_vec, &out_pat);
	for (test = 0; test < ntest; test++) {
	    find_index(dimension_set, index_set, 2, block, test);
	    val_out = val_pat(&out_pat, test);
	    if (index_set[0] + index_set[1] != val_out) {
		char            s1[33], s2[33], sout[33];
		int             w;
		pat_rec         show_pat;
		w = width_pat(&in1_pat);
		new_pat(&show_pat, 1, w);
		copy_pat(&in1_pat, &show_pat, test, 0, 0, 0, 1, w);
		unparse_pat(&show_pat, s1, BINARY);

		w = width_pat(&in2_pat);
		resize_pat(&show_pat, 1, w);
		copy_pat(&in2_pat, &show_pat, test, 0, 0, 0, 1, w);
		unparse_pat(&show_pat, s2, BINARY);

		w = width_pat(&out_pat);
		resize_pat(&show_pat, 1, w);
		copy_pat(&out_pat, &show_pat, test, 0, 0, 0, 1, w);
		unparse_pat(&show_pat, sout, BINARY);
		sprintf(msg, "%s + %s <> %s\n", s1, s2, sout);
		error(msg);
		free_pat(&show_pat);
	    }
	}
    }
    free_pat(&in1_pat);
    free_pat(&in2_pat);
    free_pat(&out_pat);
    return (TRUE);
}