tclbdd

Check-in [1513a7c798]
Login

Many hyperlinks are disabled.
Use anonymous login to enable hyperlinks.

Overview
Comment:add circuit verification example
Timelines: family | ancestors | descendants | both | trunk
Files: files | file ages | folders
SHA1:1513a7c798c5b531e125d7121266cf413333a2d7
User & Date: kennykb 2013-11-30 17:38:55
Context
2013-11-30
17:50
remove dribble from bdd-12.13 check-in: 8f7b52fae4 user: kennykb tags: trunk
17:38
add circuit verification example check-in: 1513a7c798 user: kennykb tags: trunk
16:34
Add 8-queens example as a test. check-in: 2cbd4f3ba6 user: kennykb tags: trunk
Changes
Hide Diffs Unified Diffs Ignore Whitespace Patch

Changes to tests/bdd.test.

925
926
927
928
929
930
931




































































932
933
934
935
936
937
938

	sys satcount solution

    }
    -cleanup {rename sys {}}
    -result 92
}





































































test bdd-13.n {restrict - reduce to constant} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0
	sys nthvar b 1
	sys nthvar c 2







>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>







925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
1001
1002
1003
1004
1005
1006

	sys satcount solution

    }
    -cleanup {rename sys {}}
    -result 92
}

test bdd-12.13 {verification of a full adder} {
    -setup {
	bdd::system create sys
	sys nthvar x 0; sys notnthvar !x 0
	sys nthvar y 1; sys notnthvar !y 1
	sys nthvar ci 2; sys notnthvar !ci 2
    }
    -body {

	# specification is a truth table
	sys constant spec_co 0
	sys constant spec_z 0
	foreach {x y ci co z} {
	    0 0 0 0 0
	    0 0 1 0 1
	    0 1 0 0 1
	    0 1 1 1 0

	    1 0 0 0 1
	    1 0 1 1 0
	    1 1 0 1 0
	    1 1 1 1 1
	} {
	    if {$x} {
		set xlit x
	    } else {
		set xlit !x
	    }
	    if {$y} {
		set ylit y
	    } else {
		set ylit !y
	    }
	    if {$ci} {
		set cilit ci
	    } else {
		set cilit !ci
	    }
	    sys & input $cilit $ylit
	    sys & input input $xlit
	    if {$co} {
		puts "spec co |= $xlit & $ylit & $cilit"
		sys | spec_co spec_co input
	    }
	    if {$z} {
		puts "spec z |= $xlit & $ylit & $cilit"
		sys | spec_z spec_z input
	    }
	}

	puts "[sys satcount spec_co] [sys satcount spec_z]"

	# implementation is a gate array
	sys & gate1 x y
	sys ^ gate2 x y
	sys & gate3 gate2 ci
	sys ^ z gate2 ci
	sys | co gate1 gate3

	puts "[sys satcount co] [sys satcount z]"
	list [expr {[sys beadindex co] == [sys beadindex spec_co]}] \
	    [expr {[sys beadindex z] == [sys beadindex spec_z]}]
    }
    -cleanup {rename sys {}}
    -result {1 1}
}
		

test bdd-13.n {restrict - reduce to constant} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0
	sys nthvar b 1
	sys nthvar c 2